14 by (auto simp add: equivp_def expand_fun_eq) |
14 by (auto simp add: equivp_def expand_fun_eq) |
15 |
15 |
16 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}" |
16 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}" |
17 begin |
17 begin |
18 |
18 |
19 quotient_def |
19 quotient_definition |
20 Zero_int_def: "0::int" as "(0::nat, 0::nat)" |
20 Zero_int_def: "0::int" as "(0::nat, 0::nat)" |
21 |
21 |
22 quotient_def |
22 quotient_definition |
23 One_int_def: "1::int" as "(1::nat, 0::nat)" |
23 One_int_def: "1::int" as "(1::nat, 0::nat)" |
24 |
24 |
25 definition |
25 definition |
26 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))" |
26 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))" |
27 |
27 |
28 quotient_def |
28 quotient_definition |
29 "(op +) :: int \<Rightarrow> int \<Rightarrow> int" |
29 "(op +) :: int \<Rightarrow> int \<Rightarrow> int" |
30 as |
30 as |
31 "add_raw" |
31 "add_raw" |
32 |
32 |
33 definition |
33 definition |
34 "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)" |
34 "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)" |
35 |
35 |
36 quotient_def |
36 quotient_definition |
37 "uminus :: int \<Rightarrow> int" |
37 "uminus :: int \<Rightarrow> int" |
38 as |
38 as |
39 "uminus_raw" |
39 "uminus_raw" |
40 |
40 |
41 fun |
41 fun |
42 mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" |
42 mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" |
43 where |
43 where |
44 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
44 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
45 |
45 |
46 quotient_def |
46 quotient_definition |
47 "(op *) :: int \<Rightarrow> int \<Rightarrow> int" |
47 "(op *) :: int \<Rightarrow> int \<Rightarrow> int" |
48 as |
48 as |
49 "mult_raw" |
49 "mult_raw" |
50 |
50 |
51 definition |
51 definition |
52 "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))" |
52 "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))" |
53 |
53 |
54 quotient_def |
54 quotient_definition |
55 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" |
55 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" |
56 as |
56 as |
57 "le_raw" |
57 "le_raw" |
58 |
58 |
59 definition |
59 definition |