| changeset 677 | 35fbace8d48d |
| parent 675 | 94d6d29459c9 |
| child 678 | 569f0e286400 |
| 675:94d6d29459c9 | 677:35fbace8d48d |
|---|---|
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
11 where |
11 where |
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
13 |
13 |
14 quotient int = "nat \<times> nat" / intrel |
14 quotient int = "nat \<times> nat" / intrel |
15 apply(unfold equivp_def) |
15 unfolding equivp_def |
16 apply(auto simp add: mem_def expand_fun_eq) |
16 by (auto simp add: mem_def expand_fun_eq) |
17 done |
|
18 |
17 |
19 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
18 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
20 begin |
19 begin |
21 |
20 |
22 quotient_def |
21 quotient_def |
38 plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" |
37 plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" |
39 where |
38 where |
40 "plus_raw" |
39 "plus_raw" |
41 |
40 |
42 fun |
41 fun |
43 minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
42 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
44 where |
43 where |
45 "minus_raw (x, y) = (y, x)" |
44 "uminus_raw (x, y) = (y, x)" |
46 |
45 |
47 quotient_def |
46 quotient_def |
48 uminus_int::"(uminus :: (int \<Rightarrow> int))" |
47 uminus_int::"(uminus :: (int \<Rightarrow> int))" |
49 where |
48 where |
50 "minus_raw" |
49 "uminus_raw" |
51 |
50 |
52 definition |
51 definition |
53 minus_int_def [code del]: "z - w = z + (-w::int)" |
52 minus_int_def [code del]: "z - w = z + (-w::int)" |
54 |
53 |
55 fun |
54 fun |
60 quotient_def |
59 quotient_def |
61 times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" |
60 times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" |
62 where |
61 where |
63 "times_raw" |
62 "times_raw" |
64 |
63 |
64 (* PROBLEM: this should be called le_int and le_raw / or odd *) |
|
65 fun |
65 fun |
66 less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
66 less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
67 where |
67 where |
68 "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)" |
68 "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)" |
69 |
69 |
88 lemma plus_raw_rsp[quot_respect]: |
88 lemma plus_raw_rsp[quot_respect]: |
89 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
89 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
90 by auto |
90 by auto |
91 |
91 |
92 lemma minus_raw_rsp[quot_respect]: |
92 lemma minus_raw_rsp[quot_respect]: |
93 shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw" |
93 shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw" |
94 by auto |
94 by auto |
95 |
95 |
96 lemma times_raw_fst: |
96 lemma times_raw_fst: |
97 assumes a: "x \<approx> z" |
97 assumes a: "x \<approx> z" |
98 shows "times_raw x y \<approx> times_raw z y" |
98 shows "times_raw x y \<approx> times_raw z y" |
115 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
115 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
116 apply(simp add: mult_ac) |
116 apply(simp add: mult_ac) |
117 apply(simp add: add_mult_distrib [symmetric]) |
117 apply(simp add: add_mult_distrib [symmetric]) |
118 done |
118 done |
119 |
119 |
120 lemma mult_raw_rsp[quot_respect]: |
120 lemma times_raw_rsp[quot_respect]: |
121 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw" |
121 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw" |
122 apply(simp only: fun_rel.simps) |
122 apply(simp only: fun_rel.simps) |
123 apply(rule allI | rule impI)+ |
123 apply(rule allI | rule impI)+ |
124 apply(rule equivp_transp[OF int_equivp]) |
124 apply(rule equivp_transp[OF int_equivp]) |
125 apply(rule times_raw_fst) |
125 apply(rule times_raw_fst) |
143 lemma plus_zero_raw: |
143 lemma plus_zero_raw: |
144 shows "plus_raw (0, 0) i \<approx> i" |
144 shows "plus_raw (0, 0) i \<approx> i" |
145 by (cases i) (simp) |
145 by (cases i) (simp) |
146 |
146 |
147 lemma plus_minus_zero_raw: |
147 lemma plus_minus_zero_raw: |
148 shows "plus_raw (minus_raw i) i \<approx> (0, 0)" |
148 shows "plus_raw (uminus_raw i) i \<approx> (0, 0)" |
149 by (cases i) (simp) |
149 by (cases i) (simp) |
150 |
150 |
151 lemma times_assoc_raw: |
151 lemma times_assoc_raw: |
152 shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)" |
152 shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)" |
153 by (cases i, cases j, cases k) |
153 by (cases i, cases j, cases k) |