1478
|
1 |
(* Title: ZF/epsilon.thy
|
0
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Epsilon induction and recursion
|
|
7 |
*)
|
|
8 |
|
2469
|
9 |
Epsilon = Nat + mono +
|
|
10 |
constdefs
|
|
11 |
eclose :: i=>i
|
|
12 |
"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
|
0
|
13 |
|
2469
|
14 |
transrec :: [i, [i,i]=>i] =>i
|
|
15 |
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
|
|
16 |
|
|
17 |
rank :: i=>i
|
|
18 |
"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
|
|
19 |
|
|
20 |
transrec2 :: [i, i, [i,i]=>i] =>i
|
|
21 |
"transrec2(k, a, b) ==
|
|
22 |
transrec(k,
|
|
23 |
%i r. if(i=0, a,
|
|
24 |
if(EX j. i=succ(j),
|
|
25 |
b(THE j. i=succ(j), r`(THE j. i=succ(j))),
|
|
26 |
UN j<i. r`j)))"
|
|
27 |
|
6070
|
28 |
recursor :: [i, [i,i]=>i, i]=>i
|
|
29 |
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
|
|
30 |
|
|
31 |
rec :: [i, i, [i,i]=>i]=>i
|
|
32 |
"rec(k,a,b) == recursor(a,b,k)"
|
|
33 |
|
0
|
34 |
end
|