src/CCL/Fix.thy
changeset 24825 c4f13ab78f9d
parent 23467 d1b97708d5eb
child 32153 a0e57fb1b930
equal deleted inserted replaced
24824:b7866aea0815 24825:c4f13ab78f9d
    12 
    12 
    13 consts
    13 consts
    14   idgen      ::       "[i]=>i"
    14   idgen      ::       "[i]=>i"
    15   INCL      :: "[i=>o]=>o"
    15   INCL      :: "[i=>o]=>o"
    16 
    16 
    17 axioms
    17 defs
    18   idgen_def:
    18   idgen_def:
    19   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
    19   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
    20 
    20 
       
    21 axioms
    21   INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
    22   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   po_INCL:    "INCL(%x. a(x) [= b(x))"
    23   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
    24   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
    24 
    25 
    25 
    26