7 |
7 |
8 The integers as equivalence classes over nat*nat. |
8 The integers as equivalence classes over nat*nat. |
9 *) |
9 *) |
10 |
10 |
11 Integ = Equiv + Arith + |
11 Integ = Equiv + Arith + |
12 consts |
12 constdefs |
13 intrel :: "((nat * nat) * (nat * nat)) set" |
13 intrel :: "((nat * nat) * (nat * nat)) set" |
14 |
14 "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
15 defs |
|
16 intrel_def |
|
17 "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
|
18 |
15 |
19 typedef (Integ) |
16 typedef (Integ) |
20 int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def) |
17 int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def) |
21 |
18 |
22 instance |
19 instance |
23 int :: {ord, plus, times, minus} |
20 int :: {ord, plus, times, minus} |
24 |
21 |
25 consts |
22 constdefs |
|
23 |
26 zNat :: nat set |
24 zNat :: nat set |
27 znat :: nat => int ("$# _" [80] 80) |
25 "zNat == {x::nat. True}" |
28 zminus :: int => int ("$~ _" [80] 80) |
26 |
|
27 znat :: nat => int ("$# _" [80] 80) |
|
28 "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
|
29 |
|
30 zminus :: int => int ("$~ _" [80] 80) |
|
31 "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" |
|
32 |
29 znegative :: int => bool |
33 znegative :: int => bool |
|
34 "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
|
35 |
30 zmagnitude :: int => int |
36 zmagnitude :: int => int |
31 zdiv,zmod :: [int,int]=>int (infixl 70) |
37 "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z). |
32 zpred,zsuc :: int=>int |
38 split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" |
|
39 |
|
40 zdiv :: [int,int]=>int (infixl 70) |
|
41 "Z1 zdiv Z2 == |
|
42 Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. |
|
43 split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), |
|
44 (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)" |
|
45 |
|
46 zmod :: [int,int]=>int (infixl 70) |
|
47 "Z1 zmod Z2 == |
|
48 Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. |
|
49 split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), |
|
50 (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)" |
|
51 |
|
52 zpred :: int=>int |
|
53 "zpred(Z) == Z - $# Suc(0)" |
|
54 |
|
55 zsuc :: int=>int |
|
56 "zsuc(Z) == Z + $# Suc(0)" |
33 |
57 |
34 defs |
58 defs |
35 zNat_def "zNat == {x::nat. True}" |
|
36 |
|
37 znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
|
38 |
|
39 zminus_def |
|
40 "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" |
|
41 |
|
42 znegative_def |
|
43 "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
|
44 |
|
45 zmagnitude_def |
|
46 "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" |
|
47 |
|
48 zadd_def |
59 zadd_def |
49 "Z1 + Z2 == |
60 "Z1 + Z2 == |
50 Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). |
61 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)" |
62 split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
52 |
63 |
59 zmult_def |
70 zmult_def |
60 "Z1 * Z2 == |
71 "Z1 * Z2 == |
61 Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. |
72 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)" |
73 split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
63 |
74 |
64 zdiv_def |
|
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)" |
|
69 |
|
70 zmod_def |
|
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)" |
|
75 |
|
76 zsuc_def "zsuc(Z) == Z + $# Suc(0)" |
|
77 |
|
78 zpred_def "zpred(Z) == Z - $# Suc(0)" |
|
79 end |
75 end |