7 |
7 |
8 header{*Epsilon Induction and Recursion*} |
8 header{*Epsilon Induction and Recursion*} |
9 |
9 |
10 theory Epsilon imports Nat begin |
10 theory Epsilon imports Nat begin |
11 |
11 |
12 constdefs |
12 definition |
13 eclose :: "i=>i" |
13 eclose :: "i=>i" where |
14 "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))" |
14 "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))" |
15 |
15 |
16 transrec :: "[i, [i,i]=>i] =>i" |
16 definition |
|
17 transrec :: "[i, [i,i]=>i] =>i" where |
17 "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" |
18 "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" |
18 |
19 |
19 rank :: "i=>i" |
20 definition |
|
21 rank :: "i=>i" where |
20 "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))" |
22 "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))" |
21 |
23 |
22 transrec2 :: "[i, i, [i,i]=>i] =>i" |
24 definition |
|
25 transrec2 :: "[i, i, [i,i]=>i] =>i" where |
23 "transrec2(k, a, b) == |
26 "transrec2(k, a, b) == |
24 transrec(k, |
27 transrec(k, |
25 %i r. if(i=0, a, |
28 %i r. if(i=0, a, |
26 if(EX j. i=succ(j), |
29 if(EX j. i=succ(j), |
27 b(THE j. i=succ(j), r`(THE j. i=succ(j))), |
30 b(THE j. i=succ(j), r`(THE j. i=succ(j))), |
28 \<Union>j<i. r`j)))" |
31 \<Union>j<i. r`j)))" |
29 |
32 |
30 recursor :: "[i, [i,i]=>i, i]=>i" |
33 definition |
|
34 recursor :: "[i, [i,i]=>i, i]=>i" where |
31 "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" |
35 "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" |
32 |
36 |
33 rec :: "[i, i, [i,i]=>i]=>i" |
37 definition |
|
38 rec :: "[i, i, [i,i]=>i]=>i" where |
34 "rec(k,a,b) == recursor(a,b,k)" |
39 "rec(k,a,b) == recursor(a,b,k)" |
35 |
40 |
36 |
41 |
37 subsection{*Basic Closure Properties*} |
42 subsection{*Basic Closure Properties*} |
38 |
43 |