|
0
|
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
|