author | paulson |
Tue, 29 Sep 1998 15:57:42 +0200 | |
changeset 5582 | a356fb49e69e |
parent 5562 | 02261e6880d1 |
child 5594 | e4439230af67 |
permissions | -rw-r--r-- |
5508 | 1 |
(* Title: IntDef.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
The integers as equivalence classes over nat*nat. |
|
7 |
*) |
|
8 |
||
9 |
IntDef = Equiv + Arith + |
|
10 |
constdefs |
|
11 |
intrel :: "((nat * nat) * (nat * nat)) set" |
|
12 |
"intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
|
13 |
||
14 |
typedef (Integ) |
|
15 |
int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def) |
|
16 |
||
17 |
instance |
|
18 |
int :: {ord, plus, times, minus} |
|
19 |
||
20 |
defs |
|
21 |
zminus_def |
|
22 |
"- Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" |
|
23 |
||
24 |
constdefs |
|
25 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
26 |
int :: nat => int |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
27 |
"int m == Abs_Integ(intrel ^^ {(m,0)})" |
5508 | 28 |
|
5540 | 29 |
neg :: int => bool |
30 |
"neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
|
5508 | 31 |
|
32 |
(*For simplifying equalities*) |
|
33 |
iszero :: int => bool |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
34 |
"iszero z == z = int 0" |
5508 | 35 |
|
36 |
defs |
|
37 |
zadd_def |
|
38 |
"Z1 + Z2 == |
|
39 |
Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). |
|
40 |
split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
|
41 |
||
42 |
zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)" |
|
43 |
||
5540 | 44 |
zless_def "Z1<Z2 == neg(Z1 - Z2)" |
5508 | 45 |
|
46 |
zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)" |
|
47 |
||
48 |
zmult_def |
|
49 |
"Z1 * Z2 == |
|
50 |
Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. |
|
51 |
split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
|
52 |
||
53 |
end |