equal
deleted
inserted
replaced
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 |