|
1 (* Title: HOL/nat |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Definition of types ind and nat. |
|
7 |
|
8 Type nat is defined as a set Nat over type ind. |
|
9 *) |
|
10 |
|
11 Nat = WF + |
|
12 types ind,nat 0 |
|
13 arities ind,nat :: term |
|
14 nat :: ord |
|
15 |
|
16 consts |
|
17 Zero_Rep :: "ind" |
|
18 Suc_Rep :: "ind => ind" |
|
19 Nat :: "ind set" |
|
20 Rep_Nat :: "nat => ind" |
|
21 Abs_Nat :: "ind => nat" |
|
22 Suc :: "nat => nat" |
|
23 nat_case :: "[nat, 'a, nat=>'a] =>'a" |
|
24 pred_nat :: "(nat*nat) set" |
|
25 nat_rec :: "[nat, 'a, [nat, 'a]=>'a] => 'a" |
|
26 "0" :: "nat" ("0") |
|
27 |
|
28 rules |
|
29 (*the axiom of infinity in 2 parts*) |
|
30 inj_Suc_Rep "inj(Suc_Rep)" |
|
31 Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)" |
|
32 Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" |
|
33 (*faking a type definition...*) |
|
34 Rep_Nat "Rep_Nat(n): Nat" |
|
35 Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n" |
|
36 Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i" |
|
37 (*defining the abstract constants*) |
|
38 Zero_def "0 == Abs_Nat(Zero_Rep)" |
|
39 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
|
40 (*nat operations and recursion*) |
|
41 nat_case_def "nat_case == (%n a f. @z. (n=0 --> z=a) \ |
|
42 \ & (!x. n=Suc(x) --> z=f(x)))" |
|
43 pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}" |
|
44 |
|
45 less_def "m<n == <m,n>:trancl(pred_nat)" |
|
46 |
|
47 le_def "m<=n::nat == ~(n<m)" |
|
48 |
|
49 nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \ |
|
50 \ %l g. nat_case(l, c, %m. d(m,g(m))))" |
|
51 end |