equal
deleted
inserted
replaced
1 (* Title : PNat.thy |
|
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
|
4 Copyright : 1998 University of Cambridge |
|
5 Description : The positive naturals |
|
6 *) |
|
7 |
|
8 |
|
9 PNat = Main + |
|
10 |
|
11 typedef |
|
12 pnat = "lfp(%X. {Suc 0} Un Suc`X)" (lfp_def) |
|
13 |
|
14 instance |
|
15 pnat :: {ord, one, plus, times} |
|
16 |
|
17 consts |
|
18 |
|
19 pSuc :: pnat => pnat |
|
20 |
|
21 constdefs |
|
22 |
|
23 pnat_of_nat :: nat => pnat |
|
24 "pnat_of_nat n == Abs_pnat(n + 1)" |
|
25 |
|
26 defs |
|
27 |
|
28 pnat_one_def |
|
29 "1 == Abs_pnat(Suc 0)" |
|
30 pnat_Suc_def |
|
31 "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
|
32 |
|
33 pnat_add_def |
|
34 "x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |
|
35 |
|
36 pnat_mult_def |
|
37 "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))" |
|
38 |
|
39 pnat_less_def |
|
40 "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)" |
|
41 |
|
42 pnat_le_def |
|
43 "x <= (y::pnat) == ~(y < x)" |
|
44 |
|
45 end |
|