equal
deleted
inserted
replaced
4 Description : The positive naturals |
4 Description : The positive naturals |
5 *) |
5 *) |
6 |
6 |
7 |
7 |
8 PNat = Arith + |
8 PNat = Arith + |
9 |
|
10 (** type pnat **) |
|
11 |
|
12 (* type definition *) |
|
13 |
9 |
14 typedef |
10 typedef |
15 pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def) |
11 pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def) |
16 |
12 |
17 instance |
13 instance |
22 pSuc :: pnat => pnat |
18 pSuc :: pnat => pnat |
23 "1p" :: pnat ("1p") |
19 "1p" :: pnat ("1p") |
24 |
20 |
25 constdefs |
21 constdefs |
26 |
22 |
27 pnat_nat :: nat => pnat ("*# _" [80] 80) |
23 pnat_of_nat :: nat => pnat |
28 "*# n == Abs_pnat(n + 1)" |
24 "pnat_of_nat n == Abs_pnat(n + 1)" |
29 |
25 |
30 defs |
26 defs |
31 |
27 |
32 pnat_one_def "1p == Abs_pnat(1)" |
28 pnat_one_def |
33 pnat_Suc_def "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
29 "1p == Abs_pnat(1)" |
34 |
30 pnat_Suc_def |
|
31 "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
35 |
32 |
36 pnat_add_def |
33 pnat_add_def |
37 "x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |
34 "x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |
38 |
35 |
39 pnat_mult_def |
36 pnat_mult_def |
40 "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))" |
37 "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))" |
41 |
38 |
42 pnat_less_def |
39 pnat_less_def |
43 "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)" |
40 "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)" |
44 |
41 |
45 pnat_le_def |
42 pnat_le_def |
46 "x <= (y::pnat) == ~(y < x)" |
43 "x <= (y::pnat) == ~(y < x)" |
47 |
44 |
48 end |
45 end |
49 |
46 |
50 |
47 |