The Theory fixp
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)
fill→ ('a LIST → ONE + 'b) × ('a LIST → ONE + 'b)
fill→ 'a LIST
fill→ 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)
fill→ ('a LIST → ONE + 'b) + ('a LIST → ONE + 'b)
fill→ 'a LIST
fill→ ONE + 'b
IndList
(ℕ → 'a)
fill→ ('a LIST → ONE + 'b) LIST
fill→ 'a LIST
fill→ 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
fill• cc2monof (tor, tent)
fill= (λ s
fill• s ∪ {t|∃ u v• u = tent v ∧ u ⊆ s ∧ t = tor v})
closure
⊢ ∀ tor tent
fill• closure (tor, tent) = lfp (cc2monof (tor, tent))
IndPair
⊢ ∀ i l r h t
fill• IndPair i (l, r) [] = InL One
fill∧ IndPair i (l, r) (Cons h t)
fill= (if h = i F
fillthen l t
fillelse if h = i T
fillthen r t
fillelse InL One)
IndInL
⊢ ∀ i j h t
fill• IndInL i j [] = InL One
fill∧ IndInL i j (Cons h t)
fill= (if h = i F then j t else InL One)
IndInR
⊢ ∀ i j h t
fill• IndInR i j [] = InL One
fill∧ IndInR i j (Cons h t)
fill= (if h = i T then j t else InL One)
IndSum
⊢ ∀ i j h t
fill• IndSum i j [] = InL One
fill∧ IndSum i j (Cons h t)
fill= (if IsL j
fillthen if h = i F then OutL j t else InL One
fillelse if h = i T
fillthen OutR j t
fillelse InL One)
IndList
⊢ ∀ i ha ta hb tb
fill• IndList i [] tb = InL One
fill∧ IndList i (Cons ha ta) [] = InL One
fill∧ IndList i (Cons ha ta) (Cons hb tb)
fill= (if ∃ j• hb = i j ∧ j < Length ta
fillthen IndList i ta (Cons hb tb)
fillelse if hb = i (Length ta)
fillthen ha tb
fillelse 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
fill• tent x = s ∧ s ⊆ closure (tor, tent) ∧ y = tor x
fill⇒ y ∈ closure (tor, tent)
closure_induction_thm
⊢ ∀ tor tent p
fill• (∀ x• (∃ y• tor y = x ∧ tent y ⊆ p) ⇒ x ∈ p)
fill⇒ closure (tor, tent) ⊆ p

up quick index

privacy policy

Created:

V