16 by (auto simp add: mem_def expand_fun_eq) |
16 by (auto simp add: mem_def expand_fun_eq) |
17 |
17 |
18 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
18 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
19 begin |
19 begin |
20 |
20 |
21 quotient_def |
21 ML {* @{term "0 :: int"} *} |
22 zero_int::"0 :: int" |
22 |
23 where |
23 quotient_def |
24 "(0::nat, 0::nat)" |
24 "0 :: int" as "(0::nat, 0::nat)" |
25 |
25 |
26 quotient_def |
26 quotient_def |
27 one_int::"1 :: int" |
27 "1 :: int" as "(1::nat, 0::nat)" |
28 where |
|
29 "(1::nat, 0::nat)" |
|
30 |
28 |
31 fun |
29 fun |
32 plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
30 plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
33 where |
31 where |
34 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
32 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
35 |
33 |
36 quotient_def |
34 quotient_def |
37 plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" |
35 "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw" |
38 where |
|
39 "plus_raw" |
|
40 |
36 |
41 fun |
37 fun |
42 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
38 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
43 where |
39 where |
44 "uminus_raw (x, y) = (y, x)" |
40 "uminus_raw (x, y) = (y, x)" |
45 |
41 |
46 quotient_def |
42 quotient_def |
47 uminus_int::"(uminus :: (int \<Rightarrow> int))" |
43 "(uminus :: (int \<Rightarrow> int))" as "uminus_raw" |
48 where |
|
49 "uminus_raw" |
|
50 |
44 |
51 definition |
45 definition |
52 minus_int_def [code del]: "z - w = z + (-w::int)" |
46 minus_int_def [code del]: "z - w = z + (-w::int)" |
53 |
47 |
54 fun |
48 fun |
55 times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
49 times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
56 where |
50 where |
57 "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
51 "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
58 |
52 |
59 quotient_def |
53 quotient_def |
60 times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" |
54 "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw" |
61 where |
|
62 "times_raw" |
|
63 |
55 |
64 (* PROBLEM: this should be called le_int and le_raw / or odd *) |
56 (* PROBLEM: this should be called le_int and le_raw / or odd *) |
65 fun |
57 fun |
66 less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
58 less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
67 where |
59 where |
68 "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)" |
60 "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)" |
69 |
61 |
70 quotient_def |
62 quotient_def |
71 less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" |
63 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw" |
72 where |
|
73 "less_eq_raw" |
|
74 |
64 |
75 definition |
65 definition |
76 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
66 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
77 |
67 |
78 definition |
68 definition |
216 |
206 |
217 definition int_of_nat_raw: |
207 definition int_of_nat_raw: |
218 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
208 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
219 |
209 |
220 quotient_def |
210 quotient_def |
221 int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" |
211 "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw" |
222 where "int_of_nat_raw" |
|
223 |
212 |
224 lemma[quot_respect]: |
213 lemma[quot_respect]: |
225 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
214 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
226 by (simp add: equivp_reflp[OF int_equivp]) |
215 by (simp add: equivp_reflp[OF int_equivp]) |
227 |
216 |