923
|
1 |
(* Title: HOL/Nat.thy
|
|
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 |
|
|
13 |
(** type ind **)
|
|
14 |
|
|
15 |
types
|
|
16 |
ind
|
|
17 |
|
|
18 |
arities
|
|
19 |
ind :: term
|
|
20 |
|
|
21 |
consts
|
|
22 |
Zero_Rep :: "ind"
|
|
23 |
Suc_Rep :: "ind => ind"
|
|
24 |
|
|
25 |
rules
|
|
26 |
(*the axiom of infinity in 2 parts*)
|
|
27 |
inj_Suc_Rep "inj(Suc_Rep)"
|
|
28 |
Suc_Rep_not_Zero_Rep "Suc_Rep(x) ~= Zero_Rep"
|
|
29 |
|
|
30 |
|
|
31 |
|
|
32 |
(** type nat **)
|
|
33 |
|
|
34 |
(* type definition *)
|
|
35 |
|
|
36 |
subtype (Nat)
|
|
37 |
nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def)
|
|
38 |
|
|
39 |
instance
|
|
40 |
nat :: ord
|
|
41 |
|
|
42 |
|
|
43 |
(* abstract constants and syntax *)
|
|
44 |
|
|
45 |
consts
|
|
46 |
"0" :: "nat" ("0")
|
|
47 |
Suc :: "nat => nat"
|
|
48 |
nat_case :: "['a, nat => 'a, nat] => 'a"
|
|
49 |
pred_nat :: "(nat * nat) set"
|
|
50 |
nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
|
|
51 |
|
|
52 |
translations
|
|
53 |
"case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
|
|
54 |
|
|
55 |
defs
|
|
56 |
Zero_def "0 == Abs_Nat(Zero_Rep)"
|
|
57 |
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
|
|
58 |
|
|
59 |
(*nat operations and recursion*)
|
|
60 |
nat_case_def "nat_case a f n == @z. (n=0 --> z=a) \
|
|
61 |
\ & (!x. n=Suc(x) --> z=f(x))"
|
|
62 |
pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
|
|
63 |
|
|
64 |
less_def "m<n == <m,n>:trancl(pred_nat)"
|
|
65 |
|
|
66 |
le_def "m<=(n::nat) == ~(n<m)"
|
|
67 |
|
|
68 |
nat_rec_def "nat_rec n c d == wfrec pred_nat n \
|
|
69 |
\ (nat_case (%g.c) (%m g.(d m (g m))))"
|
|
70 |
end
|