| author | wenzelm |
| Fri, 05 Oct 2001 21:52:39 +0200 | |
| changeset 11701 | 3d51fbf81c17 |
| parent 11464 | ddea204de5bc |
| child 12018 | ec054019c910 |
| permissions | -rw-r--r-- |
| paulson@5078 | 1 |
(* Title : PNat.thy |
| paulson@7219 | 2 |
ID : $Id$ |
| paulson@5078 | 3 |
Author : Jacques D. Fleuriot |
| paulson@5078 | 4 |
Copyright : 1998 University of Cambridge |
| paulson@5078 | 5 |
Description : The positive naturals |
| paulson@5078 | 6 |
*) |
| paulson@5078 | 7 |
|
| paulson@5078 | 8 |
|
| wenzelm@8856 | 9 |
PNat = Main + |
| paulson@5078 | 10 |
|
| paulson@5078 | 11 |
typedef |
| wenzelm@11701 | 12 |
pnat = "lfp(%X. {Suc 0} Un Suc`X)" (lfp_def)
|
| paulson@5078 | 13 |
|
| paulson@5078 | 14 |
instance |
| paulson@5078 | 15 |
pnat :: {ord, plus, times}
|
| paulson@5078 | 16 |
|
| paulson@5078 | 17 |
consts |
| paulson@5078 | 18 |
|
| paulson@5078 | 19 |
pSuc :: pnat => pnat |
| paulson@5078 | 20 |
"1p" :: pnat ("1p")
|
| paulson@5078 | 21 |
|
| paulson@5078 | 22 |
constdefs |
| paulson@5078 | 23 |
|
| paulson@7077 | 24 |
pnat_of_nat :: nat => pnat |
| paulson@7077 | 25 |
"pnat_of_nat n == Abs_pnat(n + 1)" |
| paulson@5078 | 26 |
|
| paulson@5078 | 27 |
defs |
| paulson@5078 | 28 |
|
| paulson@7077 | 29 |
pnat_one_def |
| wenzelm@11701 | 30 |
"1p == Abs_pnat(Suc 0)" |
| paulson@7077 | 31 |
pnat_Suc_def |
| paulson@7077 | 32 |
"pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))" |
| paulson@5078 | 33 |
|
| paulson@5078 | 34 |
pnat_add_def |
| paulson@5078 | 35 |
"x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))" |
| paulson@5078 | 36 |
|
| paulson@5078 | 37 |
pnat_mult_def |
| paulson@5078 | 38 |
"x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))" |
| paulson@5078 | 39 |
|
| paulson@7077 | 40 |
pnat_less_def |
| paulson@5078 | 41 |
"x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)" |
| paulson@5078 | 42 |
|
| paulson@7077 | 43 |
pnat_le_def |
| paulson@5078 | 44 |
"x <= (y::pnat) == ~(y < x)" |
| paulson@5078 | 45 |
|
| paulson@5078 | 46 |
end |