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