33 zpred,zsuc :: "int=>int" |
33 zpred,zsuc :: "int=>int" |
34 |
34 |
35 defs |
35 defs |
36 zNat_def "zNat == {x::nat. True}" |
36 zNat_def "zNat == {x::nat. True}" |
37 |
37 |
38 znat_def "$# m == Abs_Integ(intrel ^^ {<m,0>})" |
38 znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})" |
39 |
39 |
40 zminus_def |
40 zminus_def |
41 "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{<y,x>}) p)" |
41 "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" |
42 |
42 |
43 znegative_def |
43 znegative_def |
44 "znegative(Z) == EX x y. x<y & <x,y::nat>:Rep_Integ(Z)" |
44 "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)" |
45 |
45 |
46 zmagnitude_def |
46 zmagnitude_def |
47 "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{<(y-x) + (x-y),0>}) p)" |
47 "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" |
48 |
48 |
49 zadd_def |
49 zadd_def |
50 "Z1 + Z2 == \ |
50 "Z1 + Z2 == \ |
51 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \ |
51 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \ |
52 \ split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)" |
52 \ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
53 |
53 |
54 zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" |
54 zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" |
55 |
55 |
56 zless_def "Z1<Z2 == znegative(Z1 - Z2)" |
56 zless_def "Z1<Z2 == znegative(Z1 - Z2)" |
57 |
57 |
58 zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)" |
58 zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)" |
59 |
59 |
60 zmult_def |
60 zmult_def |
61 "Z1 * Z2 == \ |
61 "Z1 * Z2 == \ |
62 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
62 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
63 \ split (%x2 y2. intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)" |
63 \ split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
64 |
64 |
65 zdiv_def |
65 zdiv_def |
66 "Z1 zdiv Z2 == \ |
66 "Z1 zdiv Z2 == \ |
67 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
67 \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ |
68 \ split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \ |
68 \ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \ |
69 \ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)" |
69 \ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)" |
70 |
70 |
71 zmod_def |
71 zmod_def |
72 "Z1 zmod Z2 == \ |
72 "Z1 zmod Z2 == \ |
73 \ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \ |
73 \ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \ |
74 \ split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)), \ |
74 \ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), \ |
75 \ (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)" |
75 \ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)" |
76 |
76 |
77 zsuc_def "zsuc(Z) == Z + $# Suc(0)" |
77 zsuc_def "zsuc(Z) == Z + $# Suc(0)" |
78 |
78 |
79 zpred_def "zpred(Z) == Z - $# Suc(0)" |
79 zpred_def "zpred(Z) == Z - $# Suc(0)" |
80 end |
80 end |