1 (* Title: Integ.thy |
1 (* Title: Integ.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 The integers as equivalence classes over nat*nat. |
6 Type "int" is a linear order |
7 *) |
7 *) |
8 |
8 |
9 Integ = Equiv + Arith + |
9 Integ = IntDef + |
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 |
10 |
14 typedef (Integ) |
11 instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) |
15 int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def) |
12 instance int :: linorder (zle_linear) |
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 |
13 |
24 constdefs |
14 constdefs |
25 |
15 zmagnitude :: int => nat |
26 znat :: nat => int ("$# _" [80] 80) |
16 "zmagnitude(Z) == @m. Z = $# m | -Z = $# m" |
27 "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
|
28 |
|
29 znegative :: int => bool |
|
30 "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
|
31 |
|
32 zmagnitude :: int => int |
|
33 "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z). |
|
34 split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" |
|
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 |
|
44 zless_def "Z1<Z2 == znegative(Z1 - Z2)" |
|
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 |
17 |
53 end |
18 end |