author | clasohm |
Mon, 05 Feb 1996 21:29:06 +0100 | |
changeset 1476 | 608483c2122a |
parent 1374 | 5e407f2a3323 |
child 1559 | 9ba0906aa60d |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: Integ.thy |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
1476 | 3 |
Authors: Riccardo Mattolini, Dip. Sistemi e Informatica |
4 |
Lawrence C Paulson, Cambridge University Computer Laboratory |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
Copyright 1994 Universita' di Firenze |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
Copyright 1993 University of Cambridge |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
The integers as equivalence classes over nat*nat. |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
9 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
Integ = Equiv + Arith + |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
consts |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
13 |
intrel :: "((nat * nat) * (nat * nat)) set" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
14 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
15 |
defs |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
16 |
intrel_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
17 |
"intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
|
1476 | 19 |
typedef (Integ) |
20 |
int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def) |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
21 |
|
994 | 22 |
instance |
23 |
int :: {ord, plus, times, minus} |
|
24 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
25 |
consts |
1374 | 26 |
zNat :: nat set |
1476 | 27 |
znat :: nat => int ("$# _" [80] 80) |
28 |
zminus :: int => int ("$~ _" [80] 80) |
|
1374 | 29 |
znegative :: int => bool |
30 |
zmagnitude :: int => int |
|
31 |
zdiv,zmod :: [int,int]=>int (infixl 70) |
|
32 |
zpred,zsuc :: int=>int |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
33 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
34 |
defs |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
zNat_def "zNat == {x::nat. True}" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
36 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
37 |
znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
38 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
39 |
zminus_def |
1476 | 40 |
"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
41 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
42 |
znegative_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
43 |
"znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
44 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
45 |
zmagnitude_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
46 |
"zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
47 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
48 |
zadd_def |
1151 | 49 |
"Z1 + Z2 == |
50 |
Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). |
|
51 |
split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
52 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
53 |
zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
55 |
zless_def "Z1<Z2 == znegative(Z1 - Z2)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
56 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
57 |
zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
58 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
59 |
zmult_def |
1151 | 60 |
"Z1 * Z2 == |
61 |
Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. |
|
62 |
split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
63 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
64 |
zdiv_def |
1151 | 65 |
"Z1 zdiv Z2 == |
66 |
Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. |
|
67 |
split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), |
|
68 |
(x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
69 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
70 |
zmod_def |
1151 | 71 |
"Z1 zmod Z2 == |
72 |
Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. |
|
73 |
split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), |
|
74 |
(x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
75 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
76 |
zsuc_def "zsuc(Z) == Z + $# Suc(0)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
77 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
78 |
zpred_def "zpred(Z) == Z - $# Suc(0)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
79 |
end |