34 intrel `` {(x + u, y + v)})" .. |
34 intrel `` {(x + u, y + v)})" .. |
35 |
35 |
36 instance int :: minus |
36 instance int :: minus |
37 minus_int_def: |
37 minus_int_def: |
38 "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})" |
38 "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})" |
39 diff_int_def: "z - w \<equiv> z + (-w)" .. |
39 diff_int_def: "z - w \<equiv> z + (-w \<Colon> int)" .. |
40 |
40 |
41 instance int :: times |
41 instance int :: times |
42 mult_int_def: "z * w \<equiv> Abs_Integ |
42 mult_int_def: "z * w \<equiv> Abs_Integ |
43 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w. |
43 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w. |
44 intrel `` {(x*u + y*v, x*v + y*u)})" .. |
44 intrel `` {(x*u + y*v, x*v + y*u)})" .. |
45 |
45 |
46 instance int :: ord |
46 instance int :: ord |
47 le_int_def: |
47 le_int_def: |
48 "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w" |
48 "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w" |
49 less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" .. |
49 less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" .. |
50 |
50 |
51 lemmas [code func del] = Zero_int_def One_int_def add_int_def |
51 lemmas [code func del] = Zero_int_def One_int_def add_int_def |
52 minus_int_def mult_int_def le_int_def less_int_def |
52 minus_int_def mult_int_def le_int_def less_int_def |
53 |
53 |
54 |
54 |
216 zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" .. |
216 zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" .. |
217 instance int :: sgn |
217 instance int :: sgn |
218 zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" .. |
218 zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" .. |
219 |
219 |
220 instance int :: distrib_lattice |
220 instance int :: distrib_lattice |
221 "inf \<equiv> min" |
221 "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min" |
222 "sup \<equiv> max" |
222 "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max" |
223 by intro_classes |
223 by intro_classes |
224 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
224 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
225 |
225 |
226 text{*The integers form an ordered integral domain*} |
226 text{*The integers form an ordered integral domain*} |
227 instance int :: ordered_idom |
227 instance int :: ordered_idom |