272 show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand) |
272 show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand) |
273 (simp add: fract_collapse) |
273 (simp add: fract_collapse) |
274 qed |
274 qed |
275 |
275 |
276 |
276 |
|
277 subsubsection {* The ordered field of fractions over an ordered idom *} |
|
278 |
|
279 lemma le_congruent2: |
|
280 "(\<lambda>x y::'a \<times> 'a::linordered_idom. |
|
281 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)}) |
|
282 respects2 fractrel" |
|
283 proof (clarsimp simp add: congruent2_def) |
|
284 fix a b a' b' c d c' d' :: 'a |
|
285 assume neq: "b \<noteq> 0" "b' \<noteq> 0" "d \<noteq> 0" "d' \<noteq> 0" |
|
286 assume eq1: "a * b' = a' * b" |
|
287 assume eq2: "c * d' = c' * d" |
|
288 |
|
289 let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" |
|
290 { |
|
291 fix a b c d x :: 'a assume x: "x \<noteq> 0" |
|
292 have "?le a b c d = ?le (a * x) (b * x) c d" |
|
293 proof - |
|
294 from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) |
|
295 hence "?le a b c d = |
|
296 ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" |
|
297 by (simp add: mult_le_cancel_right) |
|
298 also have "... = ?le (a * x) (b * x) c d" |
|
299 by (simp add: mult_ac) |
|
300 finally show ?thesis . |
|
301 qed |
|
302 } note le_factor = this |
|
303 |
|
304 let ?D = "b * d" and ?D' = "b' * d'" |
|
305 from neq have D: "?D \<noteq> 0" by simp |
|
306 from neq have "?D' \<noteq> 0" by simp |
|
307 hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" |
|
308 by (rule le_factor) |
|
309 also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" |
|
310 by (simp add: mult_ac) |
|
311 also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')" |
|
312 by (simp only: eq1 eq2) |
|
313 also have "... = ?le (a' * ?D) (b' * ?D) c' d'" |
|
314 by (simp add: mult_ac) |
|
315 also from D have "... = ?le a' b' c' d'" |
|
316 by (rule le_factor [symmetric]) |
|
317 finally show "?le a b c d = ?le a' b' c' d'" . |
|
318 qed |
|
319 |
|
320 instantiation fract :: (linordered_idom) linorder |
|
321 begin |
|
322 |
|
323 definition |
|
324 le_fract_def [code del]: |
|
325 "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r. |
|
326 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})" |
|
327 |
|
328 definition |
|
329 less_fract_def [code del]: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
|
330 |
|
331 lemma le_fract [simp]: |
|
332 assumes "b \<noteq> 0" and "d \<noteq> 0" |
|
333 shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
334 by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) |
|
335 |
|
336 lemma less_fract [simp]: |
|
337 assumes "b \<noteq> 0" and "d \<noteq> 0" |
|
338 shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
|
339 by (simp add: less_fract_def less_le_not_le mult_ac assms) |
|
340 |
|
341 instance proof |
|
342 fix q r s :: "'a fract" |
|
343 assume "q \<le> r" and "r \<le> s" thus "q \<le> s" |
|
344 proof (induct q, induct r, induct s) |
|
345 fix a b c d e f :: 'a |
|
346 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
347 assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f" |
|
348 show "Fract a b \<le> Fract e f" |
|
349 proof - |
|
350 from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" |
|
351 by (auto simp add: zero_less_mult_iff linorder_neq_iff) |
|
352 have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)" |
|
353 proof - |
|
354 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
355 by simp |
|
356 with ff show ?thesis by (simp add: mult_le_cancel_right) |
|
357 qed |
|
358 also have "... = (c * f) * (d * f) * (b * b)" |
|
359 by (simp only: mult_ac) |
|
360 also have "... \<le> (e * d) * (d * f) * (b * b)" |
|
361 proof - |
|
362 from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)" |
|
363 by simp |
|
364 with bb show ?thesis by (simp add: mult_le_cancel_right) |
|
365 qed |
|
366 finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)" |
|
367 by (simp only: mult_ac) |
|
368 with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)" |
|
369 by (simp add: mult_le_cancel_right) |
|
370 with neq show ?thesis by simp |
|
371 qed |
|
372 qed |
|
373 next |
|
374 fix q r :: "'a fract" |
|
375 assume "q \<le> r" and "r \<le> q" thus "q = r" |
|
376 proof (induct q, induct r) |
|
377 fix a b c d :: 'a |
|
378 assume neq: "b \<noteq> 0" "d \<noteq> 0" |
|
379 assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b" |
|
380 show "Fract a b = Fract c d" |
|
381 proof - |
|
382 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
383 by simp |
|
384 also have "... \<le> (a * d) * (b * d)" |
|
385 proof - |
|
386 from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" |
|
387 by simp |
|
388 thus ?thesis by (simp only: mult_ac) |
|
389 qed |
|
390 finally have "(a * d) * (b * d) = (c * b) * (b * d)" . |
|
391 moreover from neq have "b * d \<noteq> 0" by simp |
|
392 ultimately have "a * d = c * b" by simp |
|
393 with neq show ?thesis by (simp add: eq_fract) |
|
394 qed |
|
395 qed |
|
396 next |
|
397 fix q r :: "'a fract" |
|
398 show "q \<le> q" |
|
399 by (induct q) simp |
|
400 show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" |
|
401 by (simp only: less_fract_def) |
|
402 show "q \<le> r \<or> r \<le> q" |
|
403 by (induct q, induct r) |
|
404 (simp add: mult_commute, rule linorder_linear) |
|
405 qed |
|
406 |
277 end |
407 end |
|
408 |
|
409 instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}" |
|
410 begin |
|
411 |
|
412 definition |
|
413 abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))" |
|
414 |
|
415 definition |
|
416 sgn_fract_def: |
|
417 "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)" |
|
418 |
|
419 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
|
420 by (auto simp add: abs_fract_def Zero_fract_def le_less |
|
421 eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) |
|
422 |
|
423 definition |
|
424 inf_fract_def: |
|
425 "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min" |
|
426 |
|
427 definition |
|
428 sup_fract_def: |
|
429 "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max" |
|
430 |
|
431 instance by intro_classes |
|
432 (auto simp add: abs_fract_def sgn_fract_def |
|
433 min_max.sup_inf_distrib1 inf_fract_def sup_fract_def) |
|
434 |
|
435 end |
|
436 |
|
437 instance fract :: (linordered_idom) linordered_field |
|
438 proof |
|
439 fix q r s :: "'a fract" |
|
440 show "q \<le> r ==> s + q \<le> s + r" |
|
441 proof (induct q, induct r, induct s) |
|
442 fix a b c d e f :: 'a |
|
443 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
444 assume le: "Fract a b \<le> Fract c d" |
|
445 show "Fract e f + Fract a b \<le> Fract e f + Fract c d" |
|
446 proof - |
|
447 let ?F = "f * f" from neq have F: "0 < ?F" |
|
448 by (auto simp add: zero_less_mult_iff) |
|
449 from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
450 by simp |
|
451 with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" |
|
452 by (simp add: mult_le_cancel_right) |
|
453 with neq show ?thesis by (simp add: ring_simps) |
|
454 qed |
|
455 qed |
|
456 show "q < r ==> 0 < s ==> s * q < s * r" |
|
457 proof (induct q, induct r, induct s) |
|
458 fix a b c d e f :: 'a |
|
459 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
460 assume le: "Fract a b < Fract c d" |
|
461 assume gt: "0 < Fract e f" |
|
462 show "Fract e f * Fract a b < Fract e f * Fract c d" |
|
463 proof - |
|
464 let ?E = "e * f" and ?F = "f * f" |
|
465 from neq gt have "0 < ?E" |
|
466 by (auto simp add: Zero_fract_def order_less_le eq_fract) |
|
467 moreover from neq have "0 < ?F" |
|
468 by (auto simp add: zero_less_mult_iff) |
|
469 moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" |
|
470 by simp |
|
471 ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" |
|
472 by (simp add: mult_less_cancel_right) |
|
473 with neq show ?thesis |
|
474 by (simp add: mult_ac) |
|
475 qed |
|
476 qed |
|
477 qed |
|
478 |
|
479 lemma fract_induct_pos [case_names Fract]: |
|
480 fixes P :: "'a::linordered_idom fract \<Rightarrow> bool" |
|
481 assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
|
482 shows "P q" |
|
483 proof (cases q) |
|
484 have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)" |
|
485 proof - |
|
486 fix a::'a and b::'a |
|
487 assume b: "b < 0" |
|
488 hence "0 < -b" by simp |
|
489 hence "P (Fract (-a) (-b))" by (rule step) |
|
490 thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) |
|
491 qed |
|
492 case (Fract a b) |
|
493 thus "P q" by (force simp add: linorder_neq_iff step step') |
|
494 qed |
|
495 |
|
496 lemma zero_less_Fract_iff: |
|
497 "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
|
498 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
|
499 |
|
500 lemma Fract_less_zero_iff: |
|
501 "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
|
502 by (auto simp add: Zero_fract_def mult_less_0_iff) |
|
503 |
|
504 lemma zero_le_Fract_iff: |
|
505 "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
|
506 by (auto simp add: Zero_fract_def zero_le_mult_iff) |
|
507 |
|
508 lemma Fract_le_zero_iff: |
|
509 "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
510 by (auto simp add: Zero_fract_def mult_le_0_iff) |
|
511 |
|
512 lemma one_less_Fract_iff: |
|
513 "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
|
514 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
|
515 |
|
516 lemma Fract_less_one_iff: |
|
517 "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
|
518 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
|
519 |
|
520 lemma one_le_Fract_iff: |
|
521 "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
|
522 by (auto simp add: One_fract_def mult_le_cancel_right) |
|
523 |
|
524 lemma Fract_le_one_iff: |
|
525 "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
|
526 by (auto simp add: One_fract_def mult_le_cancel_right) |
|
527 |
|
528 end |