src/HOL/Computational_Algebra/Normalized_Fraction.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 65435 378175f44328 child 66886 960509bfd47e permissions -rw-r--r--
executable domain membership checks
 wenzelm@65435 ` 1` ```(* Title: HOL/Computational_Algebra/Normalized_Fraction.thy ``` haftmann@64591 ` 2` ``` Author: Manuel Eberl ``` haftmann@64591 ` 3` ```*) ``` haftmann@64591 ` 4` eberlm@63500 ` 5` ```theory Normalized_Fraction ``` eberlm@63500 ` 6` ```imports ``` eberlm@63500 ` 7` ``` Main ``` haftmann@65417 ` 8` ``` Euclidean_Algorithm ``` wenzelm@65366 ` 9` ``` Fraction_Field ``` eberlm@63500 ` 10` ```begin ``` eberlm@63500 ` 11` eberlm@63500 ` 12` ```definition quot_to_fract :: "'a :: {idom} \ 'a \ 'a fract" where ``` eberlm@63500 ` 13` ``` "quot_to_fract = (\(a,b). Fraction_Field.Fract a b)" ``` eberlm@63500 ` 14` eberlm@63500 ` 15` ```definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \ 'a \ 'a \ 'a" where ``` eberlm@63500 ` 16` ``` "normalize_quot = ``` eberlm@63500 ` 17` ``` (\(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))" ``` eberlm@63500 ` 18` eberlm@63500 ` 19` ```definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \ 'a) set" where ``` eberlm@63500 ` 20` ``` "normalized_fracts = {(a,b). coprime a b \ unit_factor b = 1}" ``` eberlm@63500 ` 21` ``` ``` eberlm@63500 ` 22` ```lemma not_normalized_fracts_0_denom [simp]: "(a, 0) \ normalized_fracts" ``` eberlm@63500 ` 23` ``` by (auto simp: normalized_fracts_def) ``` eberlm@63500 ` 24` eberlm@63500 ` 25` ```lemma unit_factor_snd_normalize_quot [simp]: ``` eberlm@63500 ` 26` ``` "unit_factor (snd (normalize_quot x)) = 1" ``` eberlm@63500 ` 27` ``` by (simp add: normalize_quot_def case_prod_unfold Let_def dvd_unit_factor_div ``` eberlm@63500 ` 28` ``` mult_unit_dvd_iff unit_factor_mult unit_factor_gcd) ``` eberlm@63500 ` 29` ``` ``` eberlm@63500 ` 30` ```lemma snd_normalize_quot_nonzero [simp]: "snd (normalize_quot x) \ 0" ``` eberlm@63500 ` 31` ``` using unit_factor_snd_normalize_quot[of x] ``` eberlm@63500 ` 32` ``` by (auto simp del: unit_factor_snd_normalize_quot) ``` eberlm@63500 ` 33` ``` ``` eberlm@63500 ` 34` ```lemma normalize_quot_aux: ``` eberlm@63500 ` 35` ``` fixes a b ``` eberlm@63500 ` 36` ``` assumes "b \ 0" ``` eberlm@63500 ` 37` ``` defines "d \ gcd a b * unit_factor b" ``` eberlm@63500 ` 38` ``` shows "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" ``` eberlm@63500 ` 39` ``` "d dvd a" "d dvd b" "d \ 0" ``` eberlm@63500 ` 40` ```proof - ``` eberlm@63500 ` 41` ``` from assms show "d dvd a" "d dvd b" ``` eberlm@63500 ` 42` ``` by (simp_all add: d_def mult_unit_dvd_iff) ``` eberlm@63500 ` 43` ``` thus "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" "d \ 0" ``` eberlm@63500 ` 44` ``` by (auto simp: normalize_quot_def Let_def d_def \b \ 0\) ``` eberlm@63500 ` 45` ```qed ``` eberlm@63500 ` 46` eberlm@63500 ` 47` ```lemma normalize_quotE: ``` eberlm@63500 ` 48` ``` assumes "b \ 0" ``` eberlm@63500 ` 49` ``` obtains d where "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" ``` eberlm@63500 ` 50` ``` "d dvd a" "d dvd b" "d \ 0" ``` eberlm@63500 ` 51` ``` using that[OF normalize_quot_aux[OF assms]] . ``` eberlm@63500 ` 52` ``` ``` eberlm@63500 ` 53` ```lemma normalize_quotE': ``` eberlm@63500 ` 54` ``` assumes "snd x \ 0" ``` eberlm@63500 ` 55` ``` obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d" ``` eberlm@63500 ` 56` ``` "d dvd fst x" "d dvd snd x" "d \ 0" ``` eberlm@63500 ` 57` ```proof - ``` eberlm@63500 ` 58` ``` from normalize_quotE[OF assms, of "fst x"] guess d . ``` eberlm@63500 ` 59` ``` from this show ?thesis unfolding prod.collapse by (intro that[of d]) ``` eberlm@63500 ` 60` ```qed ``` eberlm@63500 ` 61` ``` ``` eberlm@63500 ` 62` ```lemma coprime_normalize_quot: ``` eberlm@63500 ` 63` ``` "coprime (fst (normalize_quot x)) (snd (normalize_quot x))" ``` eberlm@63500 ` 64` ``` by (simp add: normalize_quot_def case_prod_unfold Let_def ``` eberlm@63500 ` 65` ``` div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime) ``` eberlm@63500 ` 66` eberlm@63500 ` 67` ```lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \ normalized_fracts" ``` eberlm@63500 ` 68` ``` by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold) ``` eberlm@63500 ` 69` eberlm@63500 ` 70` ```lemma normalize_quot_eq_iff: ``` eberlm@63500 ` 71` ``` assumes "b \ 0" "d \ 0" ``` eberlm@63500 ` 72` ``` shows "normalize_quot (a,b) = normalize_quot (c,d) \ a * d = b * c" ``` eberlm@63500 ` 73` ```proof - ``` eberlm@63500 ` 74` ``` define x y where "x = normalize_quot (a,b)" and "y = normalize_quot (c,d)" ``` eberlm@63500 ` 75` ``` from normalize_quotE[OF assms(1), of a] normalize_quotE[OF assms(2), of c] ``` eberlm@63500 ` 76` ``` obtain d1 d2 ``` eberlm@63500 ` 77` ``` where "a = fst x * d1" "b = snd x * d1" "c = fst y * d2" "d = snd y * d2" "d1 \ 0" "d2 \ 0" ``` eberlm@63500 ` 78` ``` unfolding x_def y_def by metis ``` eberlm@63500 ` 79` ``` hence "a * d = b * c \ fst x * snd y = snd x * fst y" by simp ``` eberlm@63500 ` 80` ``` also have "\ \ fst x = fst y \ snd x = snd y" ``` eberlm@63500 ` 81` ``` by (intro coprime_crossproduct') (simp_all add: x_def y_def coprime_normalize_quot) ``` eberlm@63500 ` 82` ``` also have "\ \ x = y" using prod_eqI by blast ``` eberlm@63500 ` 83` ``` finally show "x = y \ a * d = b * c" .. ``` eberlm@63500 ` 84` ```qed ``` eberlm@63500 ` 85` eberlm@63500 ` 86` ```lemma normalize_quot_eq_iff': ``` eberlm@63500 ` 87` ``` assumes "snd x \ 0" "snd y \ 0" ``` eberlm@63500 ` 88` ``` shows "normalize_quot x = normalize_quot y \ fst x * snd y = snd x * fst y" ``` eberlm@63500 ` 89` ``` using assms by (cases x, cases y, hypsubst) (subst normalize_quot_eq_iff, simp_all) ``` eberlm@63500 ` 90` eberlm@63500 ` 91` ```lemma normalize_quot_id: "x \ normalized_fracts \ normalize_quot x = x" ``` eberlm@63500 ` 92` ``` by (auto simp: normalized_fracts_def normalize_quot_def case_prod_unfold) ``` eberlm@63500 ` 93` eberlm@63500 ` 94` ```lemma normalize_quot_idem [simp]: "normalize_quot (normalize_quot x) = normalize_quot x" ``` eberlm@63500 ` 95` ``` by (rule normalize_quot_id) simp_all ``` eberlm@63500 ` 96` eberlm@63500 ` 97` ```lemma fractrel_iff_normalize_quot_eq: ``` eberlm@63500 ` 98` ``` "fractrel x y \ normalize_quot x = normalize_quot y \ snd x \ 0 \ snd y \ 0" ``` eberlm@63500 ` 99` ``` by (cases x, cases y) (auto simp: fractrel_def normalize_quot_eq_iff) ``` eberlm@63500 ` 100` ``` ``` eberlm@63500 ` 101` ```lemma fractrel_normalize_quot_left: ``` eberlm@63500 ` 102` ``` assumes "snd x \ 0" ``` eberlm@63500 ` 103` ``` shows "fractrel (normalize_quot x) y \ fractrel x y" ``` eberlm@63500 ` 104` ``` using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto ``` eberlm@63500 ` 105` eberlm@63500 ` 106` ```lemma fractrel_normalize_quot_right: ``` eberlm@63500 ` 107` ``` assumes "snd x \ 0" ``` eberlm@63500 ` 108` ``` shows "fractrel y (normalize_quot x) \ fractrel y x" ``` eberlm@63500 ` 109` ``` using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto ``` eberlm@63500 ` 110` eberlm@63500 ` 111` ``` ``` eberlm@63500 ` 112` ```lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \ 'a \ 'a" ``` eberlm@63500 ` 113` ``` is normalize_quot ``` eberlm@63500 ` 114` ``` by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all ``` eberlm@63500 ` 115` ``` ``` eberlm@63500 ` 116` ```lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x" ``` eberlm@63500 ` 117` ``` unfolding quot_to_fract_def ``` eberlm@63500 ` 118` ```proof transfer ``` eberlm@63500 ` 119` ``` fix x :: "'a \ 'a" assume rel: "fractrel x x" ``` eberlm@63500 ` 120` ``` define x' where "x' = normalize_quot x" ``` eberlm@63500 ` 121` ``` obtain a b where [simp]: "x = (a, b)" by (cases x) ``` eberlm@63500 ` 122` ``` from rel have "b \ 0" by simp ``` eberlm@63500 ` 123` ``` from normalize_quotE[OF this, of a] guess d . ``` eberlm@63500 ` 124` ``` hence "a = fst x' * d" "b = snd x' * d" "d \ 0" "snd x' \ 0" by (simp_all add: x'_def) ``` eberlm@63500 ` 125` ``` thus "fractrel (case x' of (a, b) \ if b = 0 then (0, 1) else (a, b)) x" ``` eberlm@63500 ` 126` ``` by (auto simp add: case_prod_unfold) ``` eberlm@63500 ` 127` ```qed ``` eberlm@63500 ` 128` eberlm@63500 ` 129` ```lemma quot_of_fract_quot_to_fract: "quot_of_fract (quot_to_fract x) = normalize_quot x" ``` eberlm@63500 ` 130` ```proof (cases "snd x = 0") ``` eberlm@63500 ` 131` ``` case True ``` eberlm@63500 ` 132` ``` thus ?thesis unfolding quot_to_fract_def ``` eberlm@63500 ` 133` ``` by transfer (simp add: case_prod_unfold normalize_quot_def) ``` eberlm@63500 ` 134` ```next ``` eberlm@63500 ` 135` ``` case False ``` eberlm@63500 ` 136` ``` thus ?thesis unfolding quot_to_fract_def by transfer (simp add: case_prod_unfold) ``` eberlm@63500 ` 137` ```qed ``` eberlm@63500 ` 138` eberlm@63500 ` 139` ```lemma quot_of_fract_quot_to_fract': ``` eberlm@63500 ` 140` ``` "x \ normalized_fracts \ quot_of_fract (quot_to_fract x) = x" ``` eberlm@63500 ` 141` ``` unfolding quot_to_fract_def by transfer (auto simp: normalize_quot_id) ``` eberlm@63500 ` 142` eberlm@63500 ` 143` ```lemma quot_of_fract_in_normalized_fracts [simp]: "quot_of_fract x \ normalized_fracts" ``` eberlm@63500 ` 144` ``` by transfer simp ``` eberlm@63500 ` 145` eberlm@63500 ` 146` ```lemma normalize_quotI: ``` eberlm@63500 ` 147` ``` assumes "a * d = b * c" "b \ 0" "(c, d) \ normalized_fracts" ``` eberlm@63500 ` 148` ``` shows "normalize_quot (a, b) = (c, d)" ``` eberlm@63500 ` 149` ```proof - ``` eberlm@63500 ` 150` ``` from assms have "normalize_quot (a, b) = normalize_quot (c, d)" ``` eberlm@63500 ` 151` ``` by (subst normalize_quot_eq_iff) auto ``` eberlm@63500 ` 152` ``` also have "\ = (c, d)" by (intro normalize_quot_id) fact ``` eberlm@63500 ` 153` ``` finally show ?thesis . ``` eberlm@63500 ` 154` ```qed ``` eberlm@63500 ` 155` eberlm@63500 ` 156` ```lemma td_normalized_fract: ``` eberlm@63500 ` 157` ``` "type_definition quot_of_fract quot_to_fract normalized_fracts" ``` eberlm@63500 ` 158` ``` by standard (simp_all add: quot_of_fract_quot_to_fract') ``` eberlm@63500 ` 159` eberlm@63500 ` 160` ```lemma quot_of_fract_add_aux: ``` eberlm@63500 ` 161` ``` assumes "snd x \ 0" "snd y \ 0" ``` eberlm@63500 ` 162` ``` shows "(fst x * snd y + fst y * snd x) * (snd (normalize_quot x) * snd (normalize_quot y)) = ``` eberlm@63500 ` 163` ``` snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) + ``` eberlm@63500 ` 164` ``` snd (normalize_quot x) * fst (normalize_quot y))" ``` eberlm@63500 ` 165` ```proof - ``` eberlm@63500 ` 166` ``` from normalize_quotE'[OF assms(1)] guess d . note d = this ``` eberlm@63500 ` 167` ``` from normalize_quotE'[OF assms(2)] guess e . note e = this ``` eberlm@63500 ` 168` ``` show ?thesis by (simp_all add: d e algebra_simps) ``` eberlm@63500 ` 169` ```qed ``` eberlm@63500 ` 170` eberlm@63500 ` 171` eberlm@63500 ` 172` ```locale fract_as_normalized_quot ``` eberlm@63500 ` 173` ```begin ``` eberlm@63500 ` 174` ```setup_lifting td_normalized_fract ``` eberlm@63500 ` 175` ```end ``` eberlm@63500 ` 176` eberlm@63500 ` 177` eberlm@63500 ` 178` ```lemma quot_of_fract_add: ``` eberlm@63500 ` 179` ``` "quot_of_fract (x + y) = ``` eberlm@63500 ` 180` ``` (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y ``` eberlm@63500 ` 181` ``` in normalize_quot (a * d + b * c, b * d))" ``` eberlm@63500 ` 182` ``` by transfer (insert quot_of_fract_add_aux, ``` eberlm@63500 ` 183` ``` simp_all add: Let_def case_prod_unfold normalize_quot_eq_iff) ``` eberlm@63500 ` 184` eberlm@63500 ` 185` ```lemma quot_of_fract_uminus: ``` eberlm@63500 ` 186` ``` "quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))" ``` haftmann@64592 ` 187` ``` by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff) ``` eberlm@63500 ` 188` eberlm@63500 ` 189` ```lemma quot_of_fract_diff: ``` eberlm@63500 ` 190` ``` "quot_of_fract (x - y) = ``` eberlm@63500 ` 191` ``` (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y ``` eberlm@63500 ` 192` ``` in normalize_quot (a * d - b * c, b * d))" (is "_ = ?rhs") ``` eberlm@63500 ` 193` ```proof - ``` eberlm@63500 ` 194` ``` have "x - y = x + -y" by simp ``` eberlm@63500 ` 195` ``` also have "quot_of_fract \ = ?rhs" ``` eberlm@63500 ` 196` ``` by (simp only: quot_of_fract_add quot_of_fract_uminus Let_def case_prod_unfold) simp_all ``` eberlm@63500 ` 197` ``` finally show ?thesis . ``` eberlm@63500 ` 198` ```qed ``` eberlm@63500 ` 199` eberlm@63500 ` 200` ```lemma normalize_quot_mult_coprime: ``` eberlm@63500 ` 201` ``` assumes "coprime a b" "coprime c d" "unit_factor b = 1" "unit_factor d = 1" ``` eberlm@63500 ` 202` ``` defines "e \ fst (normalize_quot (a, d))" and "f \ snd (normalize_quot (a, d))" ``` eberlm@63500 ` 203` ``` and "g \ fst (normalize_quot (c, b))" and "h \ snd (normalize_quot (c, b))" ``` eberlm@63500 ` 204` ``` shows "normalize_quot (a * c, b * d) = (e * g, f * h)" ``` eberlm@63500 ` 205` ```proof (rule normalize_quotI) ``` eberlm@63500 ` 206` ``` from assms have "b \ 0" "d \ 0" by auto ``` eberlm@63500 ` 207` ``` from normalize_quotE[OF \b \ 0\, of c] guess k . note k = this [folded assms] ``` eberlm@63500 ` 208` ``` from normalize_quotE[OF \d \ 0\, of a] guess l . note l = this [folded assms] ``` eberlm@63500 ` 209` ``` from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all) ``` eberlm@63500 ` 210` ``` from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1" ``` eberlm@63500 ` 211` ``` by simp_all ``` eberlm@63500 ` 212` ``` from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot) ``` eberlm@63500 ` 213` ``` with k l assms(1,2) show "(e * g, f * h) \ normalized_fracts" ``` eberlm@63500 ` 214` ``` by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq') ``` eberlm@63500 ` 215` ```qed (insert assms(3,4), auto) ``` eberlm@63500 ` 216` eberlm@63500 ` 217` ```lemma normalize_quot_mult: ``` eberlm@63500 ` 218` ``` assumes "snd x \ 0" "snd y \ 0" ``` eberlm@63500 ` 219` ``` shows "normalize_quot (fst x * fst y, snd x * snd y) = normalize_quot ``` eberlm@63500 ` 220` ``` (fst (normalize_quot x) * fst (normalize_quot y), ``` eberlm@63500 ` 221` ``` snd (normalize_quot x) * snd (normalize_quot y))" ``` eberlm@63500 ` 222` ```proof - ``` eberlm@63500 ` 223` ``` from normalize_quotE'[OF assms(1)] guess d . note d = this ``` eberlm@63500 ` 224` ``` from normalize_quotE'[OF assms(2)] guess e . note e = this ``` eberlm@63500 ` 225` ``` show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff) ``` eberlm@63500 ` 226` ```qed ``` eberlm@63500 ` 227` eberlm@63500 ` 228` ```lemma quot_of_fract_mult: ``` eberlm@63500 ` 229` ``` "quot_of_fract (x * y) = ``` eberlm@63500 ` 230` ``` (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; ``` eberlm@63500 ` 231` ``` (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b) ``` eberlm@63500 ` 232` ``` in (e*g, f*h))" ``` eberlm@63500 ` 233` ``` by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric] ``` eberlm@63500 ` 234` ``` coprime_normalize_quot normalize_quot_mult [symmetric]) ``` eberlm@63500 ` 235` ``` ``` eberlm@63500 ` 236` ```lemma normalize_quot_0 [simp]: ``` eberlm@63500 ` 237` ``` "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)" ``` eberlm@63500 ` 238` ``` by (simp_all add: normalize_quot_def) ``` eberlm@63500 ` 239` ``` ``` eberlm@63500 ` 240` ```lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \ fst x = 0 \ snd x = 0" ``` eberlm@63500 ` 241` ``` by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff) ``` eberlm@63500 ` 242` ``` find_theorems "_ div _ = 0" ``` eberlm@63500 ` 243` ``` ``` eberlm@63500 ` 244` ```lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \ snd (quot_of_fract x) = 1" ``` eberlm@63500 ` 245` ``` by transfer auto ``` eberlm@63500 ` 246` eberlm@63500 ` 247` ```lemma normalize_quot_swap: ``` eberlm@63500 ` 248` ``` assumes "a \ 0" "b \ 0" ``` eberlm@63500 ` 249` ``` defines "a' \ fst (normalize_quot (a, b))" and "b' \ snd (normalize_quot (a, b))" ``` eberlm@63500 ` 250` ``` shows "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')" ``` eberlm@63500 ` 251` ```proof (rule normalize_quotI) ``` eberlm@63500 ` 252` ``` from normalize_quotE[OF assms(2), of a] guess d . note d = this [folded assms(3,4)] ``` eberlm@63500 ` 253` ``` show "b * (a' div unit_factor a') = a * (b' div unit_factor a')" ``` eberlm@63500 ` 254` ``` using assms(1,2) d ``` eberlm@63500 ` 255` ``` by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor) ``` eberlm@63500 ` 256` ``` have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot) ``` eberlm@63500 ` 257` ``` thus "(b' div unit_factor a', a' div unit_factor a') \ normalized_fracts" ``` eberlm@63500 ` 258` ``` using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute) ``` eberlm@63500 ` 259` ```qed fact+ ``` eberlm@63500 ` 260` ``` ``` eberlm@63500 ` 261` ```lemma quot_of_fract_inverse: ``` eberlm@63500 ` 262` ``` "quot_of_fract (inverse x) = ``` eberlm@63500 ` 263` ``` (let (a,b) = quot_of_fract x; d = unit_factor a ``` eberlm@63500 ` 264` ``` in if d = 0 then (0, 1) else (b div d, a div d))" ``` eberlm@63500 ` 265` ```proof (transfer, goal_cases) ``` eberlm@63500 ` 266` ``` case (1 x) ``` eberlm@63500 ` 267` ``` from normalize_quot_swap[of "fst x" "snd x"] show ?case ``` eberlm@63500 ` 268` ``` by (auto simp: Let_def case_prod_unfold) ``` eberlm@63500 ` 269` ```qed ``` eberlm@63500 ` 270` eberlm@63500 ` 271` ```lemma normalize_quot_div_unit_left: ``` eberlm@63500 ` 272` ``` fixes x y u ``` eberlm@63500 ` 273` ``` assumes "is_unit u" ``` eberlm@63500 ` 274` ``` defines "x' \ fst (normalize_quot (x, y))" and "y' \ snd (normalize_quot (x, y))" ``` eberlm@63500 ` 275` ``` shows "normalize_quot (x div u, y) = (x' div u, y')" ``` eberlm@63500 ` 276` ```proof (cases "y = 0") ``` eberlm@63500 ` 277` ``` case False ``` eberlm@63500 ` 278` ``` from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)] ``` eberlm@63500 ` 279` ``` from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot) ``` eberlm@63500 ` 280` ``` with False d \is_unit u\ show ?thesis ``` eberlm@63500 ` 281` ``` by (intro normalize_quotI) ``` eberlm@63500 ` 282` ``` (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel ``` eberlm@63500 ` 283` ``` gcd_div_unit1) ``` eberlm@63500 ` 284` ```qed (simp_all add: assms) ``` eberlm@63500 ` 285` eberlm@63500 ` 286` ```lemma normalize_quot_div_unit_right: ``` eberlm@63500 ` 287` ``` fixes x y u ``` eberlm@63500 ` 288` ``` assumes "is_unit u" ``` eberlm@63500 ` 289` ``` defines "x' \ fst (normalize_quot (x, y))" and "y' \ snd (normalize_quot (x, y))" ``` eberlm@63500 ` 290` ``` shows "normalize_quot (x, y div u) = (x' * u, y')" ``` eberlm@63500 ` 291` ```proof (cases "y = 0") ``` eberlm@63500 ` 292` ``` case False ``` eberlm@63500 ` 293` ``` from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)] ``` eberlm@63500 ` 294` ``` from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot) ``` eberlm@63500 ` 295` ``` with False d \is_unit u\ show ?thesis ``` eberlm@63500 ` 296` ``` by (intro normalize_quotI) ``` eberlm@63500 ` 297` ``` (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel ``` eberlm@63500 ` 298` ``` gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric]) ``` eberlm@63500 ` 299` ```qed (simp_all add: assms) ``` eberlm@63500 ` 300` eberlm@63500 ` 301` ```lemma normalize_quot_normalize_left: ``` eberlm@63500 ` 302` ``` fixes x y u ``` eberlm@63500 ` 303` ``` defines "x' \ fst (normalize_quot (x, y))" and "y' \ snd (normalize_quot (x, y))" ``` eberlm@63500 ` 304` ``` shows "normalize_quot (normalize x, y) = (x' div unit_factor x, y')" ``` eberlm@63500 ` 305` ``` using normalize_quot_div_unit_left[of "unit_factor x" x y] ``` eberlm@63500 ` 306` ``` by (cases "x = 0") (simp_all add: assms) ``` eberlm@63500 ` 307` ``` ``` eberlm@63500 ` 308` ```lemma normalize_quot_normalize_right: ``` eberlm@63500 ` 309` ``` fixes x y u ``` eberlm@63500 ` 310` ``` defines "x' \ fst (normalize_quot (x, y))" and "y' \ snd (normalize_quot (x, y))" ``` eberlm@63500 ` 311` ``` shows "normalize_quot (x, normalize y) = (x' * unit_factor y, y')" ``` eberlm@63500 ` 312` ``` using normalize_quot_div_unit_right[of "unit_factor y" x y] ``` eberlm@63500 ` 313` ``` by (cases "y = 0") (simp_all add: assms) ``` eberlm@63500 ` 314` ``` ``` eberlm@63500 ` 315` ```lemma quot_of_fract_0 [simp]: "quot_of_fract 0 = (0, 1)" ``` eberlm@63500 ` 316` ``` by transfer auto ``` eberlm@63500 ` 317` eberlm@63500 ` 318` ```lemma quot_of_fract_1 [simp]: "quot_of_fract 1 = (1, 1)" ``` eberlm@63500 ` 319` ``` by transfer (rule normalize_quotI, simp_all add: normalized_fracts_def) ``` eberlm@63500 ` 320` eberlm@63500 ` 321` ```lemma quot_of_fract_divide: ``` eberlm@63500 ` 322` ``` "quot_of_fract (x / y) = (if y = 0 then (0, 1) else ``` eberlm@63500 ` 323` ``` (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; ``` eberlm@63500 ` 324` ``` (e,f) = normalize_quot (a,c); (g,h) = normalize_quot (d,b) ``` eberlm@63500 ` 325` ``` in (e * g, f * h)))" (is "_ = ?rhs") ``` eberlm@63500 ` 326` ```proof (cases "y = 0") ``` eberlm@63500 ` 327` ``` case False ``` eberlm@63500 ` 328` ``` hence A: "fst (quot_of_fract y) \ 0" by transfer auto ``` eberlm@63500 ` 329` ``` have "x / y = x * inverse y" by (simp add: divide_inverse) ``` eberlm@63500 ` 330` ``` also from False A have "quot_of_fract \ = ?rhs" ``` eberlm@63500 ` 331` ``` by (simp only: quot_of_fract_mult quot_of_fract_inverse) ``` eberlm@63500 ` 332` ``` (simp_all add: Let_def case_prod_unfold fst_quot_of_fract_0_imp ``` eberlm@63500 ` 333` ``` normalize_quot_div_unit_left normalize_quot_div_unit_right ``` eberlm@63500 ` 334` ``` normalize_quot_normalize_right normalize_quot_normalize_left) ``` eberlm@63500 ` 335` ``` finally show ?thesis . ``` eberlm@63500 ` 336` ```qed simp_all ``` eberlm@63500 ` 337` eberlm@63500 ` 338` ```end ```