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