39 finally have "b' * (a * b'') = b' * (a'' * b)" . |
39 finally have "b' * (a * b'') = b' * (a'' * b)" . |
40 moreover from B have "b' \<noteq> 0" by auto |
40 moreover from B have "b' \<noteq> 0" by auto |
41 ultimately have "a * b'' = a'' * b" by simp |
41 ultimately have "a * b'' = a'' * b" by simp |
42 with A B show "((a, b), (a'', b'')) \<in> fractrel" by auto |
42 with A B show "((a, b), (a'', b'')) \<in> fractrel" by auto |
43 qed |
43 qed |
44 |
44 |
45 lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel" |
45 lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel" |
46 by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel]) |
46 by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel]) |
47 |
47 |
48 lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel] |
48 lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel] |
49 lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel] |
49 lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel] |
50 |
50 |
51 lemma equiv_fractrel_iff [iff]: |
51 lemma equiv_fractrel_iff [iff]: |
52 assumes "snd x \<noteq> 0" and "snd y \<noteq> 0" |
52 assumes "snd x \<noteq> 0" and "snd y \<noteq> 0" |
53 shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel" |
53 shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel" |
54 by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms) |
54 by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms) |
55 |
55 |
56 definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel" |
56 definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel" |
57 |
57 |
58 typedef 'a fract = "fract :: ('a * 'a::idom) set set" |
58 typedef 'a fract = "fract :: ('a * 'a::idom) set set" |
59 unfolding fract_def |
59 unfolding fract_def |
60 proof |
60 proof |
61 have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp |
61 have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp |
62 then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" by (rule quotientI) |
62 then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" |
|
63 by (rule quotientI) |
63 qed |
64 qed |
64 |
65 |
65 lemma fractrel_in_fract [simp]: "snd x \<noteq> 0 \<Longrightarrow> fractrel `` {x} \<in> fract" |
66 lemma fractrel_in_fract [simp]: "snd x \<noteq> 0 \<Longrightarrow> fractrel `` {x} \<in> fract" |
66 by (simp add: fract_def quotientI) |
67 by (simp add: fract_def quotientI) |
67 |
68 |
68 declare Abs_fract_inject [simp] Abs_fract_inverse [simp] |
69 declare Abs_fract_inject [simp] Abs_fract_inverse [simp] |
69 |
70 |
70 |
71 |
71 subsubsection {* Representation and basic operations *} |
72 subsubsection {* Representation and basic operations *} |
72 |
73 |
73 definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where |
74 definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" |
74 "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" |
75 where "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" |
75 |
76 |
76 code_datatype Fract |
77 code_datatype Fract |
77 |
78 |
78 lemma Fract_cases [cases type: fract]: |
79 lemma Fract_cases [cases type: fract]: |
79 obtains (Fract) a b where "q = Fract a b" "b \<noteq> 0" |
80 obtains (Fract) a b where "q = Fract a b" "b \<noteq> 0" |
80 by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) |
81 by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) |
81 |
82 |
82 lemma Fract_induct [case_names Fract, induct type: fract]: |
83 lemma Fract_induct [case_names Fract, induct type: fract]: |
83 shows "(\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)) \<Longrightarrow> P q" |
84 "(\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)) \<Longrightarrow> P q" |
84 by (cases q) simp |
85 by (cases q) simp |
85 |
86 |
86 lemma eq_fract: |
87 lemma eq_fract: |
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" |
88 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" |
88 and "\<And>a. Fract a 0 = Fract 0 1" |
89 and "\<And>a. Fract a 0 = Fract 0 1" |
103 lemma add_fract [simp]: |
104 lemma add_fract [simp]: |
104 assumes "b \<noteq> (0::'a::idom)" |
105 assumes "b \<noteq> (0::'a::idom)" |
105 and "d \<noteq> 0" |
106 and "d \<noteq> 0" |
106 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
107 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
107 proof - |
108 proof - |
108 have "(\<lambda>x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) |
109 have "(\<lambda>x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) respects2 fractrel" |
109 respects2 fractrel" |
110 by (rule equiv_fractrel [THEN congruent2_commuteI]) (simp_all add: algebra_simps) |
110 apply (rule equiv_fractrel [THEN congruent2_commuteI]) |
|
111 apply (auto simp add: algebra_simps) |
|
112 unfolding mult_assoc[symmetric] |
|
113 done |
|
114 with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) |
111 with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) |
115 qed |
112 qed |
116 |
113 |
117 definition minus_fract_def: |
114 definition minus_fract_def: |
118 "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})" |
115 "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})" |
119 |
116 |
120 lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)" |
117 lemma minus_fract [simp, code]: |
|
118 fixes a b :: "'a::idom" |
|
119 shows "- Fract a b = Fract (- a) b" |
121 proof - |
120 proof - |
122 have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel" |
121 have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel" |
123 by (simp add: congruent_def split_paired_all) |
122 by (simp add: congruent_def split_paired_all) |
124 then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel) |
123 then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel) |
125 qed |
124 qed |
128 by (cases "b = 0") (simp_all add: eq_fract) |
127 by (cases "b = 0") (simp_all add: eq_fract) |
129 |
128 |
130 definition diff_fract_def: "q - r = q + - (r::'a fract)" |
129 definition diff_fract_def: "q - r = q + - (r::'a fract)" |
131 |
130 |
132 lemma diff_fract [simp]: |
131 lemma diff_fract [simp]: |
133 assumes "b \<noteq> 0" and "d \<noteq> 0" |
132 assumes "b \<noteq> 0" |
|
133 and "d \<noteq> 0" |
134 shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" |
134 shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" |
135 using assms by (simp add: diff_fract_def) |
135 using assms by (simp add: diff_fract_def) |
136 |
136 |
137 definition mult_fract_def: |
137 definition mult_fract_def: |
138 "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
138 "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
139 fractrel``{(fst x * fst y, snd x * snd y)})" |
139 fractrel``{(fst x * fst y, snd x * snd y)})" |
140 |
140 |
141 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)" |
142 proof - |
142 proof - |
143 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" |
144 apply (rule equiv_fractrel [THEN congruent2_commuteI]) |
144 by (rule equiv_fractrel [THEN congruent2_commuteI]) (simp_all add: algebra_simps) |
145 apply (auto simp add: algebra_simps) |
|
146 done |
|
147 then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) |
145 then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) |
148 qed |
146 qed |
149 |
147 |
150 lemma mult_fract_cancel: |
148 lemma mult_fract_cancel: |
151 assumes "c \<noteq> (0::'a)" |
149 assumes "c \<noteq> (0::'a)" |
152 shows "Fract (c * a) (c * b) = Fract a b" |
150 shows "Fract (c * a) (c * b) = Fract a b" |
153 proof - |
151 proof - |
154 from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) |
152 from assms have "Fract c c = Fract 1 1" |
155 then show ?thesis by (simp add: mult_fract [symmetric]) |
153 by (simp add: Fract_def) |
|
154 then show ?thesis |
|
155 by (simp add: mult_fract [symmetric]) |
156 qed |
156 qed |
157 |
157 |
158 instance |
158 instance |
159 proof |
159 proof |
160 fix q r s :: "'a fract" |
160 fix q r s :: "'a fract" |
161 show "(q * r) * s = q * (r * s)" |
161 show "(q * r) * s = q * (r * s)" |
162 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) |
163 show "q * r = r * q" |
163 show "q * r = r * q" |
164 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
164 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
165 show "1 * q = q" |
165 show "1 * q = q" |
166 by (cases q) (simp add: One_fract_def eq_fract) |
166 by (cases q) (simp add: One_fract_def eq_fract) |
231 "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q. |
231 "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q. |
232 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)})" |
233 |
233 |
234 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" |
235 proof - |
235 proof - |
236 have *: "\<And>x. (0::'a) = x \<longleftrightarrow> x = 0" by auto |
236 have *: "\<And>x. (0::'a) = x \<longleftrightarrow> x = 0" |
|
237 by auto |
237 have "(\<lambda>x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" |
238 have "(\<lambda>x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" |
238 by (auto simp add: congruent_def * algebra_simps) |
239 by (auto simp add: congruent_def * algebra_simps) |
239 then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel) |
240 then show ?thesis |
|
241 by (simp add: Fract_def inverse_fract_def UN_fractrel) |
240 qed |
242 qed |
241 |
243 |
242 definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)" |
244 definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)" |
243 |
245 |
244 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" |
246 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" |
274 assume eq1: "a * b' = a' * b" |
276 assume eq1: "a * b' = a' * b" |
275 assume eq2: "c * d' = c' * d" |
277 assume eq2: "c * d' = c' * d" |
276 |
278 |
277 let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" |
279 let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" |
278 { |
280 { |
279 fix a b c d x :: 'a assume x: "x \<noteq> 0" |
281 fix a b c d x :: 'a |
|
282 assume x: "x \<noteq> 0" |
280 have "?le a b c d = ?le (a * x) (b * x) c d" |
283 have "?le a b c d = ?le (a * x) (b * x) c d" |
281 proof - |
284 proof - |
282 from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) |
285 from x have "0 < x * x" |
|
286 by (auto simp add: zero_less_mult_iff) |
283 then have "?le a b c d = |
287 then have "?le a b c d = |
284 ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" |
288 ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" |
285 by (simp add: mult_le_cancel_right) |
289 by (simp add: mult_le_cancel_right) |
286 also have "... = ?le (a * x) (b * x) c d" |
290 also have "... = ?le (a * x) (b * x) c d" |
287 by (simp add: mult_ac) |
291 by (simp add: mult_ac) |
313 {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" |
317 {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" |
314 |
318 |
315 definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
319 definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
316 |
320 |
317 lemma le_fract [simp]: |
321 lemma le_fract [simp]: |
318 assumes "b \<noteq> 0" and "d \<noteq> 0" |
322 assumes "b \<noteq> 0" |
|
323 and "d \<noteq> 0" |
319 shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
324 shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
320 by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) |
325 by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) |
321 |
326 |
322 lemma less_fract [simp]: |
327 lemma less_fract [simp]: |
323 assumes "b \<noteq> 0" and "d \<noteq> 0" |
328 assumes "b \<noteq> 0" |
|
329 and "d \<noteq> 0" |
324 shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
330 shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
325 by (simp add: less_fract_def less_le_not_le mult_ac assms) |
331 by (simp add: less_fract_def less_le_not_le mult_ac assms) |
326 |
332 |
327 instance |
333 instance |
328 proof |
334 proof |
329 fix q r s :: "'a fract" |
335 fix q r s :: "'a fract" |
330 assume "q \<le> r" and "r \<le> s" thus "q \<le> s" |
336 assume "q \<le> r" and "r \<le> s" |
|
337 then show "q \<le> s" |
331 proof (induct q, induct r, induct s) |
338 proof (induct q, induct r, induct s) |
332 fix a b c d e f :: 'a |
339 fix a b c d e f :: 'a |
333 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
340 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
334 assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f" |
341 assume 1: "Fract a b \<le> Fract c d" |
|
342 assume 2: "Fract c d \<le> Fract e f" |
335 show "Fract a b \<le> Fract e f" |
343 show "Fract a b \<le> Fract e f" |
336 proof - |
344 proof - |
337 from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" |
345 from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" |
338 by (auto simp add: zero_less_mult_iff linorder_neq_iff) |
346 by (auto simp add: zero_less_mult_iff linorder_neq_iff) |
339 have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)" |
347 have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)" |
357 with neq show ?thesis by simp |
365 with neq show ?thesis by simp |
358 qed |
366 qed |
359 qed |
367 qed |
360 next |
368 next |
361 fix q r :: "'a fract" |
369 fix q r :: "'a fract" |
362 assume "q \<le> r" and "r \<le> q" thus "q = r" |
370 assume "q \<le> r" and "r \<le> q" |
|
371 then show "q = r" |
363 proof (induct q, induct r) |
372 proof (induct q, induct r) |
364 fix a b c d :: 'a |
373 fix a b c d :: 'a |
365 assume neq: "b \<noteq> 0" "d \<noteq> 0" |
374 assume neq: "b \<noteq> 0" "d \<noteq> 0" |
366 assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b" |
375 assume 1: "Fract a b \<le> Fract c d" |
|
376 assume 2: "Fract c d \<le> Fract a b" |
367 show "Fract a b = Fract c d" |
377 show "Fract a b = Fract c d" |
368 proof - |
378 proof - |
369 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
379 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
370 by simp |
380 by simp |
371 also have "... \<le> (a * d) * (b * d)" |
381 also have "... \<le> (a * d) * (b * d)" |
372 proof - |
382 proof - |
373 from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" |
383 from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" |
374 by simp |
384 by simp |
375 thus ?thesis by (simp only: mult_ac) |
385 then show ?thesis by (simp only: mult_ac) |
376 qed |
386 qed |
377 finally have "(a * d) * (b * d) = (c * b) * (b * d)" . |
387 finally have "(a * d) * (b * d) = (c * b) * (b * d)" . |
378 moreover from neq have "b * d \<noteq> 0" by simp |
388 moreover from neq have "b * d \<noteq> 0" by simp |
379 ultimately have "a * d = c * b" by simp |
389 ultimately have "a * d = c * b" by simp |
380 with neq show ?thesis by (simp add: eq_fract) |
390 with neq show ?thesis by (simp add: eq_fract) |
391 (simp add: mult_commute, rule linorder_linear) |
401 (simp add: mult_commute, rule linorder_linear) |
392 qed |
402 qed |
393 |
403 |
394 end |
404 end |
395 |
405 |
396 instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}" |
406 instantiation fract :: (linordered_idom) "{distrib_lattice,abs_if,sgn_if}" |
397 begin |
407 begin |
398 |
408 |
399 definition abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))" |
409 definition abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))" |
400 |
410 |
401 definition sgn_fract_def: |
411 definition sgn_fract_def: |
402 "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)" |
412 "sgn (q::'a fract) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" |
403 |
413 |
404 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
414 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
405 by (auto simp add: abs_fract_def Zero_fract_def le_less |
415 by (auto simp add: abs_fract_def Zero_fract_def le_less |
406 eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) |
416 eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) |
407 |
417 |
442 fix q r s :: "'a fract" |
452 fix q r s :: "'a fract" |
443 assume "q < r" and "0 < s" |
453 assume "q < r" and "0 < s" |
444 then show "s * q < s * r" |
454 then show "s * q < s * r" |
445 proof (induct q, induct r, induct s) |
455 proof (induct q, induct r, induct s) |
446 fix a b c d e f :: 'a |
456 fix a b c d e f :: 'a |
447 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
457 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
448 assume le: "Fract a b < Fract c d" |
458 assume le: "Fract a b < Fract c d" |
449 assume gt: "0 < Fract e f" |
459 assume gt: "0 < Fract e f" |
450 show "Fract e f * Fract a b < Fract e f * Fract c d" |
460 show "Fract e f * Fract a b < Fract e f * Fract c d" |
451 proof - |
461 proof - |
452 let ?E = "e * f" and ?F = "f * f" |
462 let ?E = "e * f" and ?F = "f * f" |
467 lemma fract_induct_pos [case_names Fract]: |
477 lemma fract_induct_pos [case_names Fract]: |
468 fixes P :: "'a::linordered_idom fract \<Rightarrow> bool" |
478 fixes P :: "'a::linordered_idom fract \<Rightarrow> bool" |
469 assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
479 assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
470 shows "P q" |
480 shows "P q" |
471 proof (cases q) |
481 proof (cases q) |
472 have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)" |
482 case (Fract a b) |
473 proof - |
483 { |
474 fix a::'a and b::'a |
484 fix a b :: 'a |
475 assume b: "b < 0" |
485 assume b: "b < 0" |
476 then have "0 < -b" by simp |
486 have "P (Fract a b)" |
477 then have "P (Fract (-a) (-b))" by (rule step) |
487 proof - |
478 thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) |
488 from b have "0 < - b" by simp |
479 qed |
489 then have "P (Fract (- a) (- b))" |
480 case (Fract a b) |
490 by (rule step) |
481 thus "P q" by (force simp add: linorder_neq_iff step step') |
491 then show "P (Fract a b)" |
|
492 by (simp add: order_less_imp_not_eq [OF b]) |
|
493 qed |
|
494 } |
|
495 with Fract show "P q" |
|
496 by (auto simp add: linorder_neq_iff step) |
482 qed |
497 qed |
483 |
498 |
484 lemma zero_less_Fract_iff: "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
499 lemma zero_less_Fract_iff: "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
485 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
500 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
486 |
501 |