73 definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where |
73 definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where |
74 "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" |
74 "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" |
75 |
75 |
76 code_datatype Fract |
76 code_datatype Fract |
77 |
77 |
78 lemma Fract_cases [case_names Fract, cases type: fract]: |
78 lemma Fract_cases [cases type: fract]: |
79 assumes "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> C" |
79 obtains (Fract) a b where "q = Fract a b" "b \<noteq> 0" |
80 shows C |
80 by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) |
81 using assms by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) |
|
82 |
81 |
83 lemma Fract_induct [case_names Fract, induct type: fract]: |
82 lemma Fract_induct [case_names Fract, induct type: fract]: |
84 assumes "\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)" |
83 shows "(\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)) \<Longrightarrow> P q" |
85 shows "P q" |
84 by (cases q) simp |
86 using assms by (cases q) simp |
|
87 |
85 |
88 lemma eq_fract: |
86 lemma eq_fract: |
89 shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
87 shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
90 and "\<And>a. Fract a 0 = Fract 0 1" |
88 and "\<And>a. Fract a 0 = Fract 0 1" |
91 and "\<And>a c. Fract 0 a = Fract 0 c" |
89 and "\<And>a c. Fract 0 a = Fract 0 c" |
92 by (simp_all add: Fract_def) |
90 by (simp_all add: Fract_def) |
93 |
91 |
94 instantiation fract :: (idom) "{comm_ring_1, power}" |
92 instantiation fract :: (idom) "{comm_ring_1,power}" |
95 begin |
93 begin |
96 |
94 |
97 definition Zero_fract_def [code_unfold]: "0 = Fract 0 1" |
95 definition Zero_fract_def [code_unfold]: "0 = Fract 0 1" |
98 |
96 |
99 definition One_fract_def [code_unfold]: "1 = Fract 1 1" |
97 definition One_fract_def [code_unfold]: "1 = Fract 1 1" |
101 definition add_fract_def: |
99 definition add_fract_def: |
102 "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
100 "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
103 fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" |
101 fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" |
104 |
102 |
105 lemma add_fract [simp]: |
103 lemma add_fract [simp]: |
106 assumes "b \<noteq> (0::'a::idom)" and "d \<noteq> 0" |
104 assumes "b \<noteq> (0::'a::idom)" |
|
105 and "d \<noteq> 0" |
107 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
106 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
108 proof - |
107 proof - |
109 have "(\<lambda>x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) |
108 have "(\<lambda>x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) |
110 respects2 fractrel" |
109 respects2 fractrel" |
111 apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps) |
110 apply (rule equiv_fractrel [THEN congruent2_commuteI]) |
112 unfolding mult_assoc[symmetric] . |
111 apply (auto simp add: algebra_simps) |
|
112 unfolding mult_assoc[symmetric] |
|
113 done |
113 with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) |
114 with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) |
114 qed |
115 qed |
115 |
116 |
116 definition minus_fract_def: |
117 definition minus_fract_def: |
117 "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})" |
118 "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})" |
138 fractrel``{(fst x * fst y, snd x * snd y)})" |
139 fractrel``{(fst x * fst y, snd x * snd y)})" |
139 |
140 |
140 lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)" |
141 lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)" |
141 proof - |
142 proof - |
142 have "(\<lambda>x y. fractrel `` {(fst x * fst y, snd x * snd y :: 'a)}) respects2 fractrel" |
143 have "(\<lambda>x y. fractrel `` {(fst x * fst y, snd x * snd y :: 'a)}) respects2 fractrel" |
143 apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps) |
144 apply (rule equiv_fractrel [THEN congruent2_commuteI]) |
144 unfolding mult_assoc[symmetric] . |
145 apply (auto simp add: algebra_simps) |
|
146 done |
145 then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) |
147 then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) |
146 qed |
148 qed |
147 |
149 |
148 lemma mult_fract_cancel: |
150 lemma mult_fract_cancel: |
149 assumes "c \<noteq> (0::'a)" |
151 assumes "c \<noteq> (0::'a)" |
153 then show ?thesis by (simp add: mult_fract [symmetric]) |
155 then show ?thesis by (simp add: mult_fract [symmetric]) |
154 qed |
156 qed |
155 |
157 |
156 instance |
158 instance |
157 proof |
159 proof |
158 fix q r s :: "'a fract" show "(q * r) * s = q * (r * s)" |
160 fix q r s :: "'a fract" |
|
161 show "(q * r) * s = q * (r * s)" |
159 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
162 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
160 next |
163 show "q * r = r * q" |
161 fix q r :: "'a fract" show "q * r = r * q" |
|
162 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
164 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
163 next |
165 show "1 * q = q" |
164 fix q :: "'a fract" show "1 * q = q" |
|
165 by (cases q) (simp add: One_fract_def eq_fract) |
166 by (cases q) (simp add: One_fract_def eq_fract) |
166 next |
167 show "(q + r) + s = q + (r + s)" |
167 fix q r s :: "'a fract" show "(q + r) + s = q + (r + s)" |
|
168 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
168 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
169 next |
169 show "q + r = r + q" |
170 fix q r :: "'a fract" show "q + r = r + q" |
|
171 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
170 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
172 next |
171 show "0 + q = q" |
173 fix q :: "'a fract" show "0 + q = q" |
|
174 by (cases q) (simp add: Zero_fract_def eq_fract) |
172 by (cases q) (simp add: Zero_fract_def eq_fract) |
175 next |
173 show "- q + q = 0" |
176 fix q :: "'a fract" show "- q + q = 0" |
|
177 by (cases q) (simp add: Zero_fract_def eq_fract) |
174 by (cases q) (simp add: Zero_fract_def eq_fract) |
178 next |
175 show "q - r = q + - r" |
179 fix q r :: "'a fract" show "q - r = q + - r" |
|
180 by (cases q, cases r) (simp add: eq_fract) |
176 by (cases q, cases r) (simp add: eq_fract) |
181 next |
177 show "(q + r) * s = q * s + r * s" |
182 fix q r s :: "'a fract" show "(q + r) * s = q * s + r * s" |
|
183 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
178 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
184 next |
179 show "(0::'a fract) \<noteq> 1" |
185 show "(0::'a fract) \<noteq> 1" by (simp add: Zero_fract_def One_fract_def eq_fract) |
180 by (simp add: Zero_fract_def One_fract_def eq_fract) |
186 qed |
181 qed |
187 |
182 |
188 end |
183 end |
189 |
184 |
190 lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1" |
185 lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1" |
203 lemma fract_expand [code_unfold]: |
198 lemma fract_expand [code_unfold]: |
204 "0 = Fract 0 1" |
199 "0 = Fract 0 1" |
205 "1 = Fract 1 1" |
200 "1 = Fract 1 1" |
206 by (simp_all add: fract_collapse) |
201 by (simp_all add: fract_collapse) |
207 |
202 |
208 lemma Fract_cases_nonzero [case_names Fract 0]: |
203 lemma Fract_cases_nonzero: |
209 assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> C" |
204 obtains (Fract) a b where "q = Fract a b" "b \<noteq> 0" "a \<noteq> 0" |
210 assumes 0: "q = 0 \<Longrightarrow> C" |
205 | (0) "q = 0" |
211 shows C |
|
212 proof (cases "q = 0") |
206 proof (cases "q = 0") |
213 case True then show C using 0 by auto |
207 case True |
|
208 then show thesis using 0 by auto |
214 next |
209 next |
215 case False |
210 case False |
216 then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto |
211 then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto |
217 moreover with False have "0 \<noteq> Fract a b" by simp |
212 moreover with False have "0 \<noteq> Fract a b" by simp |
218 with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract) |
213 with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract) |
219 with Fract `q = Fract a b` `b \<noteq> 0` show C by auto |
214 with Fract `q = Fract a b` `b \<noteq> 0` show thesis by auto |
220 qed |
215 qed |
221 |
216 |
222 |
|
223 |
217 |
224 subsubsection {* The field of rational numbers *} |
218 subsubsection {* The field of rational numbers *} |
225 |
219 |
226 context idom |
220 context idom |
227 begin |
221 begin |
|
222 |
228 subclass ring_no_zero_divisors .. |
223 subclass ring_no_zero_divisors .. |
229 thm mult_eq_0_iff |
224 |
230 end |
225 end |
231 |
226 |
232 instantiation fract :: (idom) field_inverse_zero |
227 instantiation fract :: (idom) field_inverse_zero |
233 begin |
228 begin |
234 |
229 |
235 definition inverse_fract_def: |
230 definition inverse_fract_def: |
236 "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q. |
231 "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q. |
237 fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" |
232 fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" |
238 |
233 |
239 |
|
240 lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a" |
234 lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a" |
241 proof - |
235 proof - |
242 have stupid: "\<And>x. (0::'a) = x \<longleftrightarrow> x = 0" by auto |
236 have *: "\<And>x. (0::'a) = x \<longleftrightarrow> x = 0" by auto |
243 have "(\<lambda>x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" |
237 have "(\<lambda>x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" |
244 by (auto simp add: congruent_def stupid algebra_simps) |
238 by (auto simp add: congruent_def * algebra_simps) |
245 then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel) |
239 then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel) |
246 qed |
240 qed |
247 |
241 |
248 definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)" |
242 definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)" |
249 |
243 |
313 |
307 |
314 instantiation fract :: (linordered_idom) linorder |
308 instantiation fract :: (linordered_idom) linorder |
315 begin |
309 begin |
316 |
310 |
317 definition le_fract_def: |
311 definition le_fract_def: |
318 "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
312 "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
319 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})" |
313 {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" |
320 |
314 |
321 definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
315 definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
322 |
316 |
323 lemma le_fract [simp]: |
317 lemma le_fract [simp]: |
324 assumes "b \<noteq> 0" and "d \<noteq> 0" |
318 assumes "b \<noteq> 0" and "d \<noteq> 0" |
325 shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
319 shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
326 by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) |
320 by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) |
327 |
321 |
328 lemma less_fract [simp]: |
322 lemma less_fract [simp]: |
329 assumes "b \<noteq> 0" and "d \<noteq> 0" |
323 assumes "b \<noteq> 0" and "d \<noteq> 0" |
330 shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
324 shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
331 by (simp add: less_fract_def less_le_not_le mult_ac assms) |
325 by (simp add: less_fract_def less_le_not_le mult_ac assms) |
332 |
326 |
333 instance |
327 instance |
334 proof |
328 proof |
335 fix q r s :: "'a fract" |
329 fix q r s :: "'a fract" |
336 assume "q \<le> r" and "r \<le> s" thus "q \<le> s" |
330 assume "q \<le> r" and "r \<le> s" thus "q \<le> s" |
425 end |
419 end |
426 |
420 |
427 instance fract :: (linordered_idom) linordered_field_inverse_zero |
421 instance fract :: (linordered_idom) linordered_field_inverse_zero |
428 proof |
422 proof |
429 fix q r s :: "'a fract" |
423 fix q r s :: "'a fract" |
430 show "q \<le> r ==> s + q \<le> s + r" |
424 assume "q \<le> r" |
|
425 then show "s + q \<le> s + r" |
431 proof (induct q, induct r, induct s) |
426 proof (induct q, induct r, induct s) |
432 fix a b c d e f :: 'a |
427 fix a b c d e f :: 'a |
433 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
428 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
434 assume le: "Fract a b \<le> Fract c d" |
429 assume le: "Fract a b \<le> Fract c d" |
435 show "Fract e f + Fract a b \<le> Fract e f + Fract c d" |
430 show "Fract e f + Fract a b \<le> Fract e f + Fract c d" |
436 proof - |
431 proof - |
437 let ?F = "f * f" from neq have F: "0 < ?F" |
432 let ?F = "f * f" from neq have F: "0 < ?F" |
438 by (auto simp add: zero_less_mult_iff) |
433 by (auto simp add: zero_less_mult_iff) |
441 with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" |
436 with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" |
442 by (simp add: mult_le_cancel_right) |
437 by (simp add: mult_le_cancel_right) |
443 with neq show ?thesis by (simp add: field_simps) |
438 with neq show ?thesis by (simp add: field_simps) |
444 qed |
439 qed |
445 qed |
440 qed |
446 show "q < r ==> 0 < s ==> s * q < s * r" |
441 next |
|
442 fix q r s :: "'a fract" |
|
443 assume "q < r" and "0 < s" |
|
444 then show "s * q < s * r" |
447 proof (induct q, induct r, induct s) |
445 proof (induct q, induct r, induct s) |
448 fix a b c d e f :: 'a |
446 fix a b c d e f :: 'a |
449 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
447 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
450 assume le: "Fract a b < Fract c d" |
448 assume le: "Fract a b < Fract c d" |
451 assume gt: "0 < Fract e f" |
449 assume gt: "0 < Fract e f" |
481 qed |
479 qed |
482 case (Fract a b) |
480 case (Fract a b) |
483 thus "P q" by (force simp add: linorder_neq_iff step step') |
481 thus "P q" by (force simp add: linorder_neq_iff step step') |
484 qed |
482 qed |
485 |
483 |
486 lemma zero_less_Fract_iff: |
484 lemma zero_less_Fract_iff: "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
487 "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
|
488 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
485 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
489 |
486 |
490 lemma Fract_less_zero_iff: |
487 lemma Fract_less_zero_iff: "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
491 "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
|
492 by (auto simp add: Zero_fract_def mult_less_0_iff) |
488 by (auto simp add: Zero_fract_def mult_less_0_iff) |
493 |
489 |
494 lemma zero_le_Fract_iff: |
490 lemma zero_le_Fract_iff: "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
495 "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
|
496 by (auto simp add: Zero_fract_def zero_le_mult_iff) |
491 by (auto simp add: Zero_fract_def zero_le_mult_iff) |
497 |
492 |
498 lemma Fract_le_zero_iff: |
493 lemma Fract_le_zero_iff: "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
499 "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
500 by (auto simp add: Zero_fract_def mult_le_0_iff) |
494 by (auto simp add: Zero_fract_def mult_le_0_iff) |
501 |
495 |
502 lemma one_less_Fract_iff: |
496 lemma one_less_Fract_iff: "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
503 "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
|
504 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
497 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
505 |
498 |
506 lemma Fract_less_one_iff: |
499 lemma Fract_less_one_iff: "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
507 "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
|
508 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
500 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
509 |
501 |
510 lemma one_le_Fract_iff: |
502 lemma one_le_Fract_iff: "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
511 "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
|
512 by (auto simp add: One_fract_def mult_le_cancel_right) |
503 by (auto simp add: One_fract_def mult_le_cancel_right) |
513 |
504 |
514 lemma Fract_le_one_iff: |
505 lemma Fract_le_one_iff: "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
515 "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
|
516 by (auto simp add: One_fract_def mult_le_cancel_right) |
506 by (auto simp add: One_fract_def mult_le_cancel_right) |
517 |
507 |
518 end |
508 end |