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


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


21 


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)))"


25 


26 
end
