author | wenzelm |
Fri, 08 Oct 1993 14:29:55 +0100 | |
changeset 46 | f0f4978af183 |
parent 0 | a5a9c433f639 |
child 124 | 858ab9a9b047 |
permissions | -rw-r--r-- |
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 |
||
9 |
Epsilon = Nat + |
|
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 |