equal
deleted
inserted
replaced
|
1 (* Title: ZF/nat.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Natural numbers in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 Nat = Ord + Bool + |
|
10 consts |
|
11 nat :: "i" |
|
12 nat_case :: "[i, i, i=>i]=>i" |
|
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
|
14 |
|
15 rules |
|
16 |
|
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
|
18 |
|
19 nat_case_def |
|
20 "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
|
21 |
|
22 nat_rec_def |
|
23 "nat_rec(k,a,b) == \ |
|
24 \ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))" |
|
25 |
|
26 end |