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 ML {* @{term "0 :: int"} *} |
21 ML {* @{term "0 \<Colon> int"} *} |
22 |
22 |
23 quotient_def |
23 quotient_def |
24 "0 :: int" as "(0::nat, 0::nat)" |
24 "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)" |
25 |
25 |
26 quotient_def |
26 quotient_def |
27 "1 :: int" as "(1::nat, 0::nat)" |
27 "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)" |
28 |
28 |
29 fun |
29 fun |
30 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)" |
31 where |
31 where |
32 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
32 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
33 |
33 |
34 quotient_def |
34 quotient_def |
35 "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw" |
35 "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw" |
36 |
36 |
37 fun |
37 fun |
38 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
38 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
39 where |
39 where |
40 "uminus_raw (x, y) = (y, x)" |
40 "uminus_raw (x, y) = (y, x)" |
41 |
41 |
42 quotient_def |
42 quotient_def |
43 "(uminus :: (int \<Rightarrow> int))" as "uminus_raw" |
43 "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw" |
44 |
44 |
45 definition |
45 definition |
46 minus_int_def [code del]: "z - w = z + (-w::int)" |
46 minus_int_def [code del]: "z - w = z + (-w\<Colon>int)" |
47 |
47 |
48 fun |
48 fun |
49 mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
49 mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
50 where |
50 where |
51 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
51 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
322 proof |
322 proof |
323 fix i j k :: int |
323 fix i j k :: int |
324 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
324 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
325 by (rule zmult_zless_mono2) |
325 by (rule zmult_zless_mono2) |
326 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
326 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
327 by (simp only: abs_int_def) |
327 by (simp only: zabs_def) |
328 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
328 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
329 by (simp only: sgn_int_def) |
329 by (simp only: zsgn_def) |
330 qed |
330 qed |
331 |
331 |
332 instance int :: lordered_ring |
332 instance int :: lordered_ring |
333 proof |
333 proof |
334 fix k :: int |
334 fix k :: int |
335 show "abs k = sup k (- k)" |
335 show "abs k = sup k (- k)" |
336 by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric]) |
336 by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric]) |
337 qed |
337 qed |
338 |
338 |
339 lemmas int_distrib = |
339 lemmas int_distrib = |
340 left_distrib [of "z1::int" "z2" "w", standard] |
340 left_distrib [of "z1::int" "z2" "w", standard] |
341 right_distrib [of "w::int" "z1" "z2", standard] |
341 right_distrib [of "w::int" "z1" "z2", standard] |