src/HOL/Computational_Algebra/Polynomial_Factorial.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (20 months ago) changeset 66817 0b12755ccbb2 parent 66808 1907167b6038 child 66838 17989f6bc7b2 permissions -rw-r--r--
euclidean rings need no normalization
 wenzelm@65435 ` 1` ```(* Title: HOL/Computational_Algebra/Polynomial_Factorial.thy ``` wenzelm@63764 ` 2` ``` Author: Manuel Eberl ``` wenzelm@63764 ` 3` ```*) ``` wenzelm@63764 ` 4` haftmann@66805 ` 5` ```section \Polynomials, fractions and rings\ ``` haftmann@66805 ` 6` eberlm@63498 ` 7` ```theory Polynomial_Factorial ``` eberlm@63498 ` 8` ```imports ``` eberlm@63498 ` 9` ``` Complex_Main ``` wenzelm@65366 ` 10` ``` Polynomial ``` wenzelm@65366 ` 11` ``` Normalized_Fraction ``` eberlm@63498 ` 12` ```begin ``` eberlm@63498 ` 13` eberlm@63498 ` 14` ```subsection \Lifting elements into the field of fractions\ ``` eberlm@63498 ` 15` haftmann@66805 ` 16` ```definition to_fract :: "'a :: idom \ 'a fract" ``` haftmann@66805 ` 17` ``` where "to_fract x = Fract x 1" ``` haftmann@66808 ` 18` ``` \ \FIXME: more idiomatic name, abbreviation\ ``` eberlm@63498 ` 19` eberlm@63498 ` 20` ```lemma to_fract_0 [simp]: "to_fract 0 = 0" ``` eberlm@63498 ` 21` ``` by (simp add: to_fract_def eq_fract Zero_fract_def) ``` eberlm@63498 ` 22` eberlm@63498 ` 23` ```lemma to_fract_1 [simp]: "to_fract 1 = 1" ``` eberlm@63498 ` 24` ``` by (simp add: to_fract_def eq_fract One_fract_def) ``` eberlm@63498 ` 25` eberlm@63498 ` 26` ```lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y" ``` eberlm@63498 ` 27` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 28` eberlm@63498 ` 29` ```lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y" ``` eberlm@63498 ` 30` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 31` ``` ``` eberlm@63498 ` 32` ```lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x" ``` eberlm@63498 ` 33` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 34` ``` ``` eberlm@63498 ` 35` ```lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y" ``` eberlm@63498 ` 36` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 37` eberlm@63498 ` 38` ```lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \ x = y" ``` eberlm@63498 ` 39` ``` by (simp add: to_fract_def eq_fract) ``` eberlm@63498 ` 40` ``` ``` eberlm@63498 ` 41` ```lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \ x = 0" ``` eberlm@63498 ` 42` ``` by (simp add: to_fract_def Zero_fract_def eq_fract) ``` eberlm@63498 ` 43` eberlm@63498 ` 44` ```lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \ 0" ``` eberlm@63498 ` 45` ``` by transfer simp ``` eberlm@63498 ` 46` eberlm@63498 ` 47` ```lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x" ``` eberlm@63498 ` 48` ``` by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp) ``` eberlm@63498 ` 49` eberlm@63498 ` 50` ```lemma to_fract_quot_of_fract: ``` eberlm@63498 ` 51` ``` assumes "snd (quot_of_fract x) = 1" ``` eberlm@63498 ` 52` ``` shows "to_fract (fst (quot_of_fract x)) = x" ``` eberlm@63498 ` 53` ```proof - ``` eberlm@63498 ` 54` ``` have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp ``` eberlm@63498 ` 55` ``` also note assms ``` eberlm@63498 ` 56` ``` finally show ?thesis by (simp add: to_fract_def) ``` eberlm@63498 ` 57` ```qed ``` eberlm@63498 ` 58` eberlm@63498 ` 59` ```lemma snd_quot_of_fract_Fract_whole: ``` eberlm@63498 ` 60` ``` assumes "y dvd x" ``` eberlm@63498 ` 61` ``` shows "snd (quot_of_fract (Fract x y)) = 1" ``` eberlm@63498 ` 62` ``` using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd) ``` eberlm@63498 ` 63` ``` ``` eberlm@63498 ` 64` ```lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b" ``` eberlm@63498 ` 65` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 66` eberlm@63498 ` 67` ```lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)" ``` eberlm@63498 ` 68` ``` unfolding to_fract_def by transfer (simp add: normalize_quot_def) ``` eberlm@63498 ` 69` eberlm@63498 ` 70` ```lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \ x = 0" ``` eberlm@63498 ` 71` ``` by transfer simp ``` eberlm@63498 ` 72` ``` ``` eberlm@63498 ` 73` ```lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1" ``` eberlm@63498 ` 74` ``` unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all ``` eberlm@63498 ` 75` eberlm@63498 ` 76` ```lemma coprime_quot_of_fract: ``` eberlm@63498 ` 77` ``` "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))" ``` eberlm@63498 ` 78` ``` by transfer (simp add: coprime_normalize_quot) ``` eberlm@63498 ` 79` eberlm@63498 ` 80` ```lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1" ``` eberlm@63498 ` 81` ``` using quot_of_fract_in_normalized_fracts[of x] ``` eberlm@63498 ` 82` ``` by (simp add: normalized_fracts_def case_prod_unfold) ``` eberlm@63498 ` 83` eberlm@63498 ` 84` ```lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \ normalize x = x" ``` eberlm@63498 ` 85` ``` by (subst (2) normalize_mult_unit_factor [symmetric, of x]) ``` eberlm@63498 ` 86` ``` (simp del: normalize_mult_unit_factor) ``` eberlm@63498 ` 87` ``` ``` eberlm@63498 ` 88` ```lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)" ``` eberlm@63498 ` 89` ``` by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract) ``` eberlm@63498 ` 90` eberlm@63498 ` 91` eberlm@63498 ` 92` ```subsection \Lifting polynomial coefficients to the field of fractions\ ``` eberlm@63498 ` 93` eberlm@63498 ` 94` ```abbreviation (input) fract_poly ``` eberlm@63498 ` 95` ``` where "fract_poly \ map_poly to_fract" ``` eberlm@63498 ` 96` eberlm@63498 ` 97` ```abbreviation (input) unfract_poly ``` eberlm@63498 ` 98` ``` where "unfract_poly \ map_poly (fst \ quot_of_fract)" ``` eberlm@63498 ` 99` ``` ``` eberlm@63498 ` 100` ```lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)" ``` eberlm@63498 ` 101` ``` by (simp add: smult_conv_map_poly map_poly_map_poly o_def) ``` eberlm@63498 ` 102` eberlm@63498 ` 103` ```lemma fract_poly_0 [simp]: "fract_poly 0 = 0" ``` eberlm@63498 ` 104` ``` by (simp add: poly_eqI coeff_map_poly) ``` eberlm@63498 ` 105` eberlm@63498 ` 106` ```lemma fract_poly_1 [simp]: "fract_poly 1 = 1" ``` haftmann@65486 ` 107` ``` by (simp add: map_poly_pCons) ``` eberlm@63498 ` 108` eberlm@63498 ` 109` ```lemma fract_poly_add [simp]: ``` eberlm@63498 ` 110` ``` "fract_poly (p + q) = fract_poly p + fract_poly q" ``` eberlm@63498 ` 111` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 112` eberlm@63498 ` 113` ```lemma fract_poly_diff [simp]: ``` eberlm@63498 ` 114` ``` "fract_poly (p - q) = fract_poly p - fract_poly q" ``` eberlm@63498 ` 115` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 116` nipkow@64267 ` 117` ```lemma to_fract_sum [simp]: "to_fract (sum f A) = sum (\x. to_fract (f x)) A" ``` eberlm@63498 ` 118` ``` by (cases "finite A", induction A rule: finite_induct) simp_all ``` eberlm@63498 ` 119` eberlm@63498 ` 120` ```lemma fract_poly_mult [simp]: ``` eberlm@63498 ` 121` ``` "fract_poly (p * q) = fract_poly p * fract_poly q" ``` eberlm@63498 ` 122` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult) ``` eberlm@63498 ` 123` eberlm@63498 ` 124` ```lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \ p = q" ``` eberlm@63498 ` 125` ``` by (auto simp: poly_eq_iff coeff_map_poly) ``` eberlm@63498 ` 126` eberlm@63498 ` 127` ```lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \ p = 0" ``` eberlm@63498 ` 128` ``` using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff) ``` eberlm@63498 ` 129` eberlm@63498 ` 130` ```lemma fract_poly_dvd: "p dvd q \ fract_poly p dvd fract_poly q" ``` eberlm@63498 ` 131` ``` by (auto elim!: dvdE) ``` eberlm@63498 ` 132` nipkow@63830 ` 133` ```lemma prod_mset_fract_poly: ``` haftmann@65390 ` 134` ``` "(\x\#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))" ``` haftmann@65390 ` 135` ``` by (induct A) (simp_all add: ac_simps) ``` eberlm@63498 ` 136` ``` ``` eberlm@63498 ` 137` ```lemma is_unit_fract_poly_iff: ``` eberlm@63498 ` 138` ``` "p dvd 1 \ fract_poly p dvd 1 \ content p = 1" ``` eberlm@63498 ` 139` ```proof safe ``` eberlm@63498 ` 140` ``` assume A: "p dvd 1" ``` haftmann@65389 ` 141` ``` with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)" ``` haftmann@65389 ` 142` ``` by simp ``` eberlm@63498 ` 143` ``` from A show "content p = 1" ``` eberlm@63498 ` 144` ``` by (auto simp: is_unit_poly_iff normalize_1_iff) ``` eberlm@63498 ` 145` ```next ``` eberlm@63498 ` 146` ``` assume A: "fract_poly p dvd 1" and B: "content p = 1" ``` eberlm@63498 ` 147` ``` from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 148` ``` { ``` eberlm@63498 ` 149` ``` fix n :: nat assume "n > 0" ``` eberlm@63498 ` 150` ``` have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly) ``` eberlm@63498 ` 151` ``` also note c ``` eberlm@63498 ` 152` ``` also from \n > 0\ have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits) ``` eberlm@63498 ` 153` ``` finally have "coeff p n = 0" by simp ``` eberlm@63498 ` 154` ``` } ``` eberlm@63498 ` 155` ``` hence "degree p \ 0" by (intro degree_le) simp_all ``` eberlm@63498 ` 156` ``` with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE) ``` eberlm@63498 ` 157` ```qed ``` eberlm@63498 ` 158` ``` ``` eberlm@63498 ` 159` ```lemma fract_poly_is_unit: "p dvd 1 \ fract_poly p dvd 1" ``` eberlm@63498 ` 160` ``` using fract_poly_dvd[of p 1] by simp ``` eberlm@63498 ` 161` eberlm@63498 ` 162` ```lemma fract_poly_smult_eqE: ``` eberlm@63498 ` 163` ``` fixes c :: "'a :: {idom_divide,ring_gcd} fract" ``` eberlm@63498 ` 164` ``` assumes "fract_poly p = smult c (fract_poly q)" ``` eberlm@63498 ` 165` ``` obtains a b ``` eberlm@63498 ` 166` ``` where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a" ``` eberlm@63498 ` 167` ```proof - ``` eberlm@63498 ` 168` ``` define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)" ``` eberlm@63498 ` 169` ``` have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)" ``` eberlm@63498 ` 170` ``` by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms) ``` eberlm@63498 ` 171` ``` hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff) ``` eberlm@63498 ` 172` ``` hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff) ``` eberlm@63498 ` 173` ``` moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b" ``` eberlm@63498 ` 174` ``` by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute ``` eberlm@63498 ` 175` ``` normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric]) ``` eberlm@63498 ` 176` ``` ultimately show ?thesis by (intro that[of a b]) ``` eberlm@63498 ` 177` ```qed ``` eberlm@63498 ` 178` eberlm@63498 ` 179` eberlm@63498 ` 180` ```subsection \Fractional content\ ``` eberlm@63498 ` 181` eberlm@63498 ` 182` ```abbreviation (input) Lcm_coeff_denoms ``` eberlm@63498 ` 183` ``` :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \ 'a" ``` eberlm@63498 ` 184` ``` where "Lcm_coeff_denoms p \ Lcm (snd ` quot_of_fract ` set (coeffs p))" ``` eberlm@63498 ` 185` ``` ``` eberlm@63498 ` 186` ```definition fract_content :: ``` eberlm@63498 ` 187` ``` "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \ 'a fract" where ``` eberlm@63498 ` 188` ``` "fract_content p = ``` eberlm@63498 ` 189` ``` (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" ``` eberlm@63498 ` 190` eberlm@63498 ` 191` ```definition primitive_part_fract :: ``` eberlm@63498 ` 192` ``` "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \ 'a poly" where ``` eberlm@63498 ` 193` ``` "primitive_part_fract p = ``` eberlm@63498 ` 194` ``` primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))" ``` eberlm@63498 ` 195` eberlm@63498 ` 196` ```lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0" ``` eberlm@63498 ` 197` ``` by (simp add: primitive_part_fract_def) ``` eberlm@63498 ` 198` eberlm@63498 ` 199` ```lemma fract_content_eq_0_iff [simp]: ``` eberlm@63498 ` 200` ``` "fract_content p = 0 \ p = 0" ``` eberlm@63498 ` 201` ``` unfolding fract_content_def Let_def Zero_fract_def ``` eberlm@63498 ` 202` ``` by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff) ``` eberlm@63498 ` 203` eberlm@63498 ` 204` ```lemma content_primitive_part_fract [simp]: "p \ 0 \ content (primitive_part_fract p) = 1" ``` eberlm@63498 ` 205` ``` unfolding primitive_part_fract_def ``` eberlm@63498 ` 206` ``` by (rule content_primitive_part) ``` eberlm@63498 ` 207` ``` (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) ``` eberlm@63498 ` 208` eberlm@63498 ` 209` ```lemma content_times_primitive_part_fract: ``` eberlm@63498 ` 210` ``` "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p" ``` eberlm@63498 ` 211` ```proof - ``` eberlm@63498 ` 212` ``` define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)" ``` eberlm@63498 ` 213` ``` have "fract_poly p' = ``` eberlm@63498 ` 214` ``` map_poly (to_fract \ fst \ quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)" ``` eberlm@63498 ` 215` ``` unfolding primitive_part_fract_def p'_def ``` eberlm@63498 ` 216` ``` by (subst map_poly_map_poly) (simp_all add: o_assoc) ``` eberlm@63498 ` 217` ``` also have "\ = smult (to_fract (Lcm_coeff_denoms p)) p" ``` eberlm@63498 ` 218` ``` proof (intro map_poly_idI, unfold o_apply) ``` eberlm@63498 ` 219` ``` fix c assume "c \ set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))" ``` eberlm@63498 ` 220` ``` then obtain c' where c: "c' \ set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'" ``` eberlm@63498 ` 221` ``` by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits) ``` eberlm@63498 ` 222` ``` note c(2) ``` eberlm@63498 ` 223` ``` also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))" ``` eberlm@63498 ` 224` ``` by simp ``` eberlm@63498 ` 225` ``` also have "to_fract (Lcm_coeff_denoms p) * \ = ``` eberlm@63498 ` 226` ``` Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))" ``` eberlm@63498 ` 227` ``` unfolding to_fract_def by (subst mult_fract) simp_all ``` eberlm@63498 ` 228` ``` also have "snd (quot_of_fract \) = 1" ``` eberlm@63498 ` 229` ``` by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto) ``` eberlm@63498 ` 230` ``` finally show "to_fract (fst (quot_of_fract c)) = c" ``` eberlm@63498 ` 231` ``` by (rule to_fract_quot_of_fract) ``` eberlm@63498 ` 232` ``` qed ``` eberlm@63498 ` 233` ``` also have "p' = smult (content p') (primitive_part p')" ``` eberlm@63498 ` 234` ``` by (rule content_times_primitive_part [symmetric]) ``` eberlm@63498 ` 235` ``` also have "primitive_part p' = primitive_part_fract p" ``` eberlm@63498 ` 236` ``` by (simp add: primitive_part_fract_def p'_def) ``` eberlm@63498 ` 237` ``` also have "fract_poly (smult (content p') (primitive_part_fract p)) = ``` eberlm@63498 ` 238` ``` smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp ``` eberlm@63498 ` 239` ``` finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) = ``` eberlm@63498 ` 240` ``` smult (to_fract (Lcm_coeff_denoms p)) p" . ``` eberlm@63498 ` 241` ``` thus ?thesis ``` eberlm@63498 ` 242` ``` by (subst (asm) smult_eq_iff) ``` eberlm@63498 ` 243` ``` (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def) ``` eberlm@63498 ` 244` ```qed ``` eberlm@63498 ` 245` eberlm@63498 ` 246` ```lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)" ``` eberlm@63498 ` 247` ```proof - ``` eberlm@63498 ` 248` ``` have "Lcm_coeff_denoms (fract_poly p) = 1" ``` haftmann@63905 ` 249` ``` by (auto simp: set_coeffs_map_poly) ``` eberlm@63498 ` 250` ``` hence "fract_content (fract_poly p) = ``` eberlm@63498 ` 251` ``` to_fract (content (map_poly (fst \ quot_of_fract \ to_fract) p))" ``` eberlm@63498 ` 252` ``` by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff) ``` eberlm@63498 ` 253` ``` also have "map_poly (fst \ quot_of_fract \ to_fract) p = p" ``` eberlm@63498 ` 254` ``` by (intro map_poly_idI) simp_all ``` eberlm@63498 ` 255` ``` finally show ?thesis . ``` eberlm@63498 ` 256` ```qed ``` eberlm@63498 ` 257` eberlm@63498 ` 258` ```lemma content_decompose_fract: ``` eberlm@63498 ` 259` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly" ``` eberlm@63498 ` 260` ``` obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1" ``` eberlm@63498 ` 261` ```proof (cases "p = 0") ``` eberlm@63498 ` 262` ``` case True ``` eberlm@63498 ` 263` ``` hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all ``` eberlm@63498 ` 264` ``` thus ?thesis .. ``` eberlm@63498 ` 265` ```next ``` eberlm@63498 ` 266` ``` case False ``` eberlm@63498 ` 267` ``` thus ?thesis ``` eberlm@63498 ` 268` ``` by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract]) ``` eberlm@63498 ` 269` ```qed ``` eberlm@63498 ` 270` eberlm@63498 ` 271` eberlm@63498 ` 272` ```subsection \More properties of content and primitive part\ ``` eberlm@63498 ` 273` eberlm@63498 ` 274` ```lemma lift_prime_elem_poly: ``` eberlm@63633 ` 275` ``` assumes "prime_elem (c :: 'a :: semidom)" ``` eberlm@63633 ` 276` ``` shows "prime_elem [:c:]" ``` eberlm@63633 ` 277` ```proof (rule prime_elemI) ``` eberlm@63498 ` 278` ``` fix a b assume *: "[:c:] dvd a * b" ``` eberlm@63498 ` 279` ``` from * have dvd: "c dvd coeff (a * b) n" for n ``` eberlm@63498 ` 280` ``` by (subst (asm) const_poly_dvd_iff) blast ``` eberlm@63498 ` 281` ``` { ``` eberlm@63498 ` 282` ``` define m where "m = (GREATEST m. \c dvd coeff b m)" ``` eberlm@63498 ` 283` ``` assume "\[:c:] dvd b" ``` eberlm@63498 ` 284` ``` hence A: "\i. \c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast ``` nipkow@65963 ` 285` ``` have B: "\i. \c dvd coeff b i \ i \ degree b" ``` nipkow@65963 ` 286` ``` by (auto intro: le_degree) ``` nipkow@65965 ` 287` ``` have coeff_m: "\c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B]) ``` eberlm@63498 ` 288` ``` have "i \ m" if "\c dvd coeff b i" for i ``` nipkow@65965 ` 289` ``` unfolding m_def by (rule Greatest_le_nat[OF that B]) ``` eberlm@63498 ` 290` ``` hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force ``` eberlm@63498 ` 291` eberlm@63498 ` 292` ``` have "c dvd coeff a i" for i ``` eberlm@63498 ` 293` ``` proof (induction i rule: nat_descend_induct[of "degree a"]) ``` eberlm@63498 ` 294` ``` case (base i) ``` eberlm@63498 ` 295` ``` thus ?case by (simp add: coeff_eq_0) ``` eberlm@63498 ` 296` ``` next ``` eberlm@63498 ` 297` ``` case (descend i) ``` eberlm@63498 ` 298` ``` let ?A = "{..i+m} - {i}" ``` eberlm@63498 ` 299` ``` have "c dvd coeff (a * b) (i + m)" by (rule dvd) ``` eberlm@63498 ` 300` ``` also have "coeff (a * b) (i + m) = (\k\i + m. coeff a k * coeff b (i + m - k))" ``` eberlm@63498 ` 301` ``` by (simp add: coeff_mult) ``` eberlm@63498 ` 302` ``` also have "{..i+m} = insert i ?A" by auto ``` eberlm@63498 ` 303` ``` also have "(\k\\. coeff a k * coeff b (i + m - k)) = ``` eberlm@63498 ` 304` ``` coeff a i * coeff b m + (\k\?A. coeff a k * coeff b (i + m - k))" ``` eberlm@63498 ` 305` ``` (is "_ = _ + ?S") ``` nipkow@64267 ` 306` ``` by (subst sum.insert) simp_all ``` eberlm@63498 ` 307` ``` finally have eq: "c dvd coeff a i * coeff b m + ?S" . ``` eberlm@63498 ` 308` ``` moreover have "c dvd ?S" ``` nipkow@64267 ` 309` ``` proof (rule dvd_sum) ``` eberlm@63498 ` 310` ``` fix k assume k: "k \ {..i+m} - {i}" ``` eberlm@63498 ` 311` ``` show "c dvd coeff a k * coeff b (i + m - k)" ``` eberlm@63498 ` 312` ``` proof (cases "k < i") ``` eberlm@63498 ` 313` ``` case False ``` eberlm@63498 ` 314` ``` with k have "c dvd coeff a k" by (intro descend.IH) simp ``` eberlm@63498 ` 315` ``` thus ?thesis by simp ``` eberlm@63498 ` 316` ``` next ``` eberlm@63498 ` 317` ``` case True ``` eberlm@63498 ` 318` ``` hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp ``` eberlm@63498 ` 319` ``` thus ?thesis by simp ``` eberlm@63498 ` 320` ``` qed ``` eberlm@63498 ` 321` ``` qed ``` eberlm@63498 ` 322` ``` ultimately have "c dvd coeff a i * coeff b m" ``` eberlm@63498 ` 323` ``` by (simp add: dvd_add_left_iff) ``` eberlm@63498 ` 324` ``` with assms coeff_m show "c dvd coeff a i" ``` eberlm@63633 ` 325` ``` by (simp add: prime_elem_dvd_mult_iff) ``` eberlm@63498 ` 326` ``` qed ``` eberlm@63498 ` 327` ``` hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast ``` eberlm@63498 ` 328` ``` } ``` haftmann@65486 ` 329` ``` then show "[:c:] dvd a \ [:c:] dvd b" by blast ``` haftmann@65486 ` 330` ```next ``` haftmann@65486 ` 331` ``` from assms show "[:c:] \ 0" and "\ [:c:] dvd 1" ``` haftmann@65486 ` 332` ``` by (simp_all add: prime_elem_def is_unit_const_poly_iff) ``` haftmann@65486 ` 333` ```qed ``` eberlm@63498 ` 334` eberlm@63498 ` 335` ```lemma prime_elem_const_poly_iff: ``` eberlm@63498 ` 336` ``` fixes c :: "'a :: semidom" ``` eberlm@63633 ` 337` ``` shows "prime_elem [:c:] \ prime_elem c" ``` eberlm@63498 ` 338` ```proof ``` eberlm@63633 ` 339` ``` assume A: "prime_elem [:c:]" ``` eberlm@63633 ` 340` ``` show "prime_elem c" ``` eberlm@63633 ` 341` ``` proof (rule prime_elemI) ``` eberlm@63498 ` 342` ``` fix a b assume "c dvd a * b" ``` eberlm@63498 ` 343` ``` hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac) ``` eberlm@63633 ` 344` ``` from A and this have "[:c:] dvd [:a:] \ [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD) ``` eberlm@63498 ` 345` ``` thus "c dvd a \ c dvd b" by simp ``` eberlm@63633 ` 346` ``` qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) ``` eberlm@63498 ` 347` ```qed (auto intro: lift_prime_elem_poly) ``` eberlm@63498 ` 348` eberlm@63498 ` 349` ```context ``` eberlm@63498 ` 350` ```begin ``` eberlm@63498 ` 351` eberlm@63498 ` 352` ```private lemma content_1_mult: ``` eberlm@63498 ` 353` ``` fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly" ``` eberlm@63498 ` 354` ``` assumes "content f = 1" "content g = 1" ``` eberlm@63498 ` 355` ``` shows "content (f * g) = 1" ``` eberlm@63498 ` 356` ```proof (cases "f * g = 0") ``` eberlm@63498 ` 357` ``` case False ``` eberlm@63498 ` 358` ``` from assms have "f \ 0" "g \ 0" by auto ``` eberlm@63498 ` 359` eberlm@63498 ` 360` ``` hence "f * g \ 0" by auto ``` eberlm@63498 ` 361` ``` { ``` eberlm@63498 ` 362` ``` assume "\is_unit (content (f * g))" ``` eberlm@63633 ` 363` ``` with False have "\p. p dvd content (f * g) \ prime p" ``` eberlm@63498 ` 364` ``` by (intro prime_divisor_exists) simp_all ``` eberlm@63633 ` 365` ``` then obtain p where "p dvd content (f * g)" "prime p" by blast ``` eberlm@63498 ` 366` ``` from \p dvd content (f * g)\ have "[:p:] dvd f * g" ``` eberlm@63498 ` 367` ``` by (simp add: const_poly_dvd_iff_dvd_content) ``` eberlm@63633 ` 368` ``` moreover from \prime p\ have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) ``` eberlm@63498 ` 369` ``` ultimately have "[:p:] dvd f \ [:p:] dvd g" ``` eberlm@63633 ` 370` ``` by (simp add: prime_elem_dvd_mult_iff) ``` eberlm@63498 ` 371` ``` with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) ``` eberlm@63633 ` 372` ``` with \prime p\ have False by simp ``` eberlm@63498 ` 373` ``` } ``` eberlm@63498 ` 374` ``` hence "is_unit (content (f * g))" by blast ``` eberlm@63498 ` 375` ``` hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) ``` eberlm@63498 ` 376` ``` thus ?thesis by simp ``` eberlm@63498 ` 377` ```qed (insert assms, auto) ``` eberlm@63498 ` 378` eberlm@63498 ` 379` ```lemma content_mult: ``` eberlm@63498 ` 380` ``` fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" ``` eberlm@63498 ` 381` ``` shows "content (p * q) = content p * content q" ``` eberlm@63498 ` 382` ```proof - ``` eberlm@63498 ` 383` ``` from content_decompose[of p] guess p' . note p = this ``` eberlm@63498 ` 384` ``` from content_decompose[of q] guess q' . note q = this ``` eberlm@63498 ` 385` ``` have "content (p * q) = content p * content q * content (p' * q')" ``` eberlm@63498 ` 386` ``` by (subst p, subst q) (simp add: mult_ac normalize_mult) ``` eberlm@63498 ` 387` ``` also from p q have "content (p' * q') = 1" by (intro content_1_mult) ``` eberlm@63498 ` 388` ``` finally show ?thesis by simp ``` eberlm@63498 ` 389` ```qed ``` eberlm@63498 ` 390` eberlm@63498 ` 391` ```lemma fract_poly_dvdD: ``` eberlm@63498 ` 392` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 393` ``` assumes "fract_poly p dvd fract_poly q" "content p = 1" ``` eberlm@63498 ` 394` ``` shows "p dvd q" ``` eberlm@63498 ` 395` ```proof - ``` eberlm@63498 ` 396` ``` from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE) ``` eberlm@63498 ` 397` ``` from content_decompose_fract[of r] guess c r' . note r' = this ``` eberlm@63498 ` 398` ``` from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp ``` eberlm@63498 ` 399` ``` from fract_poly_smult_eqE[OF this] guess a b . note ab = this ``` eberlm@63498 ` 400` ``` have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2)) ``` eberlm@63498 ` 401` ``` hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4)) ``` eberlm@63498 ` 402` ``` have "1 = gcd a (normalize b)" by (simp add: ab) ``` eberlm@63498 ` 403` ``` also note eq' ``` eberlm@63498 ` 404` ``` also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4)) ``` eberlm@63498 ` 405` ``` finally have [simp]: "a = 1" by simp ``` eberlm@63498 ` 406` ``` from eq ab have "q = p * ([:b:] * r')" by simp ``` eberlm@63498 ` 407` ``` thus ?thesis by (rule dvdI) ``` eberlm@63498 ` 408` ```qed ``` eberlm@63498 ` 409` eberlm@63498 ` 410` ```end ``` eberlm@63498 ` 411` eberlm@63498 ` 412` eberlm@63498 ` 413` ```subsection \Polynomials over a field are a Euclidean ring\ ``` eberlm@63498 ` 414` haftmann@66805 ` 415` ```context ``` haftmann@66805 ` 416` ```begin ``` eberlm@63498 ` 417` eberlm@63498 ` 418` ```interpretation field_poly: ``` haftmann@66817 ` 419` ``` normalization_euclidean_semiring where zero = "0 :: 'a :: field poly" ``` haftmann@66817 ` 420` ``` and one = 1 and plus = plus and minus = minus ``` haftmann@64164 ` 421` ``` and times = times ``` haftmann@66805 ` 422` ``` and normalize = "\p. smult (inverse (lead_coeff p)) p" ``` haftmann@66805 ` 423` ``` and unit_factor = "\p. [:lead_coeff p:]" ``` haftmann@66805 ` 424` ``` and euclidean_size = "\p. if p = 0 then 0 else 2 ^ degree p" ``` haftmann@64164 ` 425` ``` and divide = divide and modulo = modulo ``` haftmann@66805 ` 426` ``` rewrites "dvd.dvd (times :: 'a poly \ _) = Rings.dvd" ``` haftmann@66805 ` 427` ``` and "comm_monoid_mult.prod_mset times 1 = prod_mset" ``` haftmann@66805 ` 428` ``` and "comm_semiring_1.irreducible times 1 0 = irreducible" ``` haftmann@66805 ` 429` ``` and "comm_semiring_1.prime_elem times 1 0 = prime_elem" ``` haftmann@66805 ` 430` ```proof - ``` haftmann@66805 ` 431` ``` show "dvd.dvd (times :: 'a poly \ _) = Rings.dvd" ``` haftmann@66805 ` 432` ``` by (simp add: dvd_dict) ``` haftmann@66805 ` 433` ``` show "comm_monoid_mult.prod_mset times 1 = prod_mset" ``` haftmann@66805 ` 434` ``` by (simp add: prod_mset_dict) ``` haftmann@66805 ` 435` ``` show "comm_semiring_1.irreducible times 1 0 = irreducible" ``` haftmann@66805 ` 436` ``` by (simp add: irreducible_dict) ``` haftmann@66805 ` 437` ``` show "comm_semiring_1.prime_elem times 1 0 = prime_elem" ``` haftmann@66805 ` 438` ``` by (simp add: prime_elem_dict) ``` haftmann@66817 ` 439` ``` show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1 ``` haftmann@66817 ` 440` ``` modulo (\p. if p = 0 then 0 else 2 ^ degree p) ``` haftmann@66817 ` 441` ``` (\p. [:lead_coeff p:]) (\p. smult (inverse (lead_coeff p)) p)" ``` haftmann@66805 ` 442` ``` proof (standard, fold dvd_dict) ``` haftmann@66805 ` 443` ``` fix p :: "'a poly" ``` haftmann@66805 ` 444` ``` show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p" ``` haftmann@66805 ` 445` ``` by (cases "p = 0") simp_all ``` haftmann@66805 ` 446` ``` next ``` haftmann@66805 ` 447` ``` fix p :: "'a poly" assume "is_unit p" ``` haftmann@66805 ` 448` ``` then show "[:lead_coeff p:] = p" ``` haftmann@66805 ` 449` ``` by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps) ``` haftmann@66805 ` 450` ``` next ``` haftmann@66805 ` 451` ``` fix p :: "'a poly" assume "p \ 0" ``` haftmann@66805 ` 452` ``` then show "is_unit [:lead_coeff p:]" ``` haftmann@66805 ` 453` ``` by (simp add: is_unit_pCons_iff) ``` haftmann@66805 ` 454` ``` qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) ``` haftmann@66805 ` 455` ```qed ``` eberlm@63498 ` 456` eberlm@63722 ` 457` ```lemma field_poly_irreducible_imp_prime: ``` haftmann@66805 ` 458` ``` "prime_elem p" if "irreducible p" for p :: "'a :: field poly" ``` haftmann@66805 ` 459` ``` using that by (fact field_poly.irreducible_imp_prime_elem) ``` eberlm@63498 ` 460` nipkow@63830 ` 461` ```lemma field_poly_prod_mset_prime_factorization: ``` haftmann@66805 ` 462` ``` "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p" ``` haftmann@66805 ` 463` ``` if "p \ 0" for p :: "'a :: field poly" ``` haftmann@66805 ` 464` ``` using that by (fact field_poly.prod_mset_prime_factorization) ``` eberlm@63498 ` 465` eberlm@63722 ` 466` ```lemma field_poly_in_prime_factorization_imp_prime: ``` haftmann@66805 ` 467` ``` "prime_elem p" if "p \# field_poly.prime_factorization x" ``` haftmann@66805 ` 468` ``` for p :: "'a :: field poly" ``` haftmann@66805 ` 469` ``` by (rule field_poly.prime_imp_prime_elem, rule field_poly.in_prime_factors_imp_prime) ``` haftmann@66805 ` 470` ``` (fact that) ``` eberlm@63498 ` 471` eberlm@63498 ` 472` eberlm@63498 ` 473` ```subsection \Primality and irreducibility in polynomial rings\ ``` eberlm@63498 ` 474` eberlm@63498 ` 475` ```lemma nonconst_poly_irreducible_iff: ``` eberlm@63498 ` 476` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 477` ``` assumes "degree p \ 0" ``` eberlm@63498 ` 478` ``` shows "irreducible p \ irreducible (fract_poly p) \ content p = 1" ``` eberlm@63498 ` 479` ```proof safe ``` eberlm@63498 ` 480` ``` assume p: "irreducible p" ``` eberlm@63498 ` 481` eberlm@63498 ` 482` ``` from content_decompose[of p] guess p' . note p' = this ``` eberlm@63498 ` 483` ``` hence "p = [:content p:] * p'" by simp ``` eberlm@63498 ` 484` ``` from p this have "[:content p:] dvd 1 \ p' dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 485` ``` moreover have "\p' dvd 1" ``` eberlm@63498 ` 486` ``` proof ``` eberlm@63498 ` 487` ``` assume "p' dvd 1" ``` eberlm@63498 ` 488` ``` hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 489` ``` with assms show False by contradiction ``` eberlm@63498 ` 490` ``` qed ``` eberlm@63498 ` 491` ``` ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff) ``` eberlm@63498 ` 492` ``` ``` eberlm@63498 ` 493` ``` show "irreducible (map_poly to_fract p)" ``` eberlm@63498 ` 494` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 495` ``` have "fract_poly p = 0 \ p = 0" by (intro map_poly_eq_0_iff) auto ``` eberlm@63498 ` 496` ``` with assms show "map_poly to_fract p \ 0" by auto ``` eberlm@63498 ` 497` ``` next ``` eberlm@63498 ` 498` ``` show "\is_unit (fract_poly p)" ``` eberlm@63498 ` 499` ``` proof ``` eberlm@63498 ` 500` ``` assume "is_unit (map_poly to_fract p)" ``` eberlm@63498 ` 501` ``` hence "degree (map_poly to_fract p) = 0" ``` eberlm@63498 ` 502` ``` by (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 503` ``` hence "degree p = 0" by (simp add: degree_map_poly) ``` eberlm@63498 ` 504` ``` with assms show False by contradiction ``` eberlm@63498 ` 505` ``` qed ``` eberlm@63498 ` 506` ``` next ``` eberlm@63498 ` 507` ``` fix q r assume qr: "fract_poly p = q * r" ``` eberlm@63498 ` 508` ``` from content_decompose_fract[of q] guess cg q' . note q = this ``` eberlm@63498 ` 509` ``` from content_decompose_fract[of r] guess cr r' . note r = this ``` eberlm@63498 ` 510` ``` from qr q r p have nz: "cg \ 0" "cr \ 0" by auto ``` eberlm@63498 ` 511` ``` from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))" ``` eberlm@63498 ` 512` ``` by (simp add: q r) ``` eberlm@63498 ` 513` ``` from fract_poly_smult_eqE[OF this] guess a b . note ab = this ``` eberlm@63498 ` 514` ``` hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:) ``` eberlm@63498 ` 515` ``` with ab(4) have a: "a = normalize b" by (simp add: content_mult q r) ``` eberlm@63498 ` 516` ``` hence "normalize b = gcd a b" by simp ``` eberlm@63498 ` 517` ``` also from ab(3) have "\ = 1" . ``` eberlm@63498 ` 518` ``` finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff) ``` eberlm@63498 ` 519` ``` ``` eberlm@63498 ` 520` ``` note eq ``` eberlm@63498 ` 521` ``` also from ab(1) \a = 1\ have "cr * cg = to_fract b" by simp ``` eberlm@63498 ` 522` ``` also have "smult \ (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp ``` eberlm@63498 ` 523` ``` finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult) ``` eberlm@63498 ` 524` ``` from p and this have "([:b:] * q') dvd 1 \ r' dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 525` ``` hence "q' dvd 1 \ r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left) ``` eberlm@63498 ` 526` ``` hence "fract_poly q' dvd 1 \ fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit) ``` eberlm@63498 ` 527` ``` with q r show "is_unit q \ is_unit r" ``` eberlm@63498 ` 528` ``` by (auto simp add: is_unit_smult_iff dvd_field_iff nz) ``` eberlm@63498 ` 529` ``` qed ``` eberlm@63498 ` 530` eberlm@63498 ` 531` ```next ``` eberlm@63498 ` 532` eberlm@63498 ` 533` ``` assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1" ``` eberlm@63498 ` 534` ``` show "irreducible p" ``` eberlm@63498 ` 535` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 536` ``` from irred show "p \ 0" by auto ``` eberlm@63498 ` 537` ``` next ``` eberlm@63498 ` 538` ``` from irred show "\p dvd 1" ``` eberlm@63498 ` 539` ``` by (auto simp: irreducible_def dest: fract_poly_is_unit) ``` eberlm@63498 ` 540` ``` next ``` eberlm@63498 ` 541` ``` fix q r assume qr: "p = q * r" ``` eberlm@63498 ` 542` ``` hence "fract_poly p = fract_poly q * fract_poly r" by simp ``` eberlm@63498 ` 543` ``` from irred and this have "fract_poly q dvd 1 \ fract_poly r dvd 1" ``` eberlm@63498 ` 544` ``` by (rule irreducibleD) ``` eberlm@63498 ` 545` ``` with primitive qr show "q dvd 1 \ r dvd 1" ``` eberlm@63498 ` 546` ``` by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) ``` eberlm@63498 ` 547` ``` qed ``` eberlm@63498 ` 548` ```qed ``` eberlm@63498 ` 549` eberlm@63498 ` 550` ```private lemma irreducible_imp_prime_poly: ``` eberlm@63498 ` 551` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 552` ``` assumes "irreducible p" ``` eberlm@63633 ` 553` ``` shows "prime_elem p" ``` eberlm@63498 ` 554` ```proof (cases "degree p = 0") ``` eberlm@63498 ` 555` ``` case True ``` eberlm@63498 ` 556` ``` with assms show ?thesis ``` eberlm@63498 ` 557` ``` by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff ``` eberlm@63633 ` 558` ``` intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE) ``` eberlm@63498 ` 559` ```next ``` eberlm@63498 ` 560` ``` case False ``` eberlm@63498 ` 561` ``` from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1" ``` eberlm@63498 ` 562` ``` by (simp_all add: nonconst_poly_irreducible_iff) ``` eberlm@63633 ` 563` ``` from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime) ``` eberlm@63498 ` 564` ``` show ?thesis ``` eberlm@63633 ` 565` ``` proof (rule prime_elemI) ``` eberlm@63498 ` 566` ``` fix q r assume "p dvd q * r" ``` eberlm@63498 ` 567` ``` hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd) ``` eberlm@63498 ` 568` ``` hence "fract_poly p dvd fract_poly q * fract_poly r" by simp ``` eberlm@63498 ` 569` ``` from prime and this have "fract_poly p dvd fract_poly q \ fract_poly p dvd fract_poly r" ``` eberlm@63633 ` 570` ``` by (rule prime_elem_dvd_multD) ``` eberlm@63498 ` 571` ``` with primitive show "p dvd q \ p dvd r" by (auto dest: fract_poly_dvdD) ``` eberlm@63498 ` 572` ``` qed (insert assms, auto simp: irreducible_def) ``` eberlm@63498 ` 573` ```qed ``` eberlm@63498 ` 574` eberlm@63498 ` 575` ```lemma degree_primitive_part_fract [simp]: ``` eberlm@63498 ` 576` ``` "degree (primitive_part_fract p) = degree p" ``` eberlm@63498 ` 577` ```proof - ``` eberlm@63498 ` 578` ``` have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))" ``` eberlm@63498 ` 579` ``` by (simp add: content_times_primitive_part_fract) ``` eberlm@63498 ` 580` ``` also have "degree \ = degree (primitive_part_fract p)" ``` eberlm@63498 ` 581` ``` by (auto simp: degree_map_poly) ``` eberlm@63498 ` 582` ``` finally show ?thesis .. ``` eberlm@63498 ` 583` ```qed ``` eberlm@63498 ` 584` eberlm@63498 ` 585` ```lemma irreducible_primitive_part_fract: ``` eberlm@63498 ` 586` ``` fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" ``` eberlm@63498 ` 587` ``` assumes "irreducible p" ``` eberlm@63498 ` 588` ``` shows "irreducible (primitive_part_fract p)" ``` eberlm@63498 ` 589` ```proof - ``` eberlm@63498 ` 590` ``` from assms have deg: "degree (primitive_part_fract p) \ 0" ``` eberlm@63498 ` 591` ``` by (intro notI) ``` eberlm@63498 ` 592` ``` (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff) ``` eberlm@63498 ` 593` ``` hence [simp]: "p \ 0" by auto ``` eberlm@63498 ` 594` eberlm@63498 ` 595` ``` note \irreducible p\ ``` eberlm@63498 ` 596` ``` also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" ``` eberlm@63498 ` 597` ``` by (simp add: content_times_primitive_part_fract) ``` eberlm@63498 ` 598` ``` also have "irreducible \ \ irreducible (fract_poly (primitive_part_fract p))" ``` eberlm@63498 ` 599` ``` by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff) ``` eberlm@63498 ` 600` ``` finally show ?thesis using deg ``` eberlm@63498 ` 601` ``` by (simp add: nonconst_poly_irreducible_iff) ``` eberlm@63498 ` 602` ```qed ``` eberlm@63498 ` 603` eberlm@63633 ` 604` ```lemma prime_elem_primitive_part_fract: ``` eberlm@63498 ` 605` ``` fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" ``` eberlm@63633 ` 606` ``` shows "irreducible p \ prime_elem (primitive_part_fract p)" ``` eberlm@63498 ` 607` ``` by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) ``` eberlm@63498 ` 608` eberlm@63498 ` 609` ```lemma irreducible_linear_field_poly: ``` eberlm@63498 ` 610` ``` fixes a b :: "'a::field" ``` eberlm@63498 ` 611` ``` assumes "b \ 0" ``` eberlm@63498 ` 612` ``` shows "irreducible [:a,b:]" ``` eberlm@63498 ` 613` ```proof (rule irreducibleI) ``` eberlm@63498 ` 614` ``` fix p q assume pq: "[:a,b:] = p * q" ``` wenzelm@63539 ` 615` ``` also from pq assms have "degree \ = degree p + degree q" ``` eberlm@63498 ` 616` ``` by (intro degree_mult_eq) auto ``` eberlm@63498 ` 617` ``` finally have "degree p = 0 \ degree q = 0" using assms by auto ``` eberlm@63498 ` 618` ``` with assms pq show "is_unit p \ is_unit q" ``` eberlm@63498 ` 619` ``` by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE) ``` eberlm@63498 ` 620` ```qed (insert assms, auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 621` eberlm@63633 ` 622` ```lemma prime_elem_linear_field_poly: ``` eberlm@63633 ` 623` ``` "(b :: 'a :: field) \ 0 \ prime_elem [:a,b:]" ``` eberlm@63498 ` 624` ``` by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) ``` eberlm@63498 ` 625` eberlm@63498 ` 626` ```lemma irreducible_linear_poly: ``` eberlm@63498 ` 627` ``` fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" ``` eberlm@63498 ` 628` ``` shows "b \ 0 \ coprime a b \ irreducible [:a,b:]" ``` eberlm@63498 ` 629` ``` by (auto intro!: irreducible_linear_field_poly ``` eberlm@63498 ` 630` ``` simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) ``` eberlm@63498 ` 631` eberlm@63633 ` 632` ```lemma prime_elem_linear_poly: ``` eberlm@63498 ` 633` ``` fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" ``` eberlm@63633 ` 634` ``` shows "b \ 0 \ coprime a b \ prime_elem [:a,b:]" ``` eberlm@63498 ` 635` ``` by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly) ``` eberlm@63498 ` 636` haftmann@64591 ` 637` ``` ``` eberlm@63498 ` 638` ```subsection \Prime factorisation of polynomials\ ``` eberlm@63498 ` 639` eberlm@63498 ` 640` ```private lemma poly_prime_factorization_exists_content_1: ``` eberlm@63498 ` 641` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 642` ``` assumes "p \ 0" "content p = 1" ``` nipkow@63830 ` 643` ``` shows "\A. (\p. p \# A \ prime_elem p) \ prod_mset A = normalize p" ``` eberlm@63498 ` 644` ```proof - ``` eberlm@63498 ` 645` ``` let ?P = "field_poly.prime_factorization (fract_poly p)" ``` nipkow@63830 ` 646` ``` define c where "c = prod_mset (image_mset fract_content ?P)" ``` eberlm@63498 ` 647` ``` define c' where "c' = c * to_fract (lead_coeff p)" ``` nipkow@63830 ` 648` ``` define e where "e = prod_mset (image_mset primitive_part_fract ?P)" ``` eberlm@63498 ` 649` ``` define A where "A = image_mset (normalize \ primitive_part_fract) ?P" ``` eberlm@63498 ` 650` ``` have "content e = (\x\#field_poly.prime_factorization (map_poly to_fract p). ``` eberlm@63498 ` 651` ``` content (primitive_part_fract x))" ``` nipkow@63830 ` 652` ``` by (simp add: e_def content_prod_mset multiset.map_comp o_def) ``` eberlm@63498 ` 653` ``` also have "image_mset (\x. content (primitive_part_fract x)) ?P = image_mset (\_. 1) ?P" ``` eberlm@63498 ` 654` ``` by (intro image_mset_cong content_primitive_part_fract) auto ``` haftmann@64591 ` 655` ``` finally have content_e: "content e = 1" ``` haftmann@64591 ` 656` ``` by simp ``` eberlm@63498 ` 657` ``` ``` haftmann@66805 ` 658` ``` from \p \ 0\ have "fract_poly p = [:lead_coeff (fract_poly p):] * ``` haftmann@66805 ` 659` ``` smult (inverse (lead_coeff (fract_poly p))) (fract_poly p)" ``` haftmann@66805 ` 660` ``` by simp ``` haftmann@66805 ` 661` ``` also have "[:lead_coeff (fract_poly p):] = [:to_fract (lead_coeff p):]" ``` haftmann@66805 ` 662` ``` by (simp add: monom_0 degree_map_poly coeff_map_poly) ``` haftmann@66805 ` 663` ``` also from assms have "smult (inverse (lead_coeff (fract_poly p))) (fract_poly p) = prod_mset ?P" ``` nipkow@63830 ` 664` ``` by (subst field_poly_prod_mset_prime_factorization) simp_all ``` nipkow@63830 ` 665` ``` also have "\ = prod_mset (image_mset id ?P)" by simp ``` eberlm@63498 ` 666` ``` also have "image_mset id ?P = ``` eberlm@63498 ` 667` ``` image_mset (\x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P" ``` eberlm@63498 ` 668` ``` by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract) ``` nipkow@63830 ` 669` ``` also have "prod_mset \ = smult c (fract_poly e)" ``` haftmann@64591 ` 670` ``` by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def) ``` eberlm@63498 ` 671` ``` also have "[:to_fract (lead_coeff p):] * \ = smult c' (fract_poly e)" ``` eberlm@63498 ` 672` ``` by (simp add: c'_def) ``` eberlm@63498 ` 673` ``` finally have eq: "fract_poly p = smult c' (fract_poly e)" . ``` eberlm@63498 ` 674` ``` also obtain b where b: "c' = to_fract b" "is_unit b" ``` eberlm@63498 ` 675` ``` proof - ``` eberlm@63498 ` 676` ``` from fract_poly_smult_eqE[OF eq] guess a b . note ab = this ``` eberlm@63498 ` 677` ``` from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: ) ``` eberlm@63498 ` 678` ``` with assms content_e have "a = normalize b" by (simp add: ab(4)) ``` eberlm@63498 ` 679` ``` with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff) ``` eberlm@63498 ` 680` ``` with ab ab' have "c' = to_fract b" by auto ``` eberlm@63498 ` 681` ``` from this and \is_unit b\ show ?thesis by (rule that) ``` eberlm@63498 ` 682` ``` qed ``` eberlm@63498 ` 683` ``` hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp ``` eberlm@63498 ` 684` ``` finally have "p = smult b e" by (simp only: fract_poly_eq_iff) ``` eberlm@63498 ` 685` ``` hence "p = [:b:] * e" by simp ``` eberlm@63498 ` 686` ``` with b have "normalize p = normalize e" ``` eberlm@63498 ` 687` ``` by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff) ``` nipkow@63830 ` 688` ``` also have "normalize e = prod_mset A" ``` nipkow@63830 ` 689` ``` by (simp add: multiset.map_comp e_def A_def normalize_prod_mset) ``` nipkow@63830 ` 690` ``` finally have "prod_mset A = normalize p" .. ``` eberlm@63498 ` 691` ``` ``` eberlm@63633 ` 692` ``` have "prime_elem p" if "p \# A" for p ``` eberlm@63633 ` 693` ``` using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible ``` eberlm@63498 ` 694` ``` dest!: field_poly_in_prime_factorization_imp_prime ) ``` nipkow@63830 ` 695` ``` from this and \prod_mset A = normalize p\ show ?thesis ``` eberlm@63498 ` 696` ``` by (intro exI[of _ A]) blast ``` eberlm@63498 ` 697` ```qed ``` eberlm@63498 ` 698` eberlm@63498 ` 699` ```lemma poly_prime_factorization_exists: ``` eberlm@63498 ` 700` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 701` ``` assumes "p \ 0" ``` nipkow@63830 ` 702` ``` shows "\A. (\p. p \# A \ prime_elem p) \ prod_mset A = normalize p" ``` eberlm@63498 ` 703` ```proof - ``` eberlm@63498 ` 704` ``` define B where "B = image_mset (\x. [:x:]) (prime_factorization (content p))" ``` nipkow@63830 ` 705` ``` have "\A. (\p. p \# A \ prime_elem p) \ prod_mset A = normalize (primitive_part p)" ``` eberlm@63498 ` 706` ``` by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all) ``` eberlm@63498 ` 707` ``` then guess A by (elim exE conjE) note A = this ``` nipkow@63830 ` 708` ``` moreover from assms have "prod_mset B = [:content p:]" ``` nipkow@63830 ` 709` ``` by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization) ``` eberlm@63633 ` 710` ``` moreover have "\p. p \# B \ prime_elem p" ``` haftmann@63905 ` 711` ``` by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime) ``` eberlm@63498 ` 712` ``` ultimately show ?thesis by (intro exI[of _ "B + A"]) auto ``` eberlm@63498 ` 713` ```qed ``` eberlm@63498 ` 714` eberlm@63498 ` 715` ```end ``` eberlm@63498 ` 716` eberlm@63498 ` 717` eberlm@63498 ` 718` ```subsection \Typeclass instances\ ``` eberlm@63498 ` 719` eberlm@63498 ` 720` ```instance poly :: (factorial_ring_gcd) factorial_semiring ``` eberlm@63498 ` 721` ``` by standard (rule poly_prime_factorization_exists) ``` eberlm@63498 ` 722` eberlm@63498 ` 723` ```instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd ``` eberlm@63498 ` 724` ```begin ``` eberlm@63498 ` 725` eberlm@63498 ` 726` ```definition gcd_poly :: "'a poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 727` ``` [code del]: "gcd_poly = gcd_factorial" ``` eberlm@63498 ` 728` eberlm@63498 ` 729` ```definition lcm_poly :: "'a poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 730` ``` [code del]: "lcm_poly = lcm_factorial" ``` eberlm@63498 ` 731` ``` ``` eberlm@63498 ` 732` ```definition Gcd_poly :: "'a poly set \ 'a poly" where ``` eberlm@63498 ` 733` ``` [code del]: "Gcd_poly = Gcd_factorial" ``` eberlm@63498 ` 734` eberlm@63498 ` 735` ```definition Lcm_poly :: "'a poly set \ 'a poly" where ``` eberlm@63498 ` 736` ``` [code del]: "Lcm_poly = Lcm_factorial" ``` eberlm@63498 ` 737` ``` ``` eberlm@63498 ` 738` ```instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) ``` eberlm@63498 ` 739` eberlm@63498 ` 740` ```end ``` eberlm@63498 ` 741` haftmann@66817 ` 742` ```instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}" ``` eberlm@63498 ` 743` ```begin ``` eberlm@63498 ` 744` haftmann@64784 ` 745` ```definition euclidean_size_poly :: "'a poly \ nat" ``` haftmann@64784 ` 746` ``` where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" ``` haftmann@64784 ` 747` haftmann@64784 ` 748` ```definition uniqueness_constraint_poly :: "'a poly \ 'a poly \ bool" ``` haftmann@64784 ` 749` ``` where [simp]: "uniqueness_constraint_poly = top" ``` eberlm@63498 ` 750` haftmann@66806 ` 751` ```instance proof ``` haftmann@66806 ` 752` ``` show "(q * p + r) div p = q" if "p \ 0" ``` haftmann@66806 ` 753` ``` and "euclidean_size r < euclidean_size p" for q p r :: "'a poly" ``` haftmann@66806 ` 754` ``` proof - ``` haftmann@66806 ` 755` ``` from \p \ 0\ eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)" ``` haftmann@66806 ` 756` ``` by (simp add: eucl_rel_poly_iff distrib_right) ``` haftmann@66806 ` 757` ``` then have "(r + q * p) div p = q + r div p" ``` haftmann@66806 ` 758` ``` by (rule div_poly_eq) ``` haftmann@66806 ` 759` ``` with that show ?thesis ``` haftmann@66806 ` 760` ``` by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps) ``` haftmann@66806 ` 761` ``` qed ``` haftmann@66806 ` 762` ```qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le ``` haftmann@64784 ` 763` ``` split: if_splits) ``` haftmann@64784 ` 764` eberlm@63498 ` 765` ```end ``` eberlm@63498 ` 766` haftmann@66817 ` 767` ```instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd ``` haftmann@66817 ` 768` ``` by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard ``` eberlm@63498 ` 769` eberlm@63498 ` 770` ``` ``` eberlm@63498 ` 771` ```subsection \Polynomial GCD\ ``` eberlm@63498 ` 772` eberlm@63498 ` 773` ```lemma gcd_poly_decompose: ``` eberlm@63498 ` 774` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 775` ``` shows "gcd p q = ``` eberlm@63498 ` 776` ``` smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" ``` eberlm@63498 ` 777` ```proof (rule sym, rule gcdI) ``` eberlm@63498 ` 778` ``` have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd ``` eberlm@63498 ` 779` ``` [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all ``` eberlm@63498 ` 780` ``` thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p" ``` eberlm@63498 ` 781` ``` by simp ``` eberlm@63498 ` 782` ```next ``` eberlm@63498 ` 783` ``` have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd ``` eberlm@63498 ` 784` ``` [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all ``` eberlm@63498 ` 785` ``` thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q" ``` eberlm@63498 ` 786` ``` by simp ``` eberlm@63498 ` 787` ```next ``` eberlm@63498 ` 788` ``` fix d assume "d dvd p" "d dvd q" ``` eberlm@63498 ` 789` ``` hence "[:content d:] * primitive_part d dvd ``` eberlm@63498 ` 790` ``` [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)" ``` eberlm@63498 ` 791` ``` by (intro mult_dvd_mono) auto ``` eberlm@63498 ` 792` ``` thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" ``` eberlm@63498 ` 793` ``` by simp ``` eberlm@63498 ` 794` ```qed (auto simp: normalize_smult) ``` eberlm@63498 ` 795` ``` ``` eberlm@63498 ` 796` eberlm@63498 ` 797` ```lemma gcd_poly_pseudo_mod: ``` eberlm@63498 ` 798` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 799` ``` assumes nz: "q \ 0" and prim: "content p = 1" "content q = 1" ``` eberlm@63498 ` 800` ``` shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 801` ```proof - ``` eberlm@63498 ` 802` ``` define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)" ``` eberlm@63498 ` 803` ``` define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]" ``` eberlm@63498 ` 804` ``` have [simp]: "primitive_part a = unit_factor a" ``` eberlm@63498 ` 805` ``` by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0) ``` eberlm@63498 ` 806` ``` from nz have [simp]: "a \ 0" by (auto simp: a_def) ``` eberlm@63498 ` 807` ``` ``` eberlm@63498 ` 808` ``` have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def) ``` eberlm@63498 ` 809` ``` have "gcd (q * r + s) q = gcd q s" ``` eberlm@63498 ` 810` ``` using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac) ``` eberlm@63498 ` 811` ``` with pseudo_divmod(1)[OF nz rs] ``` eberlm@63498 ` 812` ``` have "gcd (p * a) q = gcd q s" by (simp add: a_def) ``` eberlm@63498 ` 813` ``` also from prim have "gcd (p * a) q = gcd p q" ``` eberlm@63498 ` 814` ``` by (subst gcd_poly_decompose) ``` eberlm@63498 ` 815` ``` (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim ``` eberlm@63498 ` 816` ``` simp del: mult_pCons_right ) ``` eberlm@63498 ` 817` ``` also from prim have "gcd q s = gcd q (primitive_part s)" ``` eberlm@63498 ` 818` ``` by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim) ``` eberlm@63498 ` 819` ``` also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def) ``` eberlm@63498 ` 820` ``` finally show ?thesis . ``` eberlm@63498 ` 821` ```qed ``` eberlm@63498 ` 822` eberlm@63498 ` 823` ```lemma degree_pseudo_mod_less: ``` eberlm@63498 ` 824` ``` assumes "q \ 0" "pseudo_mod p q \ 0" ``` eberlm@63498 ` 825` ``` shows "degree (pseudo_mod p q) < degree q" ``` eberlm@63498 ` 826` ``` using pseudo_mod(2)[of q p] assms by auto ``` eberlm@63498 ` 827` eberlm@63498 ` 828` ```function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 829` ``` "gcd_poly_code_aux p q = ``` eberlm@63498 ` 830` ``` (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" ``` eberlm@63498 ` 831` ```by auto ``` eberlm@63498 ` 832` ```termination ``` eberlm@63498 ` 833` ``` by (relation "measure ((\p. if p = 0 then 0 else Suc (degree p)) \ snd)") ``` haftmann@64164 ` 834` ``` (auto simp: degree_pseudo_mod_less) ``` eberlm@63498 ` 835` eberlm@63498 ` 836` ```declare gcd_poly_code_aux.simps [simp del] ``` eberlm@63498 ` 837` eberlm@63498 ` 838` ```lemma gcd_poly_code_aux_correct: ``` eberlm@63498 ` 839` ``` assumes "content p = 1" "q = 0 \ content q = 1" ``` eberlm@63498 ` 840` ``` shows "gcd_poly_code_aux p q = gcd p q" ``` eberlm@63498 ` 841` ``` using assms ``` eberlm@63498 ` 842` ```proof (induction p q rule: gcd_poly_code_aux.induct) ``` eberlm@63498 ` 843` ``` case (1 p q) ``` eberlm@63498 ` 844` ``` show ?case ``` eberlm@63498 ` 845` ``` proof (cases "q = 0") ``` eberlm@63498 ` 846` ``` case True ``` eberlm@63498 ` 847` ``` thus ?thesis by (subst gcd_poly_code_aux.simps) auto ``` eberlm@63498 ` 848` ``` next ``` eberlm@63498 ` 849` ``` case False ``` eberlm@63498 ` 850` ``` hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 851` ``` by (subst gcd_poly_code_aux.simps) simp_all ``` eberlm@63498 ` 852` ``` also from "1.prems" False ``` eberlm@63498 ` 853` ``` have "primitive_part (pseudo_mod p q) = 0 \ ``` eberlm@63498 ` 854` ``` content (primitive_part (pseudo_mod p q)) = 1" ``` eberlm@63498 ` 855` ``` by (cases "pseudo_mod p q = 0") auto ``` eberlm@63498 ` 856` ``` with "1.prems" False ``` eberlm@63498 ` 857` ``` have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = ``` eberlm@63498 ` 858` ``` gcd q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 859` ``` by (intro 1) simp_all ``` eberlm@63498 ` 860` ``` also from "1.prems" False ``` eberlm@63498 ` 861` ``` have "\ = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto ``` eberlm@63498 ` 862` ``` finally show ?thesis . ``` eberlm@63498 ` 863` ``` qed ``` eberlm@63498 ` 864` ```qed ``` eberlm@63498 ` 865` eberlm@63498 ` 866` ```definition gcd_poly_code ``` eberlm@63498 ` 867` ``` :: "'a :: factorial_ring_gcd poly \ 'a poly \ 'a poly" ``` eberlm@63498 ` 868` ``` where "gcd_poly_code p q = ``` eberlm@63498 ` 869` ``` (if p = 0 then normalize q else if q = 0 then normalize p else ``` eberlm@63498 ` 870` ``` smult (gcd (content p) (content q)) ``` eberlm@63498 ` 871` ``` (gcd_poly_code_aux (primitive_part p) (primitive_part q)))" ``` eberlm@63498 ` 872` haftmann@64591 ` 873` ```lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q" ``` haftmann@64591 ` 874` ``` by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric]) ``` haftmann@64591 ` 875` eberlm@63498 ` 876` ```lemma lcm_poly_code [code]: ``` eberlm@63498 ` 877` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 878` ``` shows "lcm p q = normalize (p * q) div gcd p q" ``` haftmann@64591 ` 879` ``` by (fact lcm_gcd) ``` eberlm@63498 ` 880` haftmann@64850 ` 881` ```lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] ``` haftmann@64850 ` 882` ```lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] ``` haftmann@64860 ` 883` haftmann@64591 ` 884` ```text \Example: ``` haftmann@64591 ` 885` ``` @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} ``` haftmann@64591 ` 886` ```\ ``` eberlm@63498 ` 887` ``` ``` wenzelm@63764 ` 888` ```end ```