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