18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
19 begin |
19 begin |
20 |
20 |
21 ML {* @{term "0 \<Colon> int"} *} |
21 ML {* @{term "0 \<Colon> int"} *} |
22 |
22 |
23 quotient_def |
23 quotient_definition |
24 "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)" |
24 "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)" |
25 |
25 |
26 quotient_def |
26 quotient_definition |
27 "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>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_definition |
35 "(op +) \<Colon> (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_definition |
43 "(uminus \<Colon> (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\<Colon>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)" |
52 |
52 |
53 quotient_def |
53 quotient_definition |
54 mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw" |
54 mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw" |
55 |
55 |
56 fun |
56 fun |
57 le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
57 le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
58 where |
58 where |
59 "le_raw (x, y) (u, v) = (x+v \<le> u+y)" |
59 "le_raw (x, y) (u, v) = (x+v \<le> u+y)" |
60 |
60 |
61 quotient_def |
61 quotient_definition |
62 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw" |
62 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw" |
63 |
63 |
64 definition |
64 definition |
65 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
65 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
66 |
66 |