diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Fix.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,26 +1,27 @@ -(* Title: CCL/Lazy/fix.thy +(* Title: CCL/Fix.thy ID: \$Id\$ Author: Martin Coen Copyright 1993 University of Cambridge - -Tentative attempt at including fixed point induction. -Justified by Smith. *) -Fix = Type + +header {* Tentative attempt at including fixed point induction; justified by Smith *} + +theory Fix +imports Type +begin consts - idgen :: "[i]=>i" INCL :: "[i=>o]=>o" -rules - - idgen_def +axioms + idgen_def: "idgen(f) == lam t. case(t,true,false,%x y.,%u. lam x. f ` u(x))" - INCL_def "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" - po_INCL "INCL(%x. a(x) [= b(x))" - INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" + INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" + po_INCL: "INCL(%x. a(x) [= b(x))" + INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" + +ML {* use_legacy_bindings (the_context ()) *} end