src/HOL/Library/Fraction_Field.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61260 e6f03fae14d5 child 63092 a949b2a5f51d permissions -rw-r--r--
more symbols;
 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@60500 ` 5` ```section\A formalization of the fraction field of any integral domain; ``` wenzelm@60500 ` 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` wenzelm@60500 ` 12` ```subsection \General fractions construction\ ``` chaieb@31761 ` 13` wenzelm@60500 ` 14` ```subsubsection \Construction of the type of fractions\ ``` chaieb@31761 ` 15` Andreas@61106 ` 16` ```context idom begin ``` Andreas@61106 ` 17` Andreas@61106 ` 18` ```definition fractrel :: "'a \ 'a \ 'a * 'a \ bool" where ``` Andreas@61106 ` 19` ``` "fractrel = (\x y. snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x)" ``` chaieb@31761 ` 20` chaieb@31761 ` 21` ```lemma fractrel_iff [simp]: ``` Andreas@61106 ` 22` ``` "fractrel x y \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" ``` chaieb@31761 ` 23` ``` by (simp add: fractrel_def) ``` chaieb@31761 ` 24` Andreas@61106 ` 25` ```lemma symp_fractrel: "symp fractrel" ``` Andreas@61106 ` 26` ``` by (simp add: symp_def) ``` chaieb@31761 ` 27` Andreas@61106 ` 28` ```lemma transp_fractrel: "transp fractrel" ``` Andreas@61106 ` 29` ```proof (rule transpI, unfold split_paired_all) ``` chaieb@31761 ` 30` ``` fix a b a' b' a'' b'' :: 'a ``` Andreas@61106 ` 31` ``` assume A: "fractrel (a, b) (a', b')" ``` Andreas@61106 ` 32` ``` assume B: "fractrel (a', b') (a'', b'')" ``` haftmann@57514 ` 33` ``` have "b' * (a * b'') = b'' * (a * b')" by (simp add: ac_simps) ``` chaieb@31761 ` 34` ``` also from A have "a * b' = a' * b" by auto ``` haftmann@57514 ` 35` ``` also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: ac_simps) ``` chaieb@31761 ` 36` ``` also from B have "a' * b'' = a'' * b'" by auto ``` haftmann@57514 ` 37` ``` also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: ac_simps) ``` chaieb@31761 ` 38` ``` finally have "b' * (a * b'') = b' * (a'' * b)" . ``` chaieb@31761 ` 39` ``` moreover from B have "b' \ 0" by auto ``` chaieb@31761 ` 40` ``` ultimately have "a * b'' = a'' * b" by simp ``` Andreas@61106 ` 41` ``` with A B show "fractrel (a, b) (a'', b'')" by auto ``` chaieb@31761 ` 42` ```qed ``` wenzelm@54463 ` 43` Andreas@61106 ` 44` ```lemma part_equivp_fractrel: "part_equivp fractrel" ``` Andreas@61106 ` 45` ```using _ symp_fractrel transp_fractrel ``` Andreas@61106 ` 46` ```by(rule part_equivpI)(rule exI[where x="(0, 1)"]; simp) ``` wenzelm@45694 ` 47` Andreas@61106 ` 48` ```end ``` chaieb@31761 ` 49` wenzelm@61260 ` 50` ```quotient_type (overloaded) 'a fract = "'a :: idom \ 'a" / partial: "fractrel" ``` Andreas@61106 ` 51` ```by(rule part_equivp_fractrel) ``` chaieb@31761 ` 52` wenzelm@60500 ` 53` ```subsubsection \Representation and basic operations\ ``` chaieb@31761 ` 54` Andreas@61106 ` 55` ```lift_definition Fract :: "'a :: idom \ 'a \ 'a fract" ``` Andreas@61106 ` 56` ``` is "\a b. if b = 0 then (0, 1) else (a, b)" ``` Andreas@61106 ` 57` ``` by simp ``` chaieb@31761 ` 58` wenzelm@53196 ` 59` ```lemma Fract_cases [cases type: fract]: ``` wenzelm@53196 ` 60` ``` obtains (Fract) a b where "q = Fract a b" "b \ 0" ``` Andreas@61106 ` 61` ```by transfer simp ``` chaieb@31761 ` 62` chaieb@31761 ` 63` ```lemma Fract_induct [case_names Fract, induct type: fract]: ``` wenzelm@54463 ` 64` ``` "(\a b. b \ 0 \ P (Fract a b)) \ P q" ``` wenzelm@53196 ` 65` ``` by (cases q) simp ``` chaieb@31761 ` 66` chaieb@31761 ` 67` ```lemma eq_fract: ``` chaieb@31761 ` 68` ``` shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" ``` wenzelm@53196 ` 69` ``` and "\a. Fract a 0 = Fract 0 1" ``` wenzelm@53196 ` 70` ``` and "\a c. Fract 0 a = Fract 0 c" ``` Andreas@61106 ` 71` ```by(transfer; simp)+ ``` chaieb@31761 ` 72` wenzelm@53196 ` 73` ```instantiation fract :: (idom) "{comm_ring_1,power}" ``` chaieb@31761 ` 74` ```begin ``` chaieb@31761 ` 75` Andreas@61106 ` 76` ```lift_definition zero_fract :: "'a fract" is "(0, 1)" by simp ``` chaieb@31761 ` 77` Andreas@61106 ` 78` ```lemma Zero_fract_def: "0 = Fract 0 1" ``` Andreas@61106 ` 79` ```by transfer simp ``` Andreas@61106 ` 80` Andreas@61106 ` 81` ```lift_definition one_fract :: "'a fract" is "(1, 1)" by simp ``` chaieb@31761 ` 82` Andreas@61106 ` 83` ```lemma One_fract_def: "1 = Fract 1 1" ``` Andreas@61106 ` 84` ```by transfer simp ``` Andreas@61106 ` 85` Andreas@61106 ` 86` ```lift_definition plus_fract :: "'a fract \ 'a fract \ 'a fract" ``` Andreas@61106 ` 87` ``` is "\q r. (fst q * snd r + fst r * snd q, snd q * snd r)" ``` Andreas@61106 ` 88` ```by(auto simp add: algebra_simps) ``` chaieb@31761 ` 89` chaieb@31761 ` 90` ```lemma add_fract [simp]: ``` Andreas@61106 ` 91` ``` "\ b \ 0; d \ 0 \ \ Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" ``` Andreas@61106 ` 92` ```by transfer simp ``` chaieb@31761 ` 93` Andreas@61106 ` 94` ```lift_definition uminus_fract :: "'a fract \ 'a fract" ``` Andreas@61106 ` 95` ``` is "\x. (- fst x, snd x)" ``` Andreas@61106 ` 96` ```by simp ``` chaieb@31761 ` 97` Andreas@61106 ` 98` ```lemma minus_fract [simp]: ``` wenzelm@54463 ` 99` ``` fixes a b :: "'a::idom" ``` wenzelm@54463 ` 100` ``` shows "- Fract a b = Fract (- a) b" ``` Andreas@61106 ` 101` ```by transfer simp ``` chaieb@31761 ` 102` chaieb@31761 ` 103` ```lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b" ``` chaieb@31761 ` 104` ``` by (cases "b = 0") (simp_all add: eq_fract) ``` chaieb@31761 ` 105` wenzelm@46573 ` 106` ```definition diff_fract_def: "q - r = q + - (r::'a fract)" ``` chaieb@31761 ` 107` chaieb@31761 ` 108` ```lemma diff_fract [simp]: ``` Andreas@61106 ` 109` ``` "\ b \ 0; d \ 0 \ \ Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" ``` Andreas@61106 ` 110` ``` by (simp add: diff_fract_def) ``` chaieb@31761 ` 111` Andreas@61106 ` 112` ```lift_definition times_fract :: "'a fract \ 'a fract \ 'a fract" ``` Andreas@61106 ` 113` ``` is "\q r. (fst q * fst r, snd q * snd r)" ``` Andreas@61106 ` 114` ```by(simp add: algebra_simps) ``` chaieb@31761 ` 115` chaieb@31761 ` 116` ```lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)" ``` Andreas@61106 ` 117` ```by transfer simp ``` chaieb@31761 ` 118` chaieb@31761 ` 119` ```lemma mult_fract_cancel: ``` Andreas@61106 ` 120` ``` "c \ 0 \ Fract (c * a) (c * b) = Fract a b" ``` Andreas@61106 ` 121` ```by transfer simp ``` chaieb@31761 ` 122` wenzelm@47252 ` 123` ```instance ``` wenzelm@47252 ` 124` ```proof ``` wenzelm@53196 ` 125` ``` fix q r s :: "'a fract" ``` wenzelm@54463 ` 126` ``` show "(q * r) * s = q * (r * s)" ``` chaieb@31761 ` 127` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` wenzelm@53196 ` 128` ``` show "q * r = r * q" ``` chaieb@31761 ` 129` ``` by (cases q, cases r) (simp add: eq_fract algebra_simps) ``` wenzelm@53196 ` 130` ``` show "1 * q = q" ``` chaieb@31761 ` 131` ``` by (cases q) (simp add: One_fract_def eq_fract) ``` wenzelm@53196 ` 132` ``` show "(q + r) + s = q + (r + s)" ``` chaieb@31761 ` 133` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` wenzelm@53196 ` 134` ``` show "q + r = r + q" ``` chaieb@31761 ` 135` ``` by (cases q, cases r) (simp add: eq_fract algebra_simps) ``` wenzelm@53196 ` 136` ``` show "0 + q = q" ``` chaieb@31761 ` 137` ``` by (cases q) (simp add: Zero_fract_def eq_fract) ``` wenzelm@53196 ` 138` ``` show "- q + q = 0" ``` chaieb@31761 ` 139` ``` by (cases q) (simp add: Zero_fract_def eq_fract) ``` wenzelm@53196 ` 140` ``` show "q - r = q + - r" ``` chaieb@31761 ` 141` ``` by (cases q, cases r) (simp add: eq_fract) ``` wenzelm@53196 ` 142` ``` show "(q + r) * s = q * s + r * s" ``` chaieb@31761 ` 143` ``` by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) ``` wenzelm@53196 ` 144` ``` show "(0::'a fract) \ 1" ``` wenzelm@53196 ` 145` ``` by (simp add: Zero_fract_def One_fract_def eq_fract) ``` chaieb@31761 ` 146` ```qed ``` chaieb@31761 ` 147` chaieb@31761 ` 148` ```end ``` chaieb@31761 ` 149` chaieb@31761 ` 150` ```lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1" ``` chaieb@31761 ` 151` ``` by (induct k) (simp_all add: Zero_fract_def One_fract_def) ``` chaieb@31761 ` 152` chaieb@31761 ` 153` ```lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" ``` chaieb@31761 ` 154` ``` by (rule of_nat_fract [symmetric]) ``` chaieb@31761 ` 155` Andreas@61106 ` 156` ```lemma fract_collapse: ``` chaieb@31761 ` 157` ``` "Fract 0 k = 0" ``` chaieb@31761 ` 158` ``` "Fract 1 1 = 1" ``` chaieb@31761 ` 159` ``` "Fract k 0 = 0" ``` Andreas@61106 ` 160` ```by(transfer; simp)+ ``` chaieb@31761 ` 161` Andreas@61106 ` 162` ```lemma fract_expand: ``` chaieb@31761 ` 163` ``` "0 = Fract 0 1" ``` chaieb@31761 ` 164` ``` "1 = Fract 1 1" ``` chaieb@31761 ` 165` ``` by (simp_all add: fract_collapse) ``` chaieb@31761 ` 166` wenzelm@53196 ` 167` ```lemma Fract_cases_nonzero: ``` wenzelm@54463 ` 168` ``` obtains (Fract) a b where "q = Fract a b" and "b \ 0" and "a \ 0" ``` wenzelm@53196 ` 169` ``` | (0) "q = 0" ``` chaieb@31761 ` 170` ```proof (cases "q = 0") ``` wenzelm@53196 ` 171` ``` case True ``` wenzelm@53196 ` 172` ``` then show thesis using 0 by auto ``` chaieb@31761 ` 173` ```next ``` chaieb@31761 ` 174` ``` case False ``` chaieb@31761 ` 175` ``` then obtain a b where "q = Fract a b" and "b \ 0" by (cases q) auto ``` wenzelm@53374 ` 176` ``` with False have "0 \ Fract a b" by simp ``` wenzelm@60500 ` 177` ``` with \b \ 0\ have "a \ 0" by (simp add: Zero_fract_def eq_fract) ``` wenzelm@60500 ` 178` ``` with Fract \q = Fract a b\ \b \ 0\ show thesis by auto ``` chaieb@31761 ` 179` ```qed ``` wenzelm@54463 ` 180` chaieb@31761 ` 181` wenzelm@60500 ` 182` ```subsubsection \The field of rational numbers\ ``` chaieb@31761 ` 183` chaieb@31761 ` 184` ```context idom ``` chaieb@31761 ` 185` ```begin ``` wenzelm@53196 ` 186` chaieb@31761 ` 187` ```subclass ring_no_zero_divisors .. ``` wenzelm@53196 ` 188` chaieb@31761 ` 189` ```end ``` chaieb@31761 ` 190` haftmann@59867 ` 191` ```instantiation fract :: (idom) field ``` chaieb@31761 ` 192` ```begin ``` chaieb@31761 ` 193` Andreas@61106 ` 194` ```lift_definition inverse_fract :: "'a fract \ 'a fract" ``` Andreas@61106 ` 195` ``` is "\x. if fst x = 0 then (0, 1) else (snd x, fst x)" ``` Andreas@61106 ` 196` ```by(auto simp add: algebra_simps) ``` chaieb@31761 ` 197` chaieb@31761 ` 198` ```lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a" ``` Andreas@61106 ` 199` ```by transfer simp ``` chaieb@31761 ` 200` haftmann@60429 ` 201` ```definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)" ``` chaieb@31761 ` 202` haftmann@60429 ` 203` ```lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" ``` chaieb@31761 ` 204` ``` by (simp add: divide_fract_def) ``` chaieb@31761 ` 205` wenzelm@47252 ` 206` ```instance ``` wenzelm@47252 ` 207` ```proof ``` chaieb@31761 ` 208` ``` fix q :: "'a fract" ``` chaieb@31761 ` 209` ``` assume "q \ 0" ``` wenzelm@46573 ` 210` ``` then show "inverse q * q = 1" ``` wenzelm@46573 ` 211` ``` by (cases q rule: Fract_cases_nonzero) ``` haftmann@57512 ` 212` ``` (simp_all add: fract_expand eq_fract mult.commute) ``` chaieb@31761 ` 213` ```next ``` chaieb@31761 ` 214` ``` fix q r :: "'a fract" ``` haftmann@60429 ` 215` ``` show "q div r = q * inverse r" by (simp add: divide_fract_def) ``` haftmann@36409 ` 216` ```next ``` wenzelm@46573 ` 217` ``` show "inverse 0 = (0:: 'a fract)" ``` wenzelm@46573 ` 218` ``` by (simp add: fract_expand) (simp add: fract_collapse) ``` chaieb@31761 ` 219` ```qed ``` chaieb@31761 ` 220` chaieb@31761 ` 221` ```end ``` chaieb@31761 ` 222` chaieb@31761 ` 223` wenzelm@60500 ` 224` ```subsubsection \The ordered field of fractions over an ordered idom\ ``` huffman@36331 ` 225` Andreas@61106 ` 226` ```instantiation fract :: (linordered_idom) linorder ``` Andreas@61106 ` 227` ```begin ``` huffman@36331 ` 228` Andreas@61106 ` 229` ```lemma less_eq_fract_respect: ``` Andreas@61106 ` 230` ``` fixes a b a' b' c d c' d' :: 'a ``` Andreas@61106 ` 231` ``` assumes neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" ``` Andreas@61106 ` 232` ``` assumes eq1: "a * b' = a' * b" ``` Andreas@61106 ` 233` ``` assumes eq2: "c * d' = c' * d" ``` Andreas@61106 ` 234` ``` shows "((a * d) * (b * d) \ (c * b) * (b * d)) \ ((a' * d') * (b' * d') \ (c' * b') * (b' * d'))" ``` Andreas@61106 ` 235` ```proof - ``` huffman@36331 ` 236` ``` let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" ``` huffman@36331 ` 237` ``` { ``` wenzelm@54463 ` 238` ``` fix a b c d x :: 'a ``` wenzelm@54463 ` 239` ``` assume x: "x \ 0" ``` huffman@36331 ` 240` ``` have "?le a b c d = ?le (a * x) (b * x) c d" ``` huffman@36331 ` 241` ``` proof - ``` wenzelm@54463 ` 242` ``` from x have "0 < x * x" ``` wenzelm@54463 ` 243` ``` by (auto simp add: zero_less_mult_iff) ``` wenzelm@46573 ` 244` ``` then have "?le a b c d = ``` huffman@36331 ` 245` ``` ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" ``` huffman@36331 ` 246` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 247` ``` also have "... = ?le (a * x) (b * x) c d" ``` haftmann@57514 ` 248` ``` by (simp add: ac_simps) ``` huffman@36331 ` 249` ``` finally show ?thesis . ``` huffman@36331 ` 250` ``` qed ``` huffman@36331 ` 251` ``` } note le_factor = this ``` huffman@36331 ` 252` huffman@36331 ` 253` ``` let ?D = "b * d" and ?D' = "b' * d'" ``` huffman@36331 ` 254` ``` from neq have D: "?D \ 0" by simp ``` huffman@36331 ` 255` ``` from neq have "?D' \ 0" by simp ``` wenzelm@46573 ` 256` ``` then have "?le a b c d = ?le (a * ?D') (b * ?D') c d" ``` huffman@36331 ` 257` ``` by (rule le_factor) ``` huffman@36331 ` 258` ``` also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" ``` haftmann@57514 ` 259` ``` by (simp add: ac_simps) ``` huffman@36331 ` 260` ``` also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" ``` huffman@36331 ` 261` ``` by (simp only: eq1 eq2) ``` huffman@36331 ` 262` ``` also have "... = ?le (a' * ?D) (b' * ?D) c' d'" ``` haftmann@57514 ` 263` ``` by (simp add: ac_simps) ``` huffman@36331 ` 264` ``` also from D have "... = ?le a' b' c' d'" ``` huffman@36331 ` 265` ``` by (rule le_factor [symmetric]) ``` huffman@36331 ` 266` ``` finally show "?le a b c d = ?le a' b' c' d'" . ``` huffman@36331 ` 267` ```qed ``` huffman@36331 ` 268` Andreas@61106 ` 269` ```lift_definition less_eq_fract :: "'a fract \ 'a fract \ bool" ``` Andreas@61106 ` 270` ``` is "\q r. (fst q * snd r) * (snd q * snd r) \ (fst r * snd q) * (snd q * snd r)" ``` Andreas@61106 ` 271` ```by (clarsimp simp add: less_eq_fract_respect) ``` huffman@36331 ` 272` wenzelm@46573 ` 273` ```definition less_fract_def: "z < (w::'a fract) \ z \ w \ \ w \ z" ``` huffman@36331 ` 274` huffman@36331 ` 275` ```lemma le_fract [simp]: ``` Andreas@61106 ` 276` ``` "\ b \ 0; d \ 0 \ \ Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" ``` Andreas@61106 ` 277` ``` by transfer simp ``` huffman@36331 ` 278` huffman@36331 ` 279` ```lemma less_fract [simp]: ``` Andreas@61106 ` 280` ``` "\ b \ 0; d \ 0 \ \ Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)" ``` haftmann@57514 ` 281` ``` by (simp add: less_fract_def less_le_not_le ac_simps assms) ``` huffman@36331 ` 282` wenzelm@47252 ` 283` ```instance ``` wenzelm@47252 ` 284` ```proof ``` huffman@36331 ` 285` ``` fix q r s :: "'a fract" ``` wenzelm@54463 ` 286` ``` assume "q \ r" and "r \ s" ``` wenzelm@54463 ` 287` ``` then show "q \ s" ``` huffman@36331 ` 288` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 289` ``` fix a b c d e f :: 'a ``` wenzelm@54463 ` 290` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` wenzelm@54463 ` 291` ``` assume 1: "Fract a b \ Fract c d" ``` wenzelm@54463 ` 292` ``` assume 2: "Fract c d \ Fract e f" ``` huffman@36331 ` 293` ``` show "Fract a b \ Fract e f" ``` huffman@36331 ` 294` ``` proof - ``` huffman@36331 ` 295` ``` from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" ``` huffman@36331 ` 296` ``` by (auto simp add: zero_less_mult_iff linorder_neq_iff) ``` huffman@36331 ` 297` ``` have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" ``` huffman@36331 ` 298` ``` proof - ``` huffman@36331 ` 299` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 300` ``` by simp ``` huffman@36331 ` 301` ``` with ff show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 302` ``` qed ``` huffman@36331 ` 303` ``` also have "... = (c * f) * (d * f) * (b * b)" ``` haftmann@57514 ` 304` ``` by (simp only: ac_simps) ``` huffman@36331 ` 305` ``` also have "... \ (e * d) * (d * f) * (b * b)" ``` huffman@36331 ` 306` ``` proof - ``` huffman@36331 ` 307` ``` from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" ``` huffman@36331 ` 308` ``` by simp ``` huffman@36331 ` 309` ``` with bb show ?thesis by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 310` ``` qed ``` huffman@36331 ` 311` ``` finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" ``` haftmann@57514 ` 312` ``` by (simp only: ac_simps) ``` huffman@36331 ` 313` ``` with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" ``` huffman@36331 ` 314` ``` by (simp add: mult_le_cancel_right) ``` huffman@36331 ` 315` ``` with neq show ?thesis by simp ``` huffman@36331 ` 316` ``` qed ``` huffman@36331 ` 317` ``` qed ``` huffman@36331 ` 318` ```next ``` huffman@36331 ` 319` ``` fix q r :: "'a fract" ``` wenzelm@54463 ` 320` ``` assume "q \ r" and "r \ q" ``` wenzelm@54463 ` 321` ``` then show "q = r" ``` huffman@36331 ` 322` ``` proof (induct q, induct r) ``` huffman@36331 ` 323` ``` fix a b c d :: 'a ``` wenzelm@54463 ` 324` ``` assume neq: "b \ 0" "d \ 0" ``` wenzelm@54463 ` 325` ``` assume 1: "Fract a b \ Fract c d" ``` wenzelm@54463 ` 326` ``` assume 2: "Fract c d \ Fract a b" ``` huffman@36331 ` 327` ``` show "Fract a b = Fract c d" ``` huffman@36331 ` 328` ``` proof - ``` huffman@36331 ` 329` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 330` ``` by simp ``` huffman@36331 ` 331` ``` also have "... \ (a * d) * (b * d)" ``` huffman@36331 ` 332` ``` proof - ``` huffman@36331 ` 333` ``` from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" ``` huffman@36331 ` 334` ``` by simp ``` haftmann@57514 ` 335` ``` then show ?thesis by (simp only: ac_simps) ``` huffman@36331 ` 336` ``` qed ``` huffman@36331 ` 337` ``` finally have "(a * d) * (b * d) = (c * b) * (b * d)" . ``` huffman@36331 ` 338` ``` moreover from neq have "b * d \ 0" by simp ``` huffman@36331 ` 339` ``` ultimately have "a * d = c * b" by simp ``` huffman@36331 ` 340` ``` with neq show ?thesis by (simp add: eq_fract) ``` huffman@36331 ` 341` ``` qed ``` huffman@36331 ` 342` ``` qed ``` huffman@36331 ` 343` ```next ``` huffman@36331 ` 344` ``` fix q r :: "'a fract" ``` huffman@36331 ` 345` ``` show "q \ q" ``` huffman@36331 ` 346` ``` by (induct q) simp ``` huffman@36331 ` 347` ``` show "(q < r) = (q \ r \ \ r \ q)" ``` huffman@36331 ` 348` ``` by (simp only: less_fract_def) ``` huffman@36331 ` 349` ``` show "q \ r \ r \ q" ``` huffman@36331 ` 350` ``` by (induct q, induct r) ``` haftmann@57512 ` 351` ``` (simp add: mult.commute, rule linorder_linear) ``` huffman@36331 ` 352` ```qed ``` huffman@36331 ` 353` huffman@36331 ` 354` ```end ``` huffman@36331 ` 355` wenzelm@54463 ` 356` ```instantiation fract :: (linordered_idom) "{distrib_lattice,abs_if,sgn_if}" ``` huffman@36331 ` 357` ```begin ``` huffman@36331 ` 358` Andreas@61106 ` 359` ```definition abs_fract_def2: "\q\ = (if q < 0 then -q else (q::'a fract))" ``` huffman@36331 ` 360` wenzelm@46573 ` 361` ```definition sgn_fract_def: ``` wenzelm@54463 ` 362` ``` "sgn (q::'a fract) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" ``` huffman@36331 ` 363` huffman@36331 ` 364` ```theorem abs_fract [simp]: "\Fract a b\ = Fract \a\ \b\" ``` Andreas@61106 ` 365` ```unfolding abs_fract_def2 not_le[symmetric] ``` Andreas@61106 ` 366` ```by transfer(auto simp add: zero_less_mult_iff le_less) ``` huffman@36331 ` 367` wenzelm@46573 ` 368` ```definition inf_fract_def: ``` wenzelm@61076 ` 369` ``` "(inf :: 'a fract \ 'a fract \ 'a fract) = min" ``` huffman@36331 ` 370` wenzelm@46573 ` 371` ```definition sup_fract_def: ``` wenzelm@61076 ` 372` ``` "(sup :: 'a fract \ 'a fract \ 'a fract) = max" ``` huffman@36331 ` 373` wenzelm@46573 ` 374` ```instance ``` Andreas@61106 ` 375` ```by intro_classes (simp_all add: abs_fract_def2 sgn_fract_def inf_fract_def sup_fract_def max_min_distrib2) ``` huffman@36331 ` 376` huffman@36331 ` 377` ```end ``` huffman@36331 ` 378` haftmann@59867 ` 379` ```instance fract :: (linordered_idom) linordered_field ``` huffman@36331 ` 380` ```proof ``` huffman@36331 ` 381` ``` fix q r s :: "'a fract" ``` wenzelm@53196 ` 382` ``` assume "q \ r" ``` wenzelm@53196 ` 383` ``` then show "s + q \ s + r" ``` huffman@36331 ` 384` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 385` ``` fix a b c d e f :: 'a ``` wenzelm@53196 ` 386` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 387` ``` assume le: "Fract a b \ Fract c d" ``` huffman@36331 ` 388` ``` show "Fract e f + Fract a b \ Fract e f + Fract c d" ``` huffman@36331 ` 389` ``` proof - ``` huffman@36331 ` 390` ``` let ?F = "f * f" from neq have F: "0 < ?F" ``` huffman@36331 ` 391` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 392` ``` from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` huffman@36331 ` 393` ``` by simp ``` huffman@36331 ` 394` ``` with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" ``` huffman@36331 ` 395` ``` by (simp add: mult_le_cancel_right) ``` haftmann@36348 ` 396` ``` with neq show ?thesis by (simp add: field_simps) ``` huffman@36331 ` 397` ``` qed ``` huffman@36331 ` 398` ``` qed ``` wenzelm@53196 ` 399` ```next ``` wenzelm@53196 ` 400` ``` fix q r s :: "'a fract" ``` wenzelm@53196 ` 401` ``` assume "q < r" and "0 < s" ``` wenzelm@53196 ` 402` ``` then show "s * q < s * r" ``` huffman@36331 ` 403` ``` proof (induct q, induct r, induct s) ``` huffman@36331 ` 404` ``` fix a b c d e f :: 'a ``` wenzelm@54463 ` 405` ``` assume neq: "b \ 0" "d \ 0" "f \ 0" ``` huffman@36331 ` 406` ``` assume le: "Fract a b < Fract c d" ``` huffman@36331 ` 407` ``` assume gt: "0 < Fract e f" ``` huffman@36331 ` 408` ``` show "Fract e f * Fract a b < Fract e f * Fract c d" ``` huffman@36331 ` 409` ``` proof - ``` huffman@36331 ` 410` ``` let ?E = "e * f" and ?F = "f * f" ``` huffman@36331 ` 411` ``` from neq gt have "0 < ?E" ``` huffman@36331 ` 412` ``` by (auto simp add: Zero_fract_def order_less_le eq_fract) ``` huffman@36331 ` 413` ``` moreover from neq have "0 < ?F" ``` huffman@36331 ` 414` ``` by (auto simp add: zero_less_mult_iff) ``` huffman@36331 ` 415` ``` moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" ``` huffman@36331 ` 416` ``` by simp ``` huffman@36331 ` 417` ``` ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" ``` huffman@36331 ` 418` ``` by (simp add: mult_less_cancel_right) ``` huffman@36331 ` 419` ``` with neq show ?thesis ``` haftmann@57514 ` 420` ``` by (simp add: ac_simps) ``` huffman@36331 ` 421` ``` qed ``` huffman@36331 ` 422` ``` qed ``` huffman@36331 ` 423` ```qed ``` huffman@36331 ` 424` huffman@36331 ` 425` ```lemma fract_induct_pos [case_names Fract]: ``` huffman@36331 ` 426` ``` fixes P :: "'a::linordered_idom fract \ bool" ``` huffman@36331 ` 427` ``` assumes step: "\a b. 0 < b \ P (Fract a b)" ``` huffman@36331 ` 428` ``` shows "P q" ``` huffman@36331 ` 429` ```proof (cases q) ``` wenzelm@54463 ` 430` ``` case (Fract a b) ``` wenzelm@54463 ` 431` ``` { ``` wenzelm@54463 ` 432` ``` fix a b :: 'a ``` huffman@36331 ` 433` ``` assume b: "b < 0" ``` wenzelm@54463 ` 434` ``` have "P (Fract a b)" ``` wenzelm@54463 ` 435` ``` proof - ``` wenzelm@54463 ` 436` ``` from b have "0 < - b" by simp ``` wenzelm@54463 ` 437` ``` then have "P (Fract (- a) (- b))" ``` wenzelm@54463 ` 438` ``` by (rule step) ``` wenzelm@54463 ` 439` ``` then show "P (Fract a b)" ``` wenzelm@54463 ` 440` ``` by (simp add: order_less_imp_not_eq [OF b]) ``` wenzelm@54463 ` 441` ``` qed ``` wenzelm@54463 ` 442` ``` } ``` wenzelm@54463 ` 443` ``` with Fract show "P q" ``` wenzelm@54463 ` 444` ``` by (auto simp add: linorder_neq_iff step) ``` huffman@36331 ` 445` ```qed ``` huffman@36331 ` 446` wenzelm@53196 ` 447` ```lemma zero_less_Fract_iff: "0 < b \ 0 < Fract a b \ 0 < a" ``` huffman@36331 ` 448` ``` by (auto simp add: Zero_fract_def zero_less_mult_iff) ``` huffman@36331 ` 449` wenzelm@53196 ` 450` ```lemma Fract_less_zero_iff: "0 < b \ Fract a b < 0 \ a < 0" ``` huffman@36331 ` 451` ``` by (auto simp add: Zero_fract_def mult_less_0_iff) ``` huffman@36331 ` 452` wenzelm@53196 ` 453` ```lemma zero_le_Fract_iff: "0 < b \ 0 \ Fract a b \ 0 \ a" ``` huffman@36331 ` 454` ``` by (auto simp add: Zero_fract_def zero_le_mult_iff) ``` huffman@36331 ` 455` wenzelm@53196 ` 456` ```lemma Fract_le_zero_iff: "0 < b \ Fract a b \ 0 \ a \ 0" ``` huffman@36331 ` 457` ``` by (auto simp add: Zero_fract_def mult_le_0_iff) ``` huffman@36331 ` 458` wenzelm@53196 ` 459` ```lemma one_less_Fract_iff: "0 < b \ 1 < Fract a b \ b < a" ``` huffman@36331 ` 460` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 461` wenzelm@53196 ` 462` ```lemma Fract_less_one_iff: "0 < b \ Fract a b < 1 \ a < b" ``` huffman@36331 ` 463` ``` by (auto simp add: One_fract_def mult_less_cancel_right_disj) ``` huffman@36331 ` 464` wenzelm@53196 ` 465` ```lemma one_le_Fract_iff: "0 < b \ 1 \ Fract a b \ b \ a" ``` huffman@36331 ` 466` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 467` wenzelm@53196 ` 468` ```lemma Fract_le_one_iff: "0 < b \ Fract a b \ 1 \ a \ b" ``` huffman@36331 ` 469` ``` by (auto simp add: One_fract_def mult_le_cancel_right) ``` huffman@36331 ` 470` huffman@36331 ` 471` ```end ```