17456

1 
(* Title: CCL/Fix.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen

0

4 
Copyright 1993 University of Cambridge


5 
*)


6 

17456

7 
header {* Tentative attempt at including fixed point induction; justified by Smith *}


8 


9 
theory Fix


10 
imports Type


11 
begin

0

12 


13 
consts

1474

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

0

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


16 

17456

17 
axioms


18 
idgen_def:

3837

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

0

20 

17456

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


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


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


24 


25 
ML {* use_legacy_bindings (the_context ()) *}

0

26 


27 
end
