# HG changeset patch # User huffman # Date 1272126876 25200 # Node ID 6b9e487450ba367ee156ce01406f44de2febdc47 # Parent 58d4dc6000fc77856e7b291091809c21fc3d9167 Library/Fraction_Field.thy: ordering relations for fractions diff -r 58d4dc6000fc -r 6b9e487450ba src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Fri Apr 23 23:42:46 2010 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Sat Apr 24 09:34:36 2010 -0700 @@ -274,4 +274,255 @@ qed -end \ No newline at end of file +subsubsection {* The ordered field of fractions over an ordered idom *} + +lemma le_congruent2: + "(\x y::'a \ 'a::linordered_idom. + {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)}) + respects2 fractrel" +proof (clarsimp simp add: congruent2_def) + fix a b a' b' c d c' d' :: 'a + assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" + assume eq1: "a * b' = a' * b" + assume eq2: "c * d' = c' * d" + + let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" + { + fix a b c d x :: 'a assume x: "x \ 0" + have "?le a b c d = ?le (a * x) (b * x) c d" + proof - + from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) + hence "?le a b c d = + ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" + by (simp add: mult_le_cancel_right) + also have "... = ?le (a * x) (b * x) c d" + by (simp add: mult_ac) + finally show ?thesis . + qed + } note le_factor = this + + let ?D = "b * d" and ?D' = "b' * d'" + from neq have D: "?D \ 0" by simp + from neq have "?D' \ 0" by simp + hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" + by (rule le_factor) + also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" + by (simp add: mult_ac) + also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" + by (simp only: eq1 eq2) + also have "... = ?le (a' * ?D) (b' * ?D) c' d'" + by (simp add: mult_ac) + also from D have "... = ?le a' b' c' d'" + by (rule le_factor [symmetric]) + finally show "?le a b c d = ?le a' b' c' d'" . +qed + +instantiation fract :: (linordered_idom) linorder +begin + +definition + le_fract_def [code del]: + "q \ r \ contents (\x \ Rep_fract q. \y \ Rep_fract r. + {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)})" + +definition + less_fract_def [code del]: "z < (w::'a fract) \ z \ w \ \ w \ z" + +lemma le_fract [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" +by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) + +lemma less_fract [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)" +by (simp add: less_fract_def less_le_not_le mult_ac assms) + +instance proof + fix q r s :: "'a fract" + assume "q \ r" and "r \ s" thus "q \ s" + proof (induct q, induct r, induct s) + fix a b c d e f :: 'a + assume neq: "b \ 0" "d \ 0" "f \ 0" + assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f" + show "Fract a b \ Fract e f" + proof - + from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" + by (auto simp add: zero_less_mult_iff linorder_neq_iff) + have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" + proof - + from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + with ff show ?thesis by (simp add: mult_le_cancel_right) + qed + also have "... = (c * f) * (d * f) * (b * b)" + by (simp only: mult_ac) + also have "... \ (e * d) * (d * f) * (b * b)" + proof - + from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" + by simp + with bb show ?thesis by (simp add: mult_le_cancel_right) + qed + finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" + by (simp only: mult_ac) + with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" + by (simp add: mult_le_cancel_right) + with neq show ?thesis by simp + qed + qed +next + fix q r :: "'a fract" + assume "q \ r" and "r \ q" thus "q = r" + proof (induct q, induct r) + fix a b c d :: 'a + assume neq: "b \ 0" "d \ 0" + assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b" + show "Fract a b = Fract c d" + proof - + from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + also have "... \ (a * d) * (b * d)" + proof - + from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" + by simp + thus ?thesis by (simp only: mult_ac) + qed + finally have "(a * d) * (b * d) = (c * b) * (b * d)" . + moreover from neq have "b * d \ 0" by simp + ultimately have "a * d = c * b" by simp + with neq show ?thesis by (simp add: eq_fract) + qed + qed +next + fix q r :: "'a fract" + show "q \ q" + by (induct q) simp + show "(q < r) = (q \ r \ \ r \ q)" + by (simp only: less_fract_def) + show "q \ r \ r \ q" + by (induct q, induct r) + (simp add: mult_commute, rule linorder_linear) +qed + +end + +instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}" +begin + +definition + abs_fract_def: "\q\ = (if q < 0 then -q else (q::'a fract))" + +definition + sgn_fract_def: + "sgn (q::'a fract) = (if q=0 then 0 else if 0Fract a b\ = Fract \a\ \b\" + by (auto simp add: abs_fract_def Zero_fract_def le_less + eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) + +definition + inf_fract_def: + "(inf \ 'a fract \ 'a fract \ 'a fract) = min" + +definition + sup_fract_def: + "(sup \ 'a fract \ 'a fract \ 'a fract) = max" + +instance by intro_classes + (auto simp add: abs_fract_def sgn_fract_def + min_max.sup_inf_distrib1 inf_fract_def sup_fract_def) + +end + +instance fract :: (linordered_idom) linordered_field +proof + fix q r s :: "'a fract" + show "q \ r ==> s + q \ s + r" + proof (induct q, induct r, induct s) + fix a b c d e f :: 'a + assume neq: "b \ 0" "d \ 0" "f \ 0" + assume le: "Fract a b \ Fract c d" + show "Fract e f + Fract a b \ Fract e f + Fract c d" + proof - + let ?F = "f * f" from neq have F: "0 < ?F" + by (auto simp add: zero_less_mult_iff) + from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" + by (simp add: mult_le_cancel_right) + with neq show ?thesis by (simp add: ring_simps) + qed + qed + show "q < r ==> 0 < s ==> s * q < s * r" + proof (induct q, induct r, induct s) + fix a b c d e f :: 'a + assume neq: "b \ 0" "d \ 0" "f \ 0" + assume le: "Fract a b < Fract c d" + assume gt: "0 < Fract e f" + show "Fract e f * Fract a b < Fract e f * Fract c d" + proof - + let ?E = "e * f" and ?F = "f * f" + from neq gt have "0 < ?E" + by (auto simp add: Zero_fract_def order_less_le eq_fract) + moreover from neq have "0 < ?F" + by (auto simp add: zero_less_mult_iff) + moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" + by simp + ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" + by (simp add: mult_less_cancel_right) + with neq show ?thesis + by (simp add: mult_ac) + qed + qed +qed + +lemma fract_induct_pos [case_names Fract]: + fixes P :: "'a::linordered_idom fract \ bool" + assumes step: "\a b. 0 < b \ P (Fract a b)" + shows "P q" +proof (cases q) + have step': "\a b. b < 0 \ P (Fract a b)" + proof - + fix a::'a and b::'a + assume b: "b < 0" + hence "0 < -b" by simp + hence "P (Fract (-a) (-b))" by (rule step) + thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) + qed + case (Fract a b) + thus "P q" by (force simp add: linorder_neq_iff step step') +qed + +lemma zero_less_Fract_iff: + "0 < b \ 0 < Fract a b \ 0 < a" + by (auto simp add: Zero_fract_def zero_less_mult_iff) + +lemma Fract_less_zero_iff: + "0 < b \ Fract a b < 0 \ a < 0" + by (auto simp add: Zero_fract_def mult_less_0_iff) + +lemma zero_le_Fract_iff: + "0 < b \ 0 \ Fract a b \ 0 \ a" + by (auto simp add: Zero_fract_def zero_le_mult_iff) + +lemma Fract_le_zero_iff: + "0 < b \ Fract a b \ 0 \ a \ 0" + by (auto simp add: Zero_fract_def mult_le_0_iff) + +lemma one_less_Fract_iff: + "0 < b \ 1 < Fract a b \ b < a" + by (auto simp add: One_fract_def mult_less_cancel_right_disj) + +lemma Fract_less_one_iff: + "0 < b \ Fract a b < 1 \ a < b" + by (auto simp add: One_fract_def mult_less_cancel_right_disj) + +lemma one_le_Fract_iff: + "0 < b \ 1 \ Fract a b \ b \ a" + by (auto simp add: One_fract_def mult_le_cancel_right) + +lemma Fract_le_one_iff: + "0 < b \ Fract a b \ 1 \ a \ b" + by (auto simp add: One_fract_def mult_le_cancel_right) + +end