author | paulson |
Thu, 15 Jul 1999 10:34:37 +0200 | |
changeset 7010 | 63120b6dca50 |
parent 5594 | e4439230af67 |
child 7127 | 48e235179ffb |
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 |
|
5594 | 38 |
"z + w == |
39 |
Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). |
|
5508 | 40 |
split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
41 |
||
5594 | 42 |
zdiff_def "z - w == z + -(w::int)" |
5508 | 43 |
|
5594 | 44 |
zless_def "z<w == neg(z - w)" |
5508 | 45 |
|
5594 | 46 |
zle_def "z <= (w::int) == ~(w < z)" |
5508 | 47 |
|
48 |
zmult_def |
|
5594 | 49 |
"z * w == |
50 |
Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). split (%x1 y1. |
|
5508 | 51 |
split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
52 |
||
53 |
end |