src/HOL/Library/Fraction_Field.thy
 author haftmann Fri Oct 01 16:05:25 2010 +0200 (2010-10-01) changeset 39910 10097e0a9dbd parent 37765 26bdfb7b680b child 40815 6e2d17cc0d1d permissions -rw-r--r--
constant `contents` renamed to `the_elem`
 haftmann@35372 ` 1` ```(* Title: HOL/Library/Fraction_Field.thy ``` chaieb@31761 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@31761 ` 3` ```*) ``` chaieb@31761 ` 4` chaieb@31761 ` 5` ```header{* A formalization of the fraction field of any integral domain ``` haftmann@35372 ` 6` ``` A generalization of Rat.thy from int to any integral domain *} ``` chaieb@31761 ` 7` chaieb@31761 ` 8` ```theory Fraction_Field ``` haftmann@35372 ` 9` ```imports Main ``` chaieb@31761 ` 10` ```begin ``` chaieb@31761 ` 11` chaieb@31761 ` 12` ```subsection {* General fractions construction *} ``` chaieb@31761 ` 13` chaieb@31761 ` 14` ```subsubsection {* Construction of the type of fractions *} ``` chaieb@31761 ` 15` chaieb@31761 ` 16` ```definition fractrel :: "(('a::idom * 'a ) * ('a * 'a)) set" where ``` chaieb@31761 ` 17` ``` "fractrel == {(x, y). snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x}" ``` chaieb@31761 ` 18` chaieb@31761 ` 19` ```lemma fractrel_iff [simp]: ``` chaieb@31761 ` 20` ``` "(x, y) \ fractrel \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" ``` chaieb@31761 ` 21` ``` by (simp add: fractrel_def) ``` chaieb@31761 ` 22` chaieb@31761 ` 23` ```lemma refl_fractrel: "refl_on {x. snd x \ 0} fractrel" ``` chaieb@31761 ` 24` ``` by (auto simp add: refl_on_def fractrel_def) ``` chaieb@31761 ` 25` chaieb@31761 ` 26` ```lemma sym_fractrel: "sym fractrel" ``` chaieb@31761 ` 27` ``` by (simp add: fractrel_def sym_def) ``` chaieb@31761 ` 28` chaieb@31761 ` 29` ```lemma trans_fractrel: "trans fractrel" ``` chaieb@31761 ` 30` ```proof (rule transI, unfold split_paired_all) ``` chaieb@31761 ` 31` ``` fix a b a' b' a'' b'' :: 'a ``` chaieb@31761 ` 32` ``` assume A: "((a, b), (a', b')) \ fractrel" ``` chaieb@31761 ` 33` ``` assume B: "((a', b'), (a'', b'')) \ fractrel" ``` chaieb@31761 ` 34` ``` have "b' * (a * b'') = b'' * (a * b')" by (simp add: mult_ac) ``` chaieb@31761 ` 35` ``` also from A have "a * b' = a' * b" by auto ``` chaieb@31761 ` 36` ``` also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: mult_ac) ``` chaieb@31761 ` 37` ``` also from B have "a' * b'' = a'' * b'" by auto ``` chaieb@31761 ` 38` ``` also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: mult_ac) ``` chaieb@31761 ` 39` ``` finally have "b' * (a * b'') = b' * (a'' * b)" . ``` chaieb@31761 ` 40` ``` moreover from B have "b' \ 0" by auto ``` chaieb@31761 ` 41` ``` ultimately have "a * b'' = a'' * b" by simp ``` chaieb@31761 ` 42` ``` with A B show "((a, b), (a'', b'')) \ fractrel" by auto ``` chaieb@31761 ` 43` ```qed ``` chaieb@31761 ` 44` ``` ``` chaieb@31761 ` 45` ```lemma equiv_fractrel: "equiv {x. snd x \ 0} fractrel" ``` chaieb@31761 ` 46` ``` by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel]) ``` chaieb@31761 ` 47` chaieb@31761 ` 48` ```lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel] ``` chaieb@31761 ` 49` ```lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel] ``` chaieb@31761 ` 50` chaieb@31761 ` 51` ```lemma equiv_fractrel_iff [iff]: ``` chaieb@31761 ` 52` ``` assumes "snd x \ 0" and "snd y \ 0" ``` chaieb@31761 ` 53` ``` shows "fractrel `` {x} = fractrel `` {y} \ (x, y) \ fractrel" ``` chaieb@31761 ` 54` ``` by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms) ``` chaieb@31761 ` 55` chaieb@31761 ` 56` ```typedef 'a fract = "{(x::'a\'a). snd x \ (0::'a::idom)} // fractrel" ``` chaieb@31761 ` 57` ```proof ``` chaieb@31761 ` 58` ``` have "(0::'a, 1::'a) \ {x. snd x \ 0}" by simp ``` chaieb@31761 ` 59` ``` then show "fractrel `` {(0::'a, 1)} \ {x. snd x \ 0} // fractrel" by (rule quotientI) ``` chaieb@31761 ` 60` ```qed ``` chaieb@31761 ` 61` chaieb@31761 ` 62` ```lemma fractrel_in_fract [simp]: "snd x \ 0 \ fractrel `` {x} \ fract" ``` chaieb@31761 ` 63` ``` by (simp add: fract_def quotientI) ``` chaieb@31761 ` 64` chaieb@31761 ` 65` ```declare Abs_fract_inject [simp] Abs_fract_inverse [simp] ``` chaieb@31761 ` 66` chaieb@31761 ` 67` chaieb@31761 ` 68` ```subsubsection {* Representation and basic operations *} ``` chaieb@31761 ` 69` chaieb@31761 ` 70` ```definition ``` chaieb@31761 ` 71` ``` Fract :: "'a::idom \ 'a \ 'a fract" where ``` haftmann@37765 ` 72` ``` "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" ``` chaieb@31761 ` 73` chaieb@31761 ` 74` ```code_datatype Fract ``` chaieb@31761 ` 75` chaieb@31761 ` 76` ```lemma Fract_cases [case_names Fract, cases type: fract]: ``` chaieb@31761 ` 77` ``` assumes "\a b. q = Fract a b \ b \ 0 \ C" ``` chaieb@31761 ` 78` ``` shows C ``` chaieb@31761 ` 79` ``` using assms by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) ``` chaieb@31761 ` 80` chaieb@31761 ` 81` ```lemma Fract_induct [case_names Fract, induct type: fract]: ``` chaieb@31761 ` 82` ``` assumes "\a b. b \ 0 \ P (Fract a b)" ``` chaieb@31761 ` 83` ``` shows "P q" ``` chaieb@31761 ` 84` ``` using assms by (cases q) simp ``` chaieb@31761 ` 85` chaieb@31761 ` 86` ```lemma eq_fract: ``` chaieb@31761 ` 87` ``` shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" ``` chaieb@31761 ` 88` ``` and "\a. Fract a 0 = Fract 0 1" ``` chaieb@31761 ` 89` ``` and "\a c. Fract 0 a = Fract 0 c" ``` chaieb@31761 ` 90` ``` by (simp_all add: Fract_def) ``` chaieb@31761 ` 91` chaieb@31761 ` 92` ```instantiation fract :: (idom) "{comm_ring_1, power}" ``` chaieb@31761 ` 93` ```begin ``` chaieb@31761 ` 94` chaieb@31761 ` 95` ```definition ``` haftmann@37765 ` 96` ``` Zero_fract_def [code_unfold]: "0 = Fract 0 1" ``` chaieb@31761 ` 97` chaieb@31761 ` 98` ```definition ``` haftmann@37765 ` 99` ``` One_fract_def [code_unfold]: "1 = Fract 1 1" ``` chaieb@31761 ` 100` chaieb@31761 ` 101` ```definition ``` haftmann@37765 ` 102` ``` add_fract_def: ``` chaieb@31761 ` 103` ``` "q + r = Abs_fract (\x \ Rep_fract q. \y \ Rep_fract r. ``` chaieb@31761 ` 104` ``` fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" ``` chaieb@31761 ` 105` chaieb@31761 ` 106` ```lemma add_fract [simp]: ``` chaieb@31761 ` 107` ``` assumes "b \ (0::'a::idom)" and "d \ 0" ``` chaieb@31761 ` 108` ``` shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" ``` chaieb@31761 ` 109` ```proof - ``` chaieb@31761 ` 110` ``` have "(\x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) ``` chaieb@31761 ` 111` ``` respects2 fractrel" ``` chaieb@31761 ` 112` ``` apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps) ``` chaieb@31761 ` 113` ``` unfolding mult_assoc[symmetric] . ``` chaieb@31761 ` 114` ``` with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) ``` chaieb@31761 ` 115` ```qed ``` chaieb@31761 ` 116` chaieb@31761 ` 117` ```definition ``` haftmann@37765 ` 118` ``` minus_fract_def: ``` chaieb@31761 ` 119` ``` "- q = Abs_fract (\x \ Rep_fract q. fractrel `` {(- fst x, snd x)})" ``` chaieb@31761 ` 120` chaieb@31761 ` 121` ```lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)" ``` chaieb@31761 ` 122` ```proof - ``` chaieb@31761 ` 123` ``` have "(\x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel" ``` chaieb@31761 ` 124` ``` by (simp add: congruent_def) ``` chaieb@31761 ` 125` ``` then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel) ``` chaieb@31761 ` 126` ```qed ``` chaieb@31761 ` 127` chaieb@31761 ` 128` ```lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b" ``` chaieb@31761 ` 129` ``` by (cases "b = 0") (simp_all add: eq_fract) ``` chaieb@31761 ` 130` chaieb@31761 ` 131` ```definition ``` haftmann@37765 ` 132` ``` diff_fract_def: "q - r = q + - (r::'a fract)" ``` chaieb@31761 ` 133` chaieb@31761 ` 134` ```lemma diff_fract [simp]: ``` chaieb@31761 ` 135` ``` assumes "b \ 0" and "d \ 0" ``` chaieb@31761 ` 136` ``` shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" ``` chaieb@31761 ` 137` ``` using assms by (simp add: diff_fract_def diff_minus) ``` chaieb@31761 ` 138` chaieb@31761 ` 139` ```definition ``` haftmann@37765 ` 140` ``` mult_fract_def: ``` chaieb@31761 ` 141` ``` "q * r = Abs_fract (\x \ Rep_fract q. \y \ Rep_fract r. ``` chaieb@31761 ` 142` ``` fractrel``{(fst x * fst y, snd x * snd y)})" ``` chaieb@31761 ` 143` chaieb@31761 ` 144` ```lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)" ``` chaieb@31761 ` 145` ```proof - ``` chaieb@31761 ` 146` ``` have "(\x y. fractrel `` {(fst x * fst y, snd x * snd y :: 'a)}) respects2 fractrel" ``` chaieb@31761 ` 147` ``` apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps) ``` chaieb@31761 ` 148` ``` unfolding mult_assoc[symmetric] . ``` chaieb@31761 ` 149` ``` then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) ``` chaieb@31761 ` 150` ```qed ``` chaieb@31761 ` 151` chaieb@31761 ` 152` ```lemma mult_fract_cancel: ``` chaieb@31761 ` 153` ``` assumes "c \ 0" ``` chaieb@31761 ` 154` ``` shows "Fract (c * a) (c * b) = Fract a b" ``` chaieb@31761 ` 155` ```proof - ``` chaieb@31761 ` 156` ``` from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) ``` chaieb@31761 ` 157` ``` then show ?thesis by (simp add: mult_fract [symmetric]) ``` chaieb@31761 ` 158` ```qed ``` chaieb@31761 ` 159` chaieb@31761 ` 160` ```instance proof ``` chaieb@31761 ` 161` ``` fix q r s :: "'a fract" show "(q * r) * s = q * (r * s)" ``` chaieb@31761 ` 162` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` chaieb@31761 ` 163` ```next ``` chaieb@31761 ` 164` ``` fix q r :: "'a fract" show "q * r = r * q" ``` chaieb@31761 ` 165` ``` by (cases q, cases r) (simp add: eq_fract algebra_simps) ``` chaieb@31761 ` 166` ```next ``` chaieb@31761 ` 167` ``` fix q :: "'a fract" show "1 * q = q" ``` chaieb@31761 ` 168` ``` by (cases q) (simp add: One_fract_def eq_fract) ``` chaieb@31761 ` 169` ```next ``` chaieb@31761 ` 170` ``` fix q r s :: "'a fract" show "(q + r) + s = q + (r + s)" ``` chaieb@31761 ` 171` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` chaieb@31761 ` 172` ```next ``` chaieb@31761 ` 173` ``` fix q r :: "'a fract" show "q + r = r + q" ``` chaieb@31761 ` 174` ``` by (cases q, cases r) (simp add: eq_fract algebra_simps) ``` chaieb@31761 ` 175` ```next ``` chaieb@31761 ` 176` ``` fix q :: "'a fract" show "0 + q = q" ``` chaieb@31761 ` 177` ``` by (cases q) (simp add: Zero_fract_def eq_fract) ``` chaieb@31761 ` 178` ```next ``` chaieb@31761 ` 179` ``` fix q :: "'a fract" show "- q + q = 0" ``` chaieb@31761 ` 180` ``` by (cases q) (simp add: Zero_fract_def eq_fract) ``` chaieb@31761 ` 181` ```next ``` chaieb@31761 ` 182` ``` fix q r :: "'a fract" show "q - r = q + - r" ``` chaieb@31761 ` 183` ``` by (cases q, cases r) (simp add: eq_fract) ``` chaieb@31761 ` 184` ```next ``` chaieb@31761 ` 185` ``` fix q r s :: "'a fract" show "(q + r) * s = q * s + r * s" ``` chaieb@31761 ` 186` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` chaieb@31761 ` 187` ```next ``` chaieb@31761 ` 188` ``` show "(0::'a fract) \ 1" by (simp add: Zero_fract_def One_fract_def eq_fract) ``` chaieb@31761 ` 189` ```qed ``` chaieb@31761 ` 190` chaieb@31761 ` 191` ```end ``` chaieb@31761 ` 192` chaieb@31761 ` 193` ```lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1" ``` chaieb@31761 ` 194` ``` by (induct k) (simp_all add: Zero_fract_def One_fract_def) ``` chaieb@31761 ` 195` chaieb@31761 ` 196` ```lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" ``` chaieb@31761 ` 197` ``` by (rule of_nat_fract [symmetric]) ``` chaieb@31761 ` 198` haftmann@31998 ` 199` ```lemma fract_collapse [code_post]: ``` chaieb@31761 ` 200` ``` "Fract 0 k = 0" ``` chaieb@31761 ` 201` ``` "Fract 1 1 = 1" ``` chaieb@31761 ` 202` ``` "Fract k 0 = 0" ``` chaieb@31761 ` 203` ``` by (cases "k = 0") ``` chaieb@31761 ` 204` ``` (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def) ``` chaieb@31761 ` 205` haftmann@31998 ` 206` ```lemma fract_expand [code_unfold]: ``` chaieb@31761 ` 207` ``` "0 = Fract 0 1" ``` chaieb@31761 ` 208` ``` "1 = Fract 1 1" ``` chaieb@31761 ` 209` ``` by (simp_all add: fract_collapse) ``` chaieb@31761 ` 210` chaieb@31761 ` 211` ```lemma Fract_cases_nonzero [case_names Fract 0]: ``` chaieb@31761 ` 212` ``` assumes Fract: "\a b. q = Fract a b \ b \ 0 \ a \ 0 \ C" ``` chaieb@31761 ` 213` ``` assumes 0: "q = 0 \ C" ``` chaieb@31761 ` 214` ``` shows C ``` chaieb@31761 ` 215` ```proof (cases "q = 0") ``` chaieb@31761 ` 216` ``` case True then show C using 0 by auto ``` chaieb@31761 ` 217` ```next ``` chaieb@31761 ` 218` ``` case False ``` chaieb@31761 ` 219` ``` then obtain a b where "q = Fract a b" and "b \ 0" by (cases q) auto ``` chaieb@31761 ` 220` ``` moreover with False have "0 \ Fract a b" by simp ``` chaieb@31761 ` 221` ``` with `b \ 0` have "a \ 0" by (simp add: Zero_fract_def eq_fract) ``` chaieb@31761 ` 222` ``` with Fract `q = Fract a b` `b \ 0` show C by auto ``` chaieb@31761 ` 223` ```qed ``` chaieb@31761 ` 224` ``` ``` chaieb@31761 ` 225` chaieb@31761 ` 226` chaieb@31761 ` 227` ```subsubsection {* The field of rational numbers *} ``` chaieb@31761 ` 228` chaieb@31761 ` 229` ```context idom ``` chaieb@31761 ` 230` ```begin ``` chaieb@31761 ` 231` ```subclass ring_no_zero_divisors .. ``` chaieb@31761 ` 232` ```thm mult_eq_0_iff ``` chaieb@31761 ` 233` ```end ``` chaieb@31761 ` 234` haftmann@36409 ` 235` ```instantiation fract :: (idom) field_inverse_zero ``` chaieb@31761 ` 236` ```begin ``` chaieb@31761 ` 237` chaieb@31761 ` 238` ```definition ``` haftmann@37765 ` 239` ``` inverse_fract_def: ``` chaieb@31761 ` 240` ``` "inverse q = Abs_fract (\x \ Rep_fract q. ``` chaieb@31761 ` 241` ``` fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" ``` chaieb@31761 ` 242` chaieb@31761 ` 243` chaieb@31761 ` 244` ```lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a" ``` chaieb@31761 ` 245` ```proof - ``` chaieb@31761 ` 246` ``` have stupid: "\x. (0::'a) = x \ x = 0" by auto ``` chaieb@31761 ` 247` ``` have "(\x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" ``` chaieb@31761 ` 248` ``` by (auto simp add: congruent_def stupid algebra_simps) ``` chaieb@31761 ` 249` ``` then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel) ``` chaieb@31761 ` 250` ```qed ``` chaieb@31761 ` 251` chaieb@31761 ` 252` ```definition ``` haftmann@37765 ` 253` ``` divide_fract_def: "q / r = q * inverse (r:: 'a fract)" ``` chaieb@31761 ` 254` chaieb@31761 ` 255` ```lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" ``` chaieb@31761 ` 256` ``` by (simp add: divide_fract_def) ``` chaieb@31761 ` 257` chaieb@31761 ` 258` ```instance proof ``` chaieb@31761 ` 259` ``` fix q :: "'a fract" ``` chaieb@31761 ` 260` ``` assume "q \ 0" ``` chaieb@31761 ` 261` ``` then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero) ``` chaieb@31761 ` 262` ``` by (simp_all add: mult_fract inverse_fract fract_expand eq_fract mult_commute) ``` chaieb@31761 ` 263` ```next ``` chaieb@31761 ` 264` ``` fix q r :: "'a fract" ``` chaieb@31761 ` 265` ``` show "q / r = q * inverse r" by (simp add: divide_fract_def) ``` haftmann@36409 ` 266` ```next ``` haftmann@36409 ` 267` ``` show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand) ``` haftmann@36409 ` 268` ``` (simp add: fract_collapse) ``` chaieb@31761 ` 269` ```qed ``` chaieb@31761 ` 270` chaieb@31761 ` 271` ```end ``` chaieb@31761 ` 272` chaieb@31761 ` 273` huffman@36331 ` 274` ```subsubsection {* The ordered field of fractions over an ordered idom *} ``` huffman@36331 ` 275` huffman@36331 ` 276` ```lemma le_congruent2: ``` huffman@36331 ` 277` ``` "(\x y::'a \ 'a::linordered_idom. ``` huffman@36331 ` 278` ``` {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)}) ``` huffman@36331 ` 279` ``` respects2 fractrel" ``` huffman@36331 ` 280` ```proof (clarsimp simp add: congruent2_def) ``` huffman@36331 ` 281` ``` fix a b a' b' c d c' d' :: 'a ``` huffman@36331 ` 282` ``` assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" ``` huffman@36331 ` 283` ``` assume eq1: "a * b' = a' * b" ``` huffman@36331 ` 284` ``` assume eq2: "c * d' = c' * d" ``` huffman@36331 ` 285` huffman@36331 ` 286` ``` let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" ``` huffman@36331 ` 287` ``` { ``` huffman@36331 ` 288` ``` fix a b c d x :: 'a assume x: "x \ 0" ``` huffman@36331 ` 289` ``` have "?le a b c d = ?le (a * x) (b * x) c d" ``` huffman@36331 ` 290` ``` proof - ``` huffman@36331 ` 291` ``` from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 292` ``` hence "?le a b c d = ``` huffman@36331 ` 293` ``` ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" ``` huffman@36331 ` 294` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 295` ``` also have "... = ?le (a * x) (b * x) c d" ``` huffman@36331 ` 296` ``` by (simp add: mult_ac) ``` huffman@36331 ` 297` ``` finally show ?thesis . ``` huffman@36331 ` 298` ``` qed ``` huffman@36331 ` 299` ``` } note le_factor = this ``` huffman@36331 ` 300` huffman@36331 ` 301` ``` let ?D = "b * d" and ?D' = "b' * d'" ``` huffman@36331 ` 302` ``` from neq have D: "?D \ 0" by simp ``` huffman@36331 ` 303` ``` from neq have "?D' \ 0" by simp ``` huffman@36331 ` 304` ``` hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" ``` huffman@36331 ` 305` ``` by (rule le_factor) ``` huffman@36331 ` 306` ``` also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" ``` huffman@36331 ` 307` ``` by (simp add: mult_ac) ``` huffman@36331 ` 308` ``` also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" ``` huffman@36331 ` 309` ``` by (simp only: eq1 eq2) ``` huffman@36331 ` 310` ``` also have "... = ?le (a' * ?D) (b' * ?D) c' d'" ``` huffman@36331 ` 311` ``` by (simp add: mult_ac) ``` huffman@36331 ` 312` ``` also from D have "... = ?le a' b' c' d'" ``` huffman@36331 ` 313` ``` by (rule le_factor [symmetric]) ``` huffman@36331 ` 314` ``` finally show "?le a b c d = ?le a' b' c' d'" . ``` huffman@36331 ` 315` ```qed ``` huffman@36331 ` 316` huffman@36331 ` 317` ```instantiation fract :: (linordered_idom) linorder ``` huffman@36331 ` 318` ```begin ``` huffman@36331 ` 319` huffman@36331 ` 320` ```definition ``` haftmann@37765 ` 321` ``` le_fract_def: ``` haftmann@39910 ` 322` ``` "q \ r \ the_elem (\x \ Rep_fract q. \y \ Rep_fract r. ``` huffman@36331 ` 323` ``` {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)})" ``` huffman@36331 ` 324` huffman@36331 ` 325` ```definition ``` haftmann@37765 ` 326` ``` less_fract_def: "z < (w::'a fract) \ z \ w \ \ w \ z" ``` huffman@36331 ` 327` huffman@36331 ` 328` ```lemma le_fract [simp]: ``` huffman@36331 ` 329` ``` assumes "b \ 0" and "d \ 0" ``` huffman@36331 ` 330` ``` shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 331` ```by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) ``` huffman@36331 ` 332` huffman@36331 ` 333` ```lemma less_fract [simp]: ``` huffman@36331 ` 334` ``` assumes "b \ 0" and "d \ 0" ``` huffman@36331 ` 335` ``` shows "Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)" ``` huffman@36331 ` 336` ```by (simp add: less_fract_def less_le_not_le mult_ac assms) ``` huffman@36331 ` 337` huffman@36331 ` 338` ```instance proof ``` huffman@36331 ` 339` ``` fix q r s :: "'a fract" ``` huffman@36331 ` 340` ``` assume "q \ r" and "r \ s" thus "q \ s" ``` huffman@36331 ` 341` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 342` ``` fix a b c d e f :: 'a ``` huffman@36331 ` 343` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 344` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f" ``` huffman@36331 ` 345` ``` show "Fract a b \ Fract e f" ``` huffman@36331 ` 346` ``` proof - ``` huffman@36331 ` 347` ``` from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" ``` huffman@36331 ` 348` ``` by (auto simp add: zero_less_mult_iff linorder_neq_iff) ``` huffman@36331 ` 349` ``` have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" ``` huffman@36331 ` 350` ``` proof - ``` huffman@36331 ` 351` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 352` ``` by simp ``` huffman@36331 ` 353` ``` with ff show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 354` ``` qed ``` huffman@36331 ` 355` ``` also have "... = (c * f) * (d * f) * (b * b)" ``` huffman@36331 ` 356` ``` by (simp only: mult_ac) ``` huffman@36331 ` 357` ``` also have "... \ (e * d) * (d * f) * (b * b)" ``` huffman@36331 ` 358` ``` proof - ``` huffman@36331 ` 359` ``` from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" ``` huffman@36331 ` 360` ``` by simp ``` huffman@36331 ` 361` ``` with bb show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 362` ``` qed ``` huffman@36331 ` 363` ``` finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" ``` huffman@36331 ` 364` ``` by (simp only: mult_ac) ``` huffman@36331 ` 365` ``` with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" ``` huffman@36331 ` 366` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 367` ``` with neq show ?thesis by simp ``` huffman@36331 ` 368` ``` qed ``` huffman@36331 ` 369` ``` qed ``` huffman@36331 ` 370` ```next ``` huffman@36331 ` 371` ``` fix q r :: "'a fract" ``` huffman@36331 ` 372` ``` assume "q \ r" and "r \ q" thus "q = r" ``` huffman@36331 ` 373` ``` proof (induct q, induct r) ``` huffman@36331 ` 374` ``` fix a b c d :: 'a ``` huffman@36331 ` 375` ``` assume neq: "b \ 0" "d \ 0" ``` huffman@36331 ` 376` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b" ``` huffman@36331 ` 377` ``` show "Fract a b = Fract c d" ``` huffman@36331 ` 378` ``` proof - ``` huffman@36331 ` 379` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 380` ``` by simp ``` huffman@36331 ` 381` ``` also have "... \ (a * d) * (b * d)" ``` huffman@36331 ` 382` ``` proof - ``` huffman@36331 ` 383` ``` from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" ``` huffman@36331 ` 384` ``` by simp ``` huffman@36331 ` 385` ``` thus ?thesis by (simp only: mult_ac) ``` huffman@36331 ` 386` ``` qed ``` huffman@36331 ` 387` ``` finally have "(a * d) * (b * d) = (c * b) * (b * d)" . ``` huffman@36331 ` 388` ``` moreover from neq have "b * d \ 0" by simp ``` huffman@36331 ` 389` ``` ultimately have "a * d = c * b" by simp ``` huffman@36331 ` 390` ``` with neq show ?thesis by (simp add: eq_fract) ``` huffman@36331 ` 391` ``` qed ``` huffman@36331 ` 392` ``` qed ``` huffman@36331 ` 393` ```next ``` huffman@36331 ` 394` ``` fix q r :: "'a fract" ``` huffman@36331 ` 395` ``` show "q \ q" ``` huffman@36331 ` 396` ``` by (induct q) simp ``` huffman@36331 ` 397` ``` show "(q < r) = (q \ r \ \ r \ q)" ``` huffman@36331 ` 398` ``` by (simp only: less_fract_def) ``` huffman@36331 ` 399` ``` show "q \ r \ r \ q" ``` huffman@36331 ` 400` ``` by (induct q, induct r) ``` huffman@36331 ` 401` ``` (simp add: mult_commute, rule linorder_linear) ``` huffman@36331 ` 402` ```qed ``` huffman@36331 ` 403` huffman@36331 ` 404` ```end ``` huffman@36331 ` 405` huffman@36331 ` 406` ```instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}" ``` huffman@36331 ` 407` ```begin ``` huffman@36331 ` 408` huffman@36331 ` 409` ```definition ``` huffman@36331 ` 410` ``` abs_fract_def: "\q\ = (if q < 0 then -q else (q::'a fract))" ``` huffman@36331 ` 411` huffman@36331 ` 412` ```definition ``` huffman@36331 ` 413` ``` sgn_fract_def: ``` huffman@36331 ` 414` ``` "sgn (q::'a fract) = (if q=0 then 0 else if 0Fract a b\ = Fract \a\ \b\" ``` huffman@36331 ` 417` ``` by (auto simp add: abs_fract_def Zero_fract_def le_less ``` huffman@36331 ` 418` ``` eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) ``` huffman@36331 ` 419` huffman@36331 ` 420` ```definition ``` huffman@36331 ` 421` ``` inf_fract_def: ``` huffman@36331 ` 422` ``` "(inf \ 'a fract \ 'a fract \ 'a fract) = min" ``` huffman@36331 ` 423` huffman@36331 ` 424` ```definition ``` huffman@36331 ` 425` ``` sup_fract_def: ``` huffman@36331 ` 426` ``` "(sup \ 'a fract \ 'a fract \ 'a fract) = max" ``` huffman@36331 ` 427` huffman@36331 ` 428` ```instance by intro_classes ``` huffman@36331 ` 429` ``` (auto simp add: abs_fract_def sgn_fract_def ``` huffman@36331 ` 430` ``` min_max.sup_inf_distrib1 inf_fract_def sup_fract_def) ``` huffman@36331 ` 431` huffman@36331 ` 432` ```end ``` huffman@36331 ` 433` haftmann@36414 ` 434` ```instance fract :: (linordered_idom) linordered_field_inverse_zero ``` huffman@36331 ` 435` ```proof ``` huffman@36331 ` 436` ``` fix q r s :: "'a fract" ``` huffman@36331 ` 437` ``` show "q \ r ==> s + q \ s + r" ``` huffman@36331 ` 438` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 439` ``` fix a b c d e f :: 'a ``` huffman@36331 ` 440` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 441` ``` assume le: "Fract a b \ Fract c d" ``` huffman@36331 ` 442` ``` show "Fract e f + Fract a b \ Fract e f + Fract c d" ``` huffman@36331 ` 443` ``` proof - ``` huffman@36331 ` 444` ``` let ?F = "f * f" from neq have F: "0 < ?F" ``` huffman@36331 ` 445` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 446` ``` from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 447` ``` by simp ``` huffman@36331 ` 448` ``` with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" ``` huffman@36331 ` 449` ``` by (simp add: mult_le_cancel_right) ``` haftmann@36348 ` 450` ``` with neq show ?thesis by (simp add: field_simps) ``` huffman@36331 ` 451` ``` qed ``` huffman@36331 ` 452` ``` qed ``` huffman@36331 ` 453` ``` show "q < r ==> 0 < s ==> s * q < s * r" ``` huffman@36331 ` 454` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 455` ``` fix a b c d e f :: 'a ``` huffman@36331 ` 456` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 457` ``` assume le: "Fract a b < Fract c d" ``` huffman@36331 ` 458` ``` assume gt: "0 < Fract e f" ``` huffman@36331 ` 459` ``` show "Fract e f * Fract a b < Fract e f * Fract c d" ``` huffman@36331 ` 460` ``` proof - ``` huffman@36331 ` 461` ``` let ?E = "e * f" and ?F = "f * f" ``` huffman@36331 ` 462` ``` from neq gt have "0 < ?E" ``` huffman@36331 ` 463` ``` by (auto simp add: Zero_fract_def order_less_le eq_fract) ``` huffman@36331 ` 464` ``` moreover from neq have "0 < ?F" ``` huffman@36331 ` 465` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 466` ``` moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" ``` huffman@36331 ` 467` ``` by simp ``` huffman@36331 ` 468` ``` ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" ``` huffman@36331 ` 469` ``` by (simp add: mult_less_cancel_right) ``` huffman@36331 ` 470` ``` with neq show ?thesis ``` huffman@36331 ` 471` ``` by (simp add: mult_ac) ``` huffman@36331 ` 472` ``` qed ``` huffman@36331 ` 473` ``` qed ``` huffman@36331 ` 474` ```qed ``` huffman@36331 ` 475` huffman@36331 ` 476` ```lemma fract_induct_pos [case_names Fract]: ``` huffman@36331 ` 477` ``` fixes P :: "'a::linordered_idom fract \ bool" ``` huffman@36331 ` 478` ``` assumes step: "\a b. 0 < b \ P (Fract a b)" ``` huffman@36331 ` 479` ``` shows "P q" ``` huffman@36331 ` 480` ```proof (cases q) ``` huffman@36331 ` 481` ``` have step': "\a b. b < 0 \ P (Fract a b)" ``` huffman@36331 ` 482` ``` proof - ``` huffman@36331 ` 483` ``` fix a::'a and b::'a ``` huffman@36331 ` 484` ``` assume b: "b < 0" ``` huffman@36331 ` 485` ``` hence "0 < -b" by simp ``` huffman@36331 ` 486` ``` hence "P (Fract (-a) (-b))" by (rule step) ``` huffman@36331 ` 487` ``` thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) ``` huffman@36331 ` 488` ``` qed ``` huffman@36331 ` 489` ``` case (Fract a b) ``` huffman@36331 ` 490` ``` thus "P q" by (force simp add: linorder_neq_iff step step') ``` huffman@36331 ` 491` ```qed ``` huffman@36331 ` 492` huffman@36331 ` 493` ```lemma zero_less_Fract_iff: ``` huffman@36331 ` 494` ``` "0 < b \ 0 < Fract a b \ 0 < a" ``` huffman@36331 ` 495` ``` by (auto simp add: Zero_fract_def zero_less_mult_iff) ``` huffman@36331 ` 496` huffman@36331 ` 497` ```lemma Fract_less_zero_iff: ``` huffman@36331 ` 498` ``` "0 < b \ Fract a b < 0 \ a < 0" ``` huffman@36331 ` 499` ``` by (auto simp add: Zero_fract_def mult_less_0_iff) ``` huffman@36331 ` 500` huffman@36331 ` 501` ```lemma zero_le_Fract_iff: ``` huffman@36331 ` 502` ``` "0 < b \ 0 \ Fract a b \ 0 \ a" ``` huffman@36331 ` 503` ``` by (auto simp add: Zero_fract_def zero_le_mult_iff) ``` huffman@36331 ` 504` huffman@36331 ` 505` ```lemma Fract_le_zero_iff: ``` huffman@36331 ` 506` ``` "0 < b \ Fract a b \ 0 \ a \ 0" ``` huffman@36331 ` 507` ``` by (auto simp add: Zero_fract_def mult_le_0_iff) ``` huffman@36331 ` 508` huffman@36331 ` 509` ```lemma one_less_Fract_iff: ``` huffman@36331 ` 510` ``` "0 < b \ 1 < Fract a b \ b < a" ``` huffman@36331 ` 511` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 512` huffman@36331 ` 513` ```lemma Fract_less_one_iff: ``` huffman@36331 ` 514` ``` "0 < b \ Fract a b < 1 \ a < b" ``` huffman@36331 ` 515` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 516` huffman@36331 ` 517` ```lemma one_le_Fract_iff: ``` huffman@36331 ` 518` ``` "0 < b \ 1 \ Fract a b \ b \ a" ``` huffman@36331 ` 519` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 520` huffman@36331 ` 521` ```lemma Fract_le_one_iff: ``` huffman@36331 ` 522` ``` "0 < b \ Fract a b \ 1 \ a \ b" ``` huffman@36331 ` 523` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 524` huffman@36331 ` 525` ```end ```