changeset 24825 | c4f13ab78f9d |
parent 23467 | d1b97708d5eb |
child 32153 | a0e57fb1b930 |
--- a/src/CCL/Fix.thy Wed Oct 03 19:49:33 2007 +0200 +++ b/src/CCL/Fix.thy Wed Oct 03 21:29:05 2007 +0200 @@ -14,10 +14,11 @@ idgen :: "[i]=>i" INCL :: "[i=>o]=>o" -axioms +defs idgen_def: "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))" +axioms 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)))"