1474

1 
(* Title: CCL/Lazy/fix.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen

0

4 
Copyright 1993 University of Cambridge


5 


6 
Tentative attempt at including fixed point induction.


7 
Justified by Smith.


8 
*)


9 


10 
Fix = Type +


11 


12 
consts


13 

1474

14 
idgen :: "[i]=>i"

0

15 
INCL :: "[i=>o]=>o"


16 


17 
rules


18 


19 
idgen_def

3837

20 
"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"

0

21 

3837

22 
INCL_def "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) > P(fix(f)))"


23 
po_INCL "INCL(%x. a(x) [= b(x))"


24 
INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"

0

25 


26 
end
