src/CCL/Fix.thy
 changeset 42156 df219e736a5d parent 36319 8feb2c4bef1a child 58889 5b7a9633cfa8
equal inserted replaced
42155:ffe99b07c9c0 42156:df219e736a5d
`     7 `
`     7 `
`     8 theory Fix`
`     8 theory Fix`
`     9 imports Type`
`     9 imports Type`
`    10 begin`
`    10 begin`
`    11 `
`    11 `
`    12 consts`
`    12 definition idgen :: "i => i"`
`    13   idgen      ::       "[i]=>i"`
`    13   where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"`
`    14   INCL      :: "[i=>o]=>o"`
`       `
`    15 `
`    14 `
`    16 defs`
`    15 axiomatization INCL :: "[i=>o]=>o" where`
`    17   idgen_def:`
`    16   INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and`
`    18   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"`
`    17   po_INCL: "INCL(%x. a(x) [= b(x))" and`
`    19 `
`       `
`    20 axioms`
`       `
`    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)))"`
`    18   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"`
`    24 `
`    19 `
`    25 `
`    20 `
`    26 subsection {* Fixed Point Induction *}`
`    21 subsection {* Fixed Point Induction *}`
`    27 `
`    22 `