author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
permissions | -rw-r--r-- |
435 | 1 |
(* Title: ZF/Nat.thy |
0 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
435 | 4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
Natural numbers in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
435 | 9 |
Nat = Ordinal + Bool + "mono" + |
0 | 10 |
consts |
1401 | 11 |
nat :: i |
12 |
nat_case :: [i, i=>i, i]=>i |
|
13 |
nat_rec :: [i, i, [i,i]=>i]=>i |
|
0 | 14 |
|
753 | 15 |
defs |
0 | 16 |
|
17 |
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
|
18 |
||
19 |
nat_case_def |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
20 |
"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
0 | 21 |
|
22 |
nat_rec_def |
|
1155 | 23 |
"nat_rec(k,a,b) == |
24 |
wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))" |
|
0 | 25 |
|
26 |
end |