|
0
|
1 |
(* Title: ZF/epsilon.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Epsilon induction and recursion
|
|
|
7 |
*)
|
|
|
8 |
|
|
124
|
9 |
Epsilon = Nat + "mono" +
|
|
0
|
10 |
consts
|
|
|
11 |
eclose,rank :: "i=>i"
|
|
|
12 |
transrec :: "[i, [i,i]=>i] =>i"
|
|
|
13 |
|
|
|
14 |
rules
|
|
|
15 |
eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
|
|
|
16 |
transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
|
|
|
17 |
rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
|
|
|
18 |
end
|