19 begin |
19 begin |
20 |
20 |
21 ML {* @{term "0 \<Colon> int"} *} |
21 ML {* @{term "0 \<Colon> int"} *} |
22 |
22 |
23 quotient_definition |
23 quotient_definition |
24 "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)" |
24 "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" |
25 |
25 |
26 quotient_definition |
26 quotient_definition |
27 "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)" |
27 "1 \<Colon> int" is "(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_definition |
34 quotient_definition |
35 "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw" |
35 "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "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_definition |
42 quotient_definition |
43 "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw" |
43 "(uminus \<Colon> (int \<Rightarrow> int))" is "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_definition |
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)" is "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_definition |
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" is "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 |
67 definition |
67 definition |
205 |
205 |
206 definition int_of_nat_raw: |
206 definition int_of_nat_raw: |
207 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
207 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
208 |
208 |
209 quotient_definition |
209 quotient_definition |
210 "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw" |
210 "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" |
211 |
211 |
212 lemma[quot_respect]: |
212 lemma[quot_respect]: |
213 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
213 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
214 by (simp add: equivp_reflp[OF int_equivp]) |
214 by (simp add: equivp_reflp[OF int_equivp]) |
215 |
215 |