|
5078
|
1 |
(* Title : PNat.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
|
4 |
Description : The positive naturals
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
|
|
|
8 |
PNat = Arith +
|
|
|
9 |
|
|
|
10 |
(** type pnat **)
|
|
|
11 |
|
|
|
12 |
(* type definition *)
|
|
|
13 |
|
|
|
14 |
typedef
|
|
|
15 |
pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)
|
|
|
16 |
|
|
|
17 |
instance
|
|
|
18 |
pnat :: {ord, plus, times}
|
|
|
19 |
|
|
|
20 |
consts
|
|
|
21 |
|
|
|
22 |
pSuc :: pnat => pnat
|
|
|
23 |
"1p" :: pnat ("1p")
|
|
|
24 |
|
|
|
25 |
constdefs
|
|
|
26 |
|
|
|
27 |
pnat_nat :: nat => pnat ("*# _" [80] 80)
|
|
|
28 |
"*# n == Abs_pnat(n + 1)"
|
|
|
29 |
|
|
|
30 |
defs
|
|
|
31 |
|
|
|
32 |
pnat_one_def "1p == Abs_pnat(1)"
|
|
|
33 |
pnat_Suc_def "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
|
|
|
34 |
|
|
|
35 |
|
|
|
36 |
pnat_add_def
|
|
|
37 |
"x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))"
|
|
|
38 |
|
|
|
39 |
pnat_mult_def
|
|
|
40 |
"x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
|
|
|
41 |
|
|
|
42 |
pnat_less_def
|
|
|
43 |
"x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
|
|
|
44 |
|
|
|
45 |
pnat_le_def
|
|
|
46 |
"x <= (y::pnat) == ~(y < x)"
|
|
|
47 |
|
|
|
48 |
end
|
|
|
49 |
|
|
|
50 |
|
|
|
51 |
|
|
|
52 |
|
|
|
53 |
|
|
|
54 |
|
|
|
55 |
|
|
|
56 |
|
|
|
57 |
|
|
|
58 |
|
|
|
59 |
|
|
|
60 |
|
|
|
61 |
|
|
|
62 |
|
|
|
63 |
|
|
|
64 |
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
|
|
|
68 |
|
|
|
69 |
|
|
|
70 |
|
|
|
71 |
|
|
|
72 |
|
|
|
73 |
|