src/HOL/Library/Fraction_Field.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 53374 a14d2a854c02 child 54230 b1d955791529 permissions -rw-r--r--
prefer Code.abort over code_abort
 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" ``` 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" ``` 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` 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` 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 ``` chaieb@31761 ` 62` ``` then show "fractrel `` {(0::'a, 1)} \ {x. snd x \ 0} // fractrel" by (rule quotientI) ``` chaieb@31761 ` 63` ```qed ``` chaieb@31761 ` 64` chaieb@31761 ` 65` ```lemma fractrel_in_fract [simp]: "snd x \ 0 \ fractrel `` {x} \ fract" ``` chaieb@31761 ` 66` ``` by (simp add: fract_def quotientI) ``` chaieb@31761 ` 67` chaieb@31761 ` 68` ```declare Abs_fract_inject [simp] Abs_fract_inverse [simp] ``` chaieb@31761 ` 69` chaieb@31761 ` 70` chaieb@31761 ` 71` ```subsubsection {* Representation and basic operations *} ``` chaieb@31761 ` 72` wenzelm@46573 ` 73` ```definition Fract :: "'a::idom \ 'a \ 'a fract" where ``` haftmann@37765 ` 74` ``` "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})" ``` chaieb@31761 ` 75` chaieb@31761 ` 76` ```code_datatype Fract ``` chaieb@31761 ` 77` wenzelm@53196 ` 78` ```lemma Fract_cases [cases type: fract]: ``` wenzelm@53196 ` 79` ``` obtains (Fract) a b where "q = Fract a b" "b \ 0" ``` wenzelm@53196 ` 80` ``` by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def) ``` chaieb@31761 ` 81` chaieb@31761 ` 82` ```lemma Fract_induct [case_names Fract, induct type: fract]: ``` wenzelm@53196 ` 83` ``` shows "(\a b. b \ 0 \ P (Fract a b)) \ P q" ``` wenzelm@53196 ` 84` ``` 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" ``` wenzelm@53196 ` 88` ``` and "\a. Fract a 0 = Fract 0 1" ``` wenzelm@53196 ` 89` ``` and "\a c. Fract 0 a = Fract 0 c" ``` chaieb@31761 ` 90` ``` by (simp_all add: Fract_def) ``` chaieb@31761 ` 91` wenzelm@53196 ` 92` ```instantiation fract :: (idom) "{comm_ring_1,power}" ``` chaieb@31761 ` 93` ```begin ``` chaieb@31761 ` 94` wenzelm@46573 ` 95` ```definition Zero_fract_def [code_unfold]: "0 = Fract 0 1" ``` chaieb@31761 ` 96` wenzelm@46573 ` 97` ```definition One_fract_def [code_unfold]: "1 = Fract 1 1" ``` chaieb@31761 ` 98` wenzelm@46573 ` 99` ```definition add_fract_def: ``` chaieb@31761 ` 100` ``` "q + r = Abs_fract (\x \ Rep_fract q. \y \ Rep_fract r. ``` chaieb@31761 ` 101` ``` fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" ``` chaieb@31761 ` 102` chaieb@31761 ` 103` ```lemma add_fract [simp]: ``` wenzelm@53196 ` 104` ``` assumes "b \ (0::'a::idom)" ``` wenzelm@53196 ` 105` ``` and "d \ 0" ``` chaieb@31761 ` 106` ``` shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" ``` chaieb@31761 ` 107` ```proof - ``` chaieb@31761 ` 108` ``` have "(\x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)}) ``` chaieb@31761 ` 109` ``` respects2 fractrel" ``` wenzelm@53196 ` 110` ``` apply (rule equiv_fractrel [THEN congruent2_commuteI]) ``` wenzelm@53196 ` 111` ``` apply (auto simp add: algebra_simps) ``` wenzelm@53196 ` 112` ``` unfolding mult_assoc[symmetric] ``` wenzelm@53196 ` 113` ``` done ``` chaieb@31761 ` 114` ``` with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2) ``` chaieb@31761 ` 115` ```qed ``` chaieb@31761 ` 116` wenzelm@46573 ` 117` ```definition minus_fract_def: ``` chaieb@31761 ` 118` ``` "- q = Abs_fract (\x \ Rep_fract q. fractrel `` {(- fst x, snd x)})" ``` chaieb@31761 ` 119` chaieb@31761 ` 120` ```lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)" ``` chaieb@31761 ` 121` ```proof - ``` chaieb@31761 ` 122` ``` have "(\x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel" ``` haftmann@40822 ` 123` ``` by (simp add: congruent_def split_paired_all) ``` chaieb@31761 ` 124` ``` then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel) ``` chaieb@31761 ` 125` ```qed ``` chaieb@31761 ` 126` chaieb@31761 ` 127` ```lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b" ``` chaieb@31761 ` 128` ``` by (cases "b = 0") (simp_all add: eq_fract) ``` chaieb@31761 ` 129` wenzelm@46573 ` 130` ```definition diff_fract_def: "q - r = q + - (r::'a fract)" ``` chaieb@31761 ` 131` chaieb@31761 ` 132` ```lemma diff_fract [simp]: ``` chaieb@31761 ` 133` ``` assumes "b \ 0" and "d \ 0" ``` chaieb@31761 ` 134` ``` shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" ``` chaieb@31761 ` 135` ``` using assms by (simp add: diff_fract_def diff_minus) ``` 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@53196 ` 144` ``` apply (rule equiv_fractrel [THEN congruent2_commuteI]) ``` wenzelm@53196 ` 145` ``` apply (auto simp add: algebra_simps) ``` wenzelm@53196 ` 146` ``` done ``` chaieb@31761 ` 147` ``` then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2) ``` chaieb@31761 ` 148` ```qed ``` chaieb@31761 ` 149` chaieb@31761 ` 150` ```lemma mult_fract_cancel: ``` wenzelm@47252 ` 151` ``` assumes "c \ (0::'a)" ``` chaieb@31761 ` 152` ``` shows "Fract (c * a) (c * b) = Fract a b" ``` chaieb@31761 ` 153` ```proof - ``` chaieb@31761 ` 154` ``` from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) ``` chaieb@31761 ` 155` ``` then show ?thesis 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@53196 ` 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@53196 ` 204` ``` obtains (Fract) a b where "q = Fract a b" "b \ 0" "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 ``` chaieb@31761 ` 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@53196 ` 236` ``` have *: "\x. (0::'a) = x \ x = 0" by auto ``` chaieb@31761 ` 237` ``` have "(\x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel" ``` wenzelm@53196 ` 238` ``` by (auto simp add: congruent_def * algebra_simps) ``` chaieb@31761 ` 239` ``` then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel) ``` chaieb@31761 ` 240` ```qed ``` chaieb@31761 ` 241` wenzelm@46573 ` 242` ```definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)" ``` chaieb@31761 ` 243` chaieb@31761 ` 244` ```lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" ``` chaieb@31761 ` 245` ``` by (simp add: divide_fract_def) ``` chaieb@31761 ` 246` wenzelm@47252 ` 247` ```instance ``` wenzelm@47252 ` 248` ```proof ``` chaieb@31761 ` 249` ``` fix q :: "'a fract" ``` chaieb@31761 ` 250` ``` assume "q \ 0" ``` wenzelm@46573 ` 251` ``` then show "inverse q * q = 1" ``` wenzelm@46573 ` 252` ``` by (cases q rule: Fract_cases_nonzero) ``` wenzelm@46573 ` 253` ``` (simp_all add: fract_expand eq_fract mult_commute) ``` chaieb@31761 ` 254` ```next ``` chaieb@31761 ` 255` ``` fix q r :: "'a fract" ``` chaieb@31761 ` 256` ``` show "q / r = q * inverse r" by (simp add: divide_fract_def) ``` haftmann@36409 ` 257` ```next ``` wenzelm@46573 ` 258` ``` show "inverse 0 = (0:: 'a fract)" ``` wenzelm@46573 ` 259` ``` by (simp add: fract_expand) (simp add: fract_collapse) ``` chaieb@31761 ` 260` ```qed ``` chaieb@31761 ` 261` chaieb@31761 ` 262` ```end ``` chaieb@31761 ` 263` chaieb@31761 ` 264` huffman@36331 ` 265` ```subsubsection {* The ordered field of fractions over an ordered idom *} ``` huffman@36331 ` 266` huffman@36331 ` 267` ```lemma le_congruent2: ``` huffman@36331 ` 268` ``` "(\x y::'a \ 'a::linordered_idom. ``` huffman@36331 ` 269` ``` {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)}) ``` huffman@36331 ` 270` ``` respects2 fractrel" ``` huffman@36331 ` 271` ```proof (clarsimp simp add: congruent2_def) ``` huffman@36331 ` 272` ``` fix a b a' b' c d c' d' :: 'a ``` huffman@36331 ` 273` ``` assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" ``` huffman@36331 ` 274` ``` assume eq1: "a * b' = a' * b" ``` huffman@36331 ` 275` ``` assume eq2: "c * d' = c' * d" ``` huffman@36331 ` 276` huffman@36331 ` 277` ``` let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" ``` huffman@36331 ` 278` ``` { ``` huffman@36331 ` 279` ``` fix a b c d x :: 'a assume x: "x \ 0" ``` huffman@36331 ` 280` ``` have "?le a b c d = ?le (a * x) (b * x) c d" ``` huffman@36331 ` 281` ``` proof - ``` huffman@36331 ` 282` ``` from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) ``` wenzelm@46573 ` 283` ``` then have "?le a b c d = ``` huffman@36331 ` 284` ``` ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" ``` huffman@36331 ` 285` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 286` ``` also have "... = ?le (a * x) (b * x) c d" ``` huffman@36331 ` 287` ``` by (simp add: mult_ac) ``` huffman@36331 ` 288` ``` finally show ?thesis . ``` huffman@36331 ` 289` ``` qed ``` huffman@36331 ` 290` ``` } note le_factor = this ``` huffman@36331 ` 291` huffman@36331 ` 292` ``` let ?D = "b * d" and ?D' = "b' * d'" ``` huffman@36331 ` 293` ``` from neq have D: "?D \ 0" by simp ``` huffman@36331 ` 294` ``` from neq have "?D' \ 0" by simp ``` wenzelm@46573 ` 295` ``` then have "?le a b c d = ?le (a * ?D') (b * ?D') c d" ``` huffman@36331 ` 296` ``` by (rule le_factor) ``` huffman@36331 ` 297` ``` also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" ``` huffman@36331 ` 298` ``` by (simp add: mult_ac) ``` huffman@36331 ` 299` ``` also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" ``` huffman@36331 ` 300` ``` by (simp only: eq1 eq2) ``` huffman@36331 ` 301` ``` also have "... = ?le (a' * ?D) (b' * ?D) c' d'" ``` huffman@36331 ` 302` ``` by (simp add: mult_ac) ``` huffman@36331 ` 303` ``` also from D have "... = ?le a' b' c' d'" ``` huffman@36331 ` 304` ``` by (rule le_factor [symmetric]) ``` huffman@36331 ` 305` ``` finally show "?le a b c d = ?le a' b' c' d'" . ``` huffman@36331 ` 306` ```qed ``` huffman@36331 ` 307` huffman@36331 ` 308` ```instantiation fract :: (linordered_idom) linorder ``` huffman@36331 ` 309` ```begin ``` huffman@36331 ` 310` wenzelm@46573 ` 311` ```definition le_fract_def: ``` wenzelm@53196 ` 312` ``` "q \ r \ the_elem (\x \ Rep_fract q. \y \ Rep_fract r. ``` wenzelm@53196 ` 313` ``` {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)})" ``` huffman@36331 ` 314` wenzelm@46573 ` 315` ```definition less_fract_def: "z < (w::'a fract) \ z \ w \ \ w \ z" ``` huffman@36331 ` 316` huffman@36331 ` 317` ```lemma le_fract [simp]: ``` huffman@36331 ` 318` ``` assumes "b \ 0" and "d \ 0" ``` huffman@36331 ` 319` ``` shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" ``` wenzelm@53196 ` 320` ``` by (simp add: Fract_def le_fract_def le_congruent2 UN_fractrel2 assms) ``` huffman@36331 ` 321` huffman@36331 ` 322` ```lemma less_fract [simp]: ``` huffman@36331 ` 323` ``` assumes "b \ 0" 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: less_fract_def less_le_not_le mult_ac assms) ``` huffman@36331 ` 326` wenzelm@47252 ` 327` ```instance ``` wenzelm@47252 ` 328` ```proof ``` huffman@36331 ` 329` ``` fix q r s :: "'a fract" ``` huffman@36331 ` 330` ``` assume "q \ r" and "r \ s" thus "q \ s" ``` huffman@36331 ` 331` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 332` ``` fix a b c d e f :: 'a ``` huffman@36331 ` 333` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 334` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f" ``` huffman@36331 ` 335` ``` show "Fract a b \ Fract e f" ``` huffman@36331 ` 336` ``` proof - ``` huffman@36331 ` 337` ``` from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" ``` huffman@36331 ` 338` ``` by (auto simp add: zero_less_mult_iff linorder_neq_iff) ``` huffman@36331 ` 339` ``` have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" ``` huffman@36331 ` 340` ``` proof - ``` huffman@36331 ` 341` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 342` ``` by simp ``` huffman@36331 ` 343` ``` with ff show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 344` ``` qed ``` huffman@36331 ` 345` ``` also have "... = (c * f) * (d * f) * (b * b)" ``` huffman@36331 ` 346` ``` by (simp only: mult_ac) ``` huffman@36331 ` 347` ``` also have "... \ (e * d) * (d * f) * (b * b)" ``` huffman@36331 ` 348` ``` proof - ``` huffman@36331 ` 349` ``` from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" ``` huffman@36331 ` 350` ``` by simp ``` huffman@36331 ` 351` ``` with bb show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 352` ``` qed ``` huffman@36331 ` 353` ``` finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" ``` huffman@36331 ` 354` ``` by (simp only: mult_ac) ``` huffman@36331 ` 355` ``` with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" ``` huffman@36331 ` 356` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 357` ``` with neq show ?thesis by simp ``` huffman@36331 ` 358` ``` qed ``` huffman@36331 ` 359` ``` qed ``` huffman@36331 ` 360` ```next ``` huffman@36331 ` 361` ``` fix q r :: "'a fract" ``` huffman@36331 ` 362` ``` assume "q \ r" and "r \ q" thus "q = r" ``` huffman@36331 ` 363` ``` proof (induct q, induct r) ``` huffman@36331 ` 364` ``` fix a b c d :: 'a ``` huffman@36331 ` 365` ``` assume neq: "b \ 0" "d \ 0" ``` huffman@36331 ` 366` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b" ``` huffman@36331 ` 367` ``` show "Fract a b = Fract c d" ``` huffman@36331 ` 368` ``` proof - ``` huffman@36331 ` 369` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 370` ``` by simp ``` huffman@36331 ` 371` ``` also have "... \ (a * d) * (b * d)" ``` huffman@36331 ` 372` ``` proof - ``` huffman@36331 ` 373` ``` from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" ``` huffman@36331 ` 374` ``` by simp ``` huffman@36331 ` 375` ``` thus ?thesis by (simp only: mult_ac) ``` huffman@36331 ` 376` ``` qed ``` huffman@36331 ` 377` ``` finally have "(a * d) * (b * d) = (c * b) * (b * d)" . ``` huffman@36331 ` 378` ``` moreover from neq have "b * d \ 0" by simp ``` huffman@36331 ` 379` ``` ultimately have "a * d = c * b" by simp ``` huffman@36331 ` 380` ``` with neq show ?thesis by (simp add: eq_fract) ``` huffman@36331 ` 381` ``` qed ``` huffman@36331 ` 382` ``` qed ``` huffman@36331 ` 383` ```next ``` huffman@36331 ` 384` ``` fix q r :: "'a fract" ``` huffman@36331 ` 385` ``` show "q \ q" ``` huffman@36331 ` 386` ``` by (induct q) simp ``` huffman@36331 ` 387` ``` show "(q < r) = (q \ r \ \ r \ q)" ``` huffman@36331 ` 388` ``` by (simp only: less_fract_def) ``` huffman@36331 ` 389` ``` show "q \ r \ r \ q" ``` huffman@36331 ` 390` ``` by (induct q, induct r) ``` huffman@36331 ` 391` ``` (simp add: mult_commute, rule linorder_linear) ``` huffman@36331 ` 392` ```qed ``` huffman@36331 ` 393` huffman@36331 ` 394` ```end ``` huffman@36331 ` 395` huffman@36331 ` 396` ```instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}" ``` huffman@36331 ` 397` ```begin ``` huffman@36331 ` 398` wenzelm@46573 ` 399` ```definition abs_fract_def: "\q\ = (if q < 0 then -q else (q::'a fract))" ``` huffman@36331 ` 400` wenzelm@46573 ` 401` ```definition sgn_fract_def: ``` wenzelm@46573 ` 402` ``` "sgn (q::'a fract) = (if q=0 then 0 else if 0Fract a b\ = Fract \a\ \b\" ``` huffman@36331 ` 405` ``` by (auto simp add: abs_fract_def Zero_fract_def le_less ``` huffman@36331 ` 406` ``` eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split) ``` huffman@36331 ` 407` wenzelm@46573 ` 408` ```definition inf_fract_def: ``` wenzelm@46573 ` 409` ``` "(inf \ 'a fract \ 'a fract \ 'a fract) = min" ``` huffman@36331 ` 410` wenzelm@46573 ` 411` ```definition sup_fract_def: ``` wenzelm@46573 ` 412` ``` "(sup \ 'a fract \ 'a fract \ 'a fract) = max" ``` huffman@36331 ` 413` wenzelm@46573 ` 414` ```instance ``` wenzelm@46573 ` 415` ``` by intro_classes ``` wenzelm@46573 ` 416` ``` (auto simp add: abs_fract_def sgn_fract_def ``` wenzelm@46573 ` 417` ``` min_max.sup_inf_distrib1 inf_fract_def sup_fract_def) ``` huffman@36331 ` 418` huffman@36331 ` 419` ```end ``` huffman@36331 ` 420` haftmann@36414 ` 421` ```instance fract :: (linordered_idom) linordered_field_inverse_zero ``` huffman@36331 ` 422` ```proof ``` huffman@36331 ` 423` ``` fix q r s :: "'a fract" ``` wenzelm@53196 ` 424` ``` assume "q \ r" ``` wenzelm@53196 ` 425` ``` then show "s + q \ s + r" ``` huffman@36331 ` 426` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 427` ``` fix a b c d e f :: 'a ``` wenzelm@53196 ` 428` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 429` ``` assume le: "Fract a b \ Fract c d" ``` huffman@36331 ` 430` ``` show "Fract e f + Fract a b \ Fract e f + Fract c d" ``` huffman@36331 ` 431` ``` proof - ``` huffman@36331 ` 432` ``` let ?F = "f * f" from neq have F: "0 < ?F" ``` huffman@36331 ` 433` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 434` ``` from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 435` ``` by simp ``` huffman@36331 ` 436` ``` with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" ``` huffman@36331 ` 437` ``` by (simp add: mult_le_cancel_right) ``` haftmann@36348 ` 438` ``` with neq show ?thesis by (simp add: field_simps) ``` huffman@36331 ` 439` ``` qed ``` huffman@36331 ` 440` ``` qed ``` wenzelm@53196 ` 441` ```next ``` wenzelm@53196 ` 442` ``` fix q r s :: "'a fract" ``` wenzelm@53196 ` 443` ``` assume "q < r" and "0 < s" ``` wenzelm@53196 ` 444` ``` then show "s * q < s * r" ``` huffman@36331 ` 445` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 446` ``` fix a b c d e f :: 'a ``` huffman@36331 ` 447` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 448` ``` assume le: "Fract a b < Fract c d" ``` huffman@36331 ` 449` ``` assume gt: "0 < Fract e f" ``` huffman@36331 ` 450` ``` show "Fract e f * Fract a b < Fract e f * Fract c d" ``` huffman@36331 ` 451` ``` proof - ``` huffman@36331 ` 452` ``` let ?E = "e * f" and ?F = "f * f" ``` huffman@36331 ` 453` ``` from neq gt have "0 < ?E" ``` huffman@36331 ` 454` ``` by (auto simp add: Zero_fract_def order_less_le eq_fract) ``` huffman@36331 ` 455` ``` moreover from neq have "0 < ?F" ``` huffman@36331 ` 456` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 457` ``` moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" ``` huffman@36331 ` 458` ``` by simp ``` huffman@36331 ` 459` ``` ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" ``` huffman@36331 ` 460` ``` by (simp add: mult_less_cancel_right) ``` huffman@36331 ` 461` ``` with neq show ?thesis ``` huffman@36331 ` 462` ``` by (simp add: mult_ac) ``` huffman@36331 ` 463` ``` qed ``` huffman@36331 ` 464` ``` qed ``` huffman@36331 ` 465` ```qed ``` huffman@36331 ` 466` huffman@36331 ` 467` ```lemma fract_induct_pos [case_names Fract]: ``` huffman@36331 ` 468` ``` fixes P :: "'a::linordered_idom fract \ bool" ``` huffman@36331 ` 469` ``` assumes step: "\a b. 0 < b \ P (Fract a b)" ``` huffman@36331 ` 470` ``` shows "P q" ``` huffman@36331 ` 471` ```proof (cases q) ``` huffman@36331 ` 472` ``` have step': "\a b. b < 0 \ P (Fract a b)" ``` huffman@36331 ` 473` ``` proof - ``` huffman@36331 ` 474` ``` fix a::'a and b::'a ``` huffman@36331 ` 475` ``` assume b: "b < 0" ``` wenzelm@46573 ` 476` ``` then have "0 < -b" by simp ``` wenzelm@46573 ` 477` ``` then have "P (Fract (-a) (-b))" by (rule step) ``` huffman@36331 ` 478` ``` thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) ``` huffman@36331 ` 479` ``` qed ``` huffman@36331 ` 480` ``` case (Fract a b) ``` huffman@36331 ` 481` ``` thus "P q" by (force simp add: linorder_neq_iff step step') ``` huffman@36331 ` 482` ```qed ``` huffman@36331 ` 483` wenzelm@53196 ` 484` ```lemma zero_less_Fract_iff: "0 < b \ 0 < Fract a b \ 0 < a" ``` huffman@36331 ` 485` ``` by (auto simp add: Zero_fract_def zero_less_mult_iff) ``` huffman@36331 ` 486` wenzelm@53196 ` 487` ```lemma Fract_less_zero_iff: "0 < b \ Fract a b < 0 \ a < 0" ``` huffman@36331 ` 488` ``` by (auto simp add: Zero_fract_def mult_less_0_iff) ``` huffman@36331 ` 489` wenzelm@53196 ` 490` ```lemma zero_le_Fract_iff: "0 < b \ 0 \ Fract a b \ 0 \ a" ``` huffman@36331 ` 491` ``` by (auto simp add: Zero_fract_def zero_le_mult_iff) ``` huffman@36331 ` 492` wenzelm@53196 ` 493` ```lemma Fract_le_zero_iff: "0 < b \ Fract a b \ 0 \ a \ 0" ``` huffman@36331 ` 494` ``` by (auto simp add: Zero_fract_def mult_le_0_iff) ``` huffman@36331 ` 495` wenzelm@53196 ` 496` ```lemma one_less_Fract_iff: "0 < b \ 1 < Fract a b \ b < a" ``` huffman@36331 ` 497` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 498` wenzelm@53196 ` 499` ```lemma Fract_less_one_iff: "0 < b \ Fract a b < 1 \ a < b" ``` huffman@36331 ` 500` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 501` wenzelm@53196 ` 502` ```lemma one_le_Fract_iff: "0 < b \ 1 \ Fract a b \ b \ a" ``` huffman@36331 ` 503` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 504` wenzelm@53196 ` 505` ```lemma Fract_le_one_iff: "0 < b \ Fract a b \ 1 \ a \ b" ``` huffman@36331 ` 506` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 507` huffman@36331 ` 508` ```end ```