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) ('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

V