author | clasohm |
Fri, 24 Mar 1995 12:30:35 +0100 | |
changeset 972 | e61b058d58d2 |
parent 925 | 15539deb6863 |
child 994 | b5e3fa9664fe |
permissions | -rw-r--r-- |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: Integ.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
3 |
Authors: Riccardo Mattolini, Dip. Sistemi e Informatica |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
4 |
Lawrence C Paulson, Cambridge University Computer Laboratory |
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 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
19 |
subtype (Integ) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
20 |
int = "{x::(nat*nat).True}/intrel" ("quotient_def") |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
21 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
22 |
arities int :: ord |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
23 |
int :: plus |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
24 |
int :: times |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
25 |
int :: minus |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
26 |
consts |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
zNat :: "nat set" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
znat :: "nat => int" ("$# _" [80] 80) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
29 |
zminus :: "int => int" ("$~ _" [80] 80) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
30 |
znegative :: "int => bool" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
31 |
zmagnitude :: "int => int" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
32 |
zdiv,zmod :: "[int,int]=>int" (infixl 70) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
33 |
zpred,zsuc :: "int=>int" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
34 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
defs |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
36 |
zNat_def "zNat == {x::nat. True}" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
37 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
38 |
znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
39 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
40 |
zminus_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
41 |
"$~ 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
|
42 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
43 |
znegative_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
44 |
"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
|
45 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
46 |
zmagnitude_def |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
47 |
"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
|
48 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
49 |
zadd_def |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
50 |
"Z1 + Z2 == \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
51 |
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
52 |
\ 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
|
53 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
55 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
56 |
zless_def "Z1<Z2 == znegative(Z1 - Z2)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
57 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
58 |
zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
59 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
60 |
zmult_def |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
61 |
"Z1 * Z2 == \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
62 |
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
63 |
\ 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
|
64 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
65 |
zdiv_def |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
66 |
"Z1 zdiv Z2 == \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
67 |
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
68 |
\ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
69 |
\ (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
|
70 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
71 |
zmod_def |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
72 |
"Z1 zmod Z2 == \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
73 |
\ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
74 |
\ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
75 |
\ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
76 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
77 |
zsuc_def "zsuc(Z) == Z + $# Suc(0)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
78 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
79 |
zpred_def "zpred(Z) == Z - $# Suc(0)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
80 |
end |