|
2608
|
1 |
(* Title: HOL/NatDef.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 |
NatDef = 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 |
typedef (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 :: ['a, [nat, 'a] => 'a, nat] => 'a
|
|
|
51 |
|
|
|
52 |
syntax
|
|
|
53 |
"1" :: nat ("1")
|
|
|
54 |
"2" :: nat ("2")
|
|
|
55 |
|
|
|
56 |
translations
|
|
|
57 |
"1" == "Suc 0"
|
|
|
58 |
"2" == "Suc 1"
|
|
|
59 |
"case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
|
|
|
60 |
|
|
|
61 |
|
|
|
62 |
defs
|
|
|
63 |
Zero_def "0 == Abs_Nat(Zero_Rep)"
|
|
|
64 |
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
|
|
|
65 |
|
|
|
66 |
(*nat operations and recursion*)
|
|
|
67 |
nat_case_def "nat_case a f n == @z. (n=0 --> z=a)
|
|
|
68 |
& (!x. n=Suc x --> z=f(x))"
|
|
|
69 |
pred_nat_def "pred_nat == {p. ? n. p = (n, Suc n)}"
|
|
|
70 |
|
|
|
71 |
less_def "m<n == (m,n):trancl(pred_nat)"
|
|
|
72 |
|
|
|
73 |
le_def "m<=(n::nat) == ~(n<m)"
|
|
|
74 |
|
|
|
75 |
nat_rec_def "nat_rec c d ==
|
|
|
76 |
wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
|
|
|
77 |
end
|