author | paulson |
Tue, 03 Jul 2001 15:28:24 +0200 | |
changeset 11394 | e88c2c89f98e |
parent 11326 | 680ebd093cfe |
child 11464 | ddea204de5bc |
permissions | -rw-r--r-- |
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 |
||
10212 | 11 |
NatDef = Wellfounded_Recursion + |
2608 | 12 |
|
13 |
(** type ind **) |
|
14 |
||
3947 | 15 |
global |
16 |
||
2608 | 17 |
types |
18 |
ind |
|
19 |
||
20 |
arities |
|
21 |
ind :: term |
|
22 |
||
23 |
consts |
|
24 |
Zero_Rep :: ind |
|
25 |
Suc_Rep :: ind => ind |
|
26 |
||
27 |
rules |
|
28 |
(*the axiom of infinity in 2 parts*) |
|
29 |
inj_Suc_Rep "inj(Suc_Rep)" |
|
30 |
Suc_Rep_not_Zero_Rep "Suc_Rep(x) ~= Zero_Rep" |
|
31 |
||
32 |
||
33 |
||
34 |
(** type nat **) |
|
35 |
||
36 |
(* type definition *) |
|
37 |
||
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
38 |
consts |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
39 |
Nat' :: "ind set" |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
40 |
|
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
41 |
inductive Nat' |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
42 |
intrs |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
43 |
Zero_RepI "Zero_Rep : Nat'" |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
44 |
Suc_RepI "i : Nat' ==> Suc_Rep i : Nat'" |
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
45 |
|
2608 | 46 |
typedef (Nat) |
11326
680ebd093cfe
Representing set for type nat is now defined via "inductive".
berghofe
parents:
10832
diff
changeset
|
47 |
nat = "Nat'" (Nat'.Zero_RepI) |
2608 | 48 |
|
49 |
instance |
|
8943 | 50 |
nat :: {ord, zero} |
2608 | 51 |
|
52 |
||
53 |
(* abstract constants and syntax *) |
|
54 |
||
55 |
consts |
|
56 |
Suc :: nat => nat |
|
57 |
pred_nat :: "(nat * nat) set" |
|
58 |
||
59 |
syntax |
|
60 |
"1" :: nat ("1") |
|
61 |
"2" :: nat ("2") |
|
62 |
||
63 |
translations |
|
5187
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
3947
diff
changeset
|
64 |
"1" == "Suc 0" |
55f07169cf5f
Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents:
3947
diff
changeset
|
65 |
"2" == "Suc 1" |
2608 | 66 |
|
67 |
||
3947 | 68 |
local |
69 |
||
2608 | 70 |
defs |
71 |
Zero_def "0 == Abs_Nat(Zero_Rep)" |
|
72 |
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
|
73 |
||
7872 | 74 |
(*nat operations*) |
3236 | 75 |
pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
2608 | 76 |
|
77 |
less_def "m<n == (m,n):trancl(pred_nat)" |
|
78 |
||
79 |
le_def "m<=(n::nat) == ~(n<m)" |
|
80 |
||
81 |
end |