| Parents |
| hol |
| Constants |
|
monotonic
|
('a SET → 'b SET) → BOOL |
|
lfp
|
('a SET → 'a SET) → 'a SET |
|
gfp
|
('a SET → 'a SET) → 'a SET |
|
cc2monof
|
('a → 'b) × ('a → 'b SET) → 'b SET → 'b SET |
|
closure
|
('a → 'b) × ('a → 'b SET) → 'b SET |
|
IndPair
|
(BOOL → 'a)  → ('a LIST → ONE + 'b) × ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b
|
|
IndInL
|
(BOOL → 'a) → ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b |
|
IndInR
|
(BOOL → 'a) → ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b |
|
IndSum
|
(BOOL → 'a) → ('a LIST → ONE + 'b) + ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b
|
|
IndList
|
(ℕ → 'a) → ('a LIST → ONE + 'b) LIST → 'a LIST → ONE + 'b
|
| Definitions |
|
monotonic
|
⊢ ∀ f• monotonic f ⇔ (∀ x y• x ⊆ y ⇒ f x ⊆ f y) |
|
lfp
|
⊢ ∀ f• lfp f = ⋂ {X|f X ⊆ X} |
|
gfp
|
⊢ ∀ f• gfp f = ⋃ {X|X ⊆ f X} |
|
cc2monof
|
⊢ ∀ tor tent • cc2monof (tor, tent) = (λ s • s ∪ {t|∃ u v• u = tent v ∧ u ⊆ s ∧ t = tor v})
|
|
closure
|
⊢ ∀ tor tent • closure (tor, tent) = lfp (cc2monof (tor, tent))
|
|
IndPair
|
⊢ ∀ i l r h t • IndPair i (l, r) [] = InL One ∧ IndPair i (l, r) (Cons h t) = (if h = i F then l t else if h = i T then r t else InL One)
|
|
IndInL
|
⊢ ∀ i j h t • IndInL i j [] = InL One ∧ IndInL i j (Cons h t) = (if h = i F then j t else InL One)
|
|
IndInR
|
⊢ ∀ i j h t • IndInR i j [] = InL One ∧ IndInR i j (Cons h t) = (if h = i T then j t else InL One)
|
|
IndSum
|
⊢ ∀ i j h t • IndSum i j [] = InL One ∧ IndSum i j (Cons h t) = (if IsL j then if h = i F then OutL j t else InL One else if h = i T then OutR j t else InL One)
|
|
IndList
|
⊢ ∀ i ha ta hb tb • IndList i [] tb = InL One ∧ IndList i (Cons ha ta) [] = InL One ∧ IndList i (Cons ha ta) (Cons hb tb) = (if ∃ j• hb = i j ∧ j < Length ta then IndList i ta (Cons hb tb) else if hb = i (Length ta) then ha tb else InL One)
|
| Theorems |
|
least_fixpoint_thm
|
⊢ ∀ h• monotonic h ⇒ h (lfp h) = lfp h |
|
lfp_min_thm
|
⊢ ∀ h• monotonic h ⇒ (∀ g• h g = g ⇒ lfp h ⊆ g) |
|
lfp_induction_thm
|
⊢ ∀ h• monotonic h ⇒ (∀ s• h s ⊆ s ⇒ lfp h ⊆ s) |
|
greatest_fixpoint_thm
|
⊢ ∀ h• monotonic h ⇒ h (gfp h) = gfp h |
|
gfp_max_thm
|
⊢ ∀ h• monotonic h ⇒ (∀ g• h g = g ⇒ g ⊆ gfp h) |
|
gfp_coinduction_thm
|
⊢ ∀ h• monotonic h ⇒ (∀ s• s ⊆ h s ⇒ s ⊆ gfp h) |
|
mono_cc2monof_thm
|
⊢ ∀ tor tent• monotonic (cc2monof (tor, tent)) |
|
closure_thm1
|
⊢ ∀ tor tent s x y • tent x = s ∧ s ⊆ closure (tor, tent) ∧ y = tor x ⇒ y ∈ closure (tor, tent)
|
|
closure_induction_thm
|
⊢ ∀ tor tent p
• (∀ x• (∃ y• tor y = x ∧ tent y ⊆ p) ⇒ x ∈ p) ⇒ closure (tor, tent) ⊆ p
|
