src/HOL/Library/Polynomial_Factorial.thy
 author eberlm Tue Aug 16 12:02:09 2016 +0200 (2016-08-16) changeset 63704 6209c06d776f parent 63633 src/HOL/Number_Theory/Polynomial_Factorial.thy@2accfb71e33b child 63705 7d371a18b6a2 permissions -rw-r--r--
Polynomial algebra cleanup
 eberlm@63498 ` 1` ```theory Polynomial_Factorial ``` eberlm@63498 ` 2` ```imports ``` eberlm@63498 ` 3` ``` Complex_Main ``` eberlm@63498 ` 4` ``` Euclidean_Algorithm ``` eberlm@63498 ` 5` ``` "~~/src/HOL/Library/Polynomial" ``` eberlm@63500 ` 6` ``` "~~/src/HOL/Library/Normalized_Fraction" ``` eberlm@63498 ` 7` ```begin ``` eberlm@63498 ` 8` eberlm@63498 ` 9` ```subsection \Prelude\ ``` eberlm@63498 ` 10` eberlm@63498 ` 11` ```lemma msetprod_mult: ``` eberlm@63498 ` 12` ``` "msetprod (image_mset (\x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)" ``` eberlm@63498 ` 13` ``` by (induction A) (simp_all add: mult_ac) ``` eberlm@63498 ` 14` ``` ``` eberlm@63498 ` 15` ```lemma msetprod_const: "msetprod (image_mset (\_. c) A) = c ^ size A" ``` eberlm@63498 ` 16` ``` by (induction A) (simp_all add: mult_ac) ``` eberlm@63498 ` 17` ``` ``` eberlm@63498 ` 18` ```lemma dvd_field_iff: "x dvd y \ (x = 0 \ y = (0::'a::field))" ``` eberlm@63498 ` 19` ```proof safe ``` eberlm@63498 ` 20` ``` assume "x \ 0" ``` eberlm@63498 ` 21` ``` hence "y = x * (y / x)" by (simp add: field_simps) ``` eberlm@63498 ` 22` ``` thus "x dvd y" by (rule dvdI) ``` eberlm@63498 ` 23` ```qed auto ``` eberlm@63498 ` 24` eberlm@63498 ` 25` ```lemma nat_descend_induct [case_names base descend]: ``` eberlm@63498 ` 26` ``` assumes "\k::nat. k > n \ P k" ``` eberlm@63498 ` 27` ``` assumes "\k::nat. k \ n \ (\i. i > k \ P i) \ P k" ``` eberlm@63498 ` 28` ``` shows "P m" ``` eberlm@63498 ` 29` ``` using assms by induction_schema (force intro!: wf_measure[of "\k. Suc n - k"])+ ``` eberlm@63498 ` 30` eberlm@63498 ` 31` ```lemma GreatestI_ex: "\k::nat. P k \ \y. P y \ y < b \ P (GREATEST x. P x)" ``` eberlm@63498 ` 32` ``` by (metis GreatestI) ``` eberlm@63498 ` 33` eberlm@63498 ` 34` eberlm@63498 ` 35` ```context field ``` eberlm@63498 ` 36` ```begin ``` eberlm@63498 ` 37` eberlm@63498 ` 38` ```subclass idom_divide .. ``` eberlm@63498 ` 39` eberlm@63498 ` 40` ```end ``` eberlm@63498 ` 41` eberlm@63498 ` 42` ```context field ``` eberlm@63498 ` 43` ```begin ``` eberlm@63498 ` 44` eberlm@63498 ` 45` ```definition normalize_field :: "'a \ 'a" ``` eberlm@63498 ` 46` ``` where [simp]: "normalize_field x = (if x = 0 then 0 else 1)" ``` eberlm@63498 ` 47` ```definition unit_factor_field :: "'a \ 'a" ``` eberlm@63498 ` 48` ``` where [simp]: "unit_factor_field x = x" ``` eberlm@63498 ` 49` ```definition euclidean_size_field :: "'a \ nat" ``` eberlm@63498 ` 50` ``` where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)" ``` eberlm@63498 ` 51` ```definition mod_field :: "'a \ 'a \ 'a" ``` eberlm@63498 ` 52` ``` where [simp]: "mod_field x y = (if y = 0 then x else 0)" ``` eberlm@63498 ` 53` eberlm@63498 ` 54` ```end ``` eberlm@63498 ` 55` eberlm@63498 ` 56` ```instantiation real :: euclidean_ring ``` eberlm@63498 ` 57` ```begin ``` eberlm@63498 ` 58` eberlm@63498 ` 59` ```definition [simp]: "normalize_real = (normalize_field :: real \ _)" ``` eberlm@63498 ` 60` ```definition [simp]: "unit_factor_real = (unit_factor_field :: real \ _)" ``` eberlm@63498 ` 61` ```definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \ _)" ``` eberlm@63498 ` 62` ```definition [simp]: "mod_real = (mod_field :: real \ _)" ``` eberlm@63498 ` 63` eberlm@63498 ` 64` ```instance by standard (simp_all add: dvd_field_iff divide_simps) ``` eberlm@63498 ` 65` ```end ``` eberlm@63498 ` 66` eberlm@63498 ` 67` ```instantiation real :: euclidean_ring_gcd ``` eberlm@63498 ` 68` ```begin ``` eberlm@63498 ` 69` eberlm@63498 ` 70` ```definition gcd_real :: "real \ real \ real" where ``` eberlm@63498 ` 71` ``` "gcd_real = gcd_eucl" ``` eberlm@63498 ` 72` ```definition lcm_real :: "real \ real \ real" where ``` eberlm@63498 ` 73` ``` "lcm_real = lcm_eucl" ``` eberlm@63498 ` 74` ```definition Gcd_real :: "real set \ real" where ``` eberlm@63498 ` 75` ``` "Gcd_real = Gcd_eucl" ``` eberlm@63498 ` 76` ```definition Lcm_real :: "real set \ real" where ``` eberlm@63498 ` 77` ``` "Lcm_real = Lcm_eucl" ``` eberlm@63498 ` 78` eberlm@63498 ` 79` ```instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def) ``` eberlm@63498 ` 80` eberlm@63498 ` 81` ```end ``` eberlm@63498 ` 82` eberlm@63498 ` 83` ```instantiation rat :: euclidean_ring ``` eberlm@63498 ` 84` ```begin ``` eberlm@63498 ` 85` eberlm@63498 ` 86` ```definition [simp]: "normalize_rat = (normalize_field :: rat \ _)" ``` eberlm@63498 ` 87` ```definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \ _)" ``` eberlm@63498 ` 88` ```definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \ _)" ``` eberlm@63498 ` 89` ```definition [simp]: "mod_rat = (mod_field :: rat \ _)" ``` eberlm@63498 ` 90` eberlm@63498 ` 91` ```instance by standard (simp_all add: dvd_field_iff divide_simps) ``` eberlm@63498 ` 92` ```end ``` eberlm@63498 ` 93` eberlm@63498 ` 94` ```instantiation rat :: euclidean_ring_gcd ``` eberlm@63498 ` 95` ```begin ``` eberlm@63498 ` 96` eberlm@63498 ` 97` ```definition gcd_rat :: "rat \ rat \ rat" where ``` eberlm@63498 ` 98` ``` "gcd_rat = gcd_eucl" ``` eberlm@63498 ` 99` ```definition lcm_rat :: "rat \ rat \ rat" where ``` eberlm@63498 ` 100` ``` "lcm_rat = lcm_eucl" ``` eberlm@63498 ` 101` ```definition Gcd_rat :: "rat set \ rat" where ``` eberlm@63498 ` 102` ``` "Gcd_rat = Gcd_eucl" ``` eberlm@63498 ` 103` ```definition Lcm_rat :: "rat set \ rat" where ``` eberlm@63498 ` 104` ``` "Lcm_rat = Lcm_eucl" ``` eberlm@63498 ` 105` eberlm@63498 ` 106` ```instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def) ``` eberlm@63498 ` 107` eberlm@63498 ` 108` ```end ``` eberlm@63498 ` 109` eberlm@63498 ` 110` ```instantiation complex :: euclidean_ring ``` eberlm@63498 ` 111` ```begin ``` eberlm@63498 ` 112` eberlm@63498 ` 113` ```definition [simp]: "normalize_complex = (normalize_field :: complex \ _)" ``` eberlm@63498 ` 114` ```definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \ _)" ``` eberlm@63498 ` 115` ```definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \ _)" ``` eberlm@63498 ` 116` ```definition [simp]: "mod_complex = (mod_field :: complex \ _)" ``` eberlm@63498 ` 117` eberlm@63498 ` 118` ```instance by standard (simp_all add: dvd_field_iff divide_simps) ``` eberlm@63498 ` 119` ```end ``` eberlm@63498 ` 120` eberlm@63498 ` 121` ```instantiation complex :: euclidean_ring_gcd ``` eberlm@63498 ` 122` ```begin ``` eberlm@63498 ` 123` eberlm@63498 ` 124` ```definition gcd_complex :: "complex \ complex \ complex" where ``` eberlm@63498 ` 125` ``` "gcd_complex = gcd_eucl" ``` eberlm@63498 ` 126` ```definition lcm_complex :: "complex \ complex \ complex" where ``` eberlm@63498 ` 127` ``` "lcm_complex = lcm_eucl" ``` eberlm@63498 ` 128` ```definition Gcd_complex :: "complex set \ complex" where ``` eberlm@63498 ` 129` ``` "Gcd_complex = Gcd_eucl" ``` eberlm@63498 ` 130` ```definition Lcm_complex :: "complex set \ complex" where ``` eberlm@63498 ` 131` ``` "Lcm_complex = Lcm_eucl" ``` eberlm@63498 ` 132` eberlm@63498 ` 133` ```instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def) ``` eberlm@63498 ` 134` eberlm@63498 ` 135` ```end ``` eberlm@63498 ` 136` eberlm@63498 ` 137` eberlm@63498 ` 138` eberlm@63498 ` 139` ```subsection \Lifting elements into the field of fractions\ ``` eberlm@63498 ` 140` eberlm@63498 ` 141` ```definition to_fract :: "'a :: idom \ 'a fract" where "to_fract x = Fract x 1" ``` eberlm@63498 ` 142` eberlm@63498 ` 143` ```lemma to_fract_0 [simp]: "to_fract 0 = 0" ``` eberlm@63498 ` 144` ``` by (simp add: to_fract_def eq_fract Zero_fract_def) ``` eberlm@63498 ` 145` eberlm@63498 ` 146` ```lemma to_fract_1 [simp]: "to_fract 1 = 1" ``` eberlm@63498 ` 147` ``` by (simp add: to_fract_def eq_fract One_fract_def) ``` eberlm@63498 ` 148` eberlm@63498 ` 149` ```lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y" ``` eberlm@63498 ` 150` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 151` eberlm@63498 ` 152` ```lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y" ``` eberlm@63498 ` 153` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 154` ``` ``` eberlm@63498 ` 155` ```lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x" ``` eberlm@63498 ` 156` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 157` ``` ``` eberlm@63498 ` 158` ```lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y" ``` eberlm@63498 ` 159` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 160` eberlm@63498 ` 161` ```lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \ x = y" ``` eberlm@63498 ` 162` ``` by (simp add: to_fract_def eq_fract) ``` eberlm@63498 ` 163` ``` ``` eberlm@63498 ` 164` ```lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \ x = 0" ``` eberlm@63498 ` 165` ``` by (simp add: to_fract_def Zero_fract_def eq_fract) ``` eberlm@63498 ` 166` eberlm@63498 ` 167` ```lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \ 0" ``` eberlm@63498 ` 168` ``` by transfer simp ``` eberlm@63498 ` 169` eberlm@63498 ` 170` ```lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x" ``` eberlm@63498 ` 171` ``` by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp) ``` eberlm@63498 ` 172` eberlm@63498 ` 173` ```lemma to_fract_quot_of_fract: ``` eberlm@63498 ` 174` ``` assumes "snd (quot_of_fract x) = 1" ``` eberlm@63498 ` 175` ``` shows "to_fract (fst (quot_of_fract x)) = x" ``` eberlm@63498 ` 176` ```proof - ``` eberlm@63498 ` 177` ``` have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp ``` eberlm@63498 ` 178` ``` also note assms ``` eberlm@63498 ` 179` ``` finally show ?thesis by (simp add: to_fract_def) ``` eberlm@63498 ` 180` ```qed ``` eberlm@63498 ` 181` eberlm@63498 ` 182` ```lemma snd_quot_of_fract_Fract_whole: ``` eberlm@63498 ` 183` ``` assumes "y dvd x" ``` eberlm@63498 ` 184` ``` shows "snd (quot_of_fract (Fract x y)) = 1" ``` eberlm@63498 ` 185` ``` using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd) ``` eberlm@63498 ` 186` ``` ``` eberlm@63498 ` 187` ```lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b" ``` eberlm@63498 ` 188` ``` by (simp add: to_fract_def) ``` eberlm@63498 ` 189` eberlm@63498 ` 190` ```lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)" ``` eberlm@63498 ` 191` ``` unfolding to_fract_def by transfer (simp add: normalize_quot_def) ``` eberlm@63498 ` 192` eberlm@63498 ` 193` ```lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \ x = 0" ``` eberlm@63498 ` 194` ``` by transfer simp ``` eberlm@63498 ` 195` ``` ``` eberlm@63498 ` 196` ```lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1" ``` eberlm@63498 ` 197` ``` unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all ``` eberlm@63498 ` 198` eberlm@63498 ` 199` ```lemma coprime_quot_of_fract: ``` eberlm@63498 ` 200` ``` "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))" ``` eberlm@63498 ` 201` ``` by transfer (simp add: coprime_normalize_quot) ``` eberlm@63498 ` 202` eberlm@63498 ` 203` ```lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1" ``` eberlm@63498 ` 204` ``` using quot_of_fract_in_normalized_fracts[of x] ``` eberlm@63498 ` 205` ``` by (simp add: normalized_fracts_def case_prod_unfold) ``` eberlm@63498 ` 206` eberlm@63498 ` 207` ```lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \ normalize x = x" ``` eberlm@63498 ` 208` ``` by (subst (2) normalize_mult_unit_factor [symmetric, of x]) ``` eberlm@63498 ` 209` ``` (simp del: normalize_mult_unit_factor) ``` eberlm@63498 ` 210` ``` ``` eberlm@63498 ` 211` ```lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)" ``` eberlm@63498 ` 212` ``` by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract) ``` eberlm@63498 ` 213` eberlm@63498 ` 214` ``` ``` eberlm@63498 ` 215` ```subsection \Mapping polynomials\ ``` eberlm@63498 ` 216` eberlm@63498 ` 217` ```definition map_poly ``` eberlm@63498 ` 218` ``` :: "('a :: comm_semiring_0 \ 'b :: comm_semiring_0) \ 'a poly \ 'b poly" where ``` eberlm@63498 ` 219` ``` "map_poly f p = Poly (map f (coeffs p))" ``` eberlm@63498 ` 220` eberlm@63498 ` 221` ```lemma map_poly_0 [simp]: "map_poly f 0 = 0" ``` eberlm@63498 ` 222` ``` by (simp add: map_poly_def) ``` eberlm@63498 ` 223` eberlm@63498 ` 224` ```lemma map_poly_1: "map_poly f 1 = [:f 1:]" ``` eberlm@63498 ` 225` ``` by (simp add: map_poly_def) ``` eberlm@63498 ` 226` eberlm@63498 ` 227` ```lemma map_poly_1' [simp]: "f 1 = 1 \ map_poly f 1 = 1" ``` eberlm@63498 ` 228` ``` by (simp add: map_poly_def one_poly_def) ``` eberlm@63498 ` 229` eberlm@63498 ` 230` ```lemma coeff_map_poly: ``` eberlm@63498 ` 231` ``` assumes "f 0 = 0" ``` eberlm@63498 ` 232` ``` shows "coeff (map_poly f p) n = f (coeff p n)" ``` eberlm@63498 ` 233` ``` by (auto simp: map_poly_def nth_default_def coeffs_def assms ``` eberlm@63498 ` 234` ``` not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc) ``` eberlm@63498 ` 235` eberlm@63498 ` 236` ```lemma coeffs_map_poly [code abstract]: ``` eberlm@63498 ` 237` ``` "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" ``` eberlm@63498 ` 238` ``` by (simp add: map_poly_def) ``` eberlm@63498 ` 239` eberlm@63498 ` 240` ```lemma set_coeffs_map_poly: ``` eberlm@63498 ` 241` ``` "(\x. f x = 0 \ x = 0) \ set (coeffs (map_poly f p)) = f ` set (coeffs p)" ``` eberlm@63498 ` 242` ``` by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0) ``` eberlm@63498 ` 243` eberlm@63498 ` 244` ```lemma coeffs_map_poly': ``` eberlm@63498 ` 245` ``` assumes "(\x. x \ 0 \ f x \ 0)" ``` eberlm@63498 ` 246` ``` shows "coeffs (map_poly f p) = map f (coeffs p)" ``` eberlm@63498 ` 247` ``` by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms ``` eberlm@63498 ` 248` ``` intro!: strip_while_not_last split: if_splits) ``` eberlm@63498 ` 249` eberlm@63498 ` 250` ```lemma degree_map_poly: ``` eberlm@63498 ` 251` ``` assumes "\x. x \ 0 \ f x \ 0" ``` eberlm@63498 ` 252` ``` shows "degree (map_poly f p) = degree p" ``` eberlm@63498 ` 253` ``` by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms) ``` eberlm@63498 ` 254` eberlm@63498 ` 255` ```lemma map_poly_eq_0_iff: ``` eberlm@63498 ` 256` ``` assumes "f 0 = 0" "\x. x \ set (coeffs p) \ x \ 0 \ f x \ 0" ``` eberlm@63498 ` 257` ``` shows "map_poly f p = 0 \ p = 0" ``` eberlm@63498 ` 258` ```proof - ``` eberlm@63498 ` 259` ``` { ``` eberlm@63498 ` 260` ``` fix n :: nat ``` eberlm@63498 ` 261` ``` have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms) ``` eberlm@63498 ` 262` ``` also have "\ = 0 \ coeff p n = 0" ``` eberlm@63498 ` 263` ``` proof (cases "n < length (coeffs p)") ``` eberlm@63498 ` 264` ``` case True ``` eberlm@63498 ` 265` ``` hence "coeff p n \ set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc) ``` eberlm@63498 ` 266` ``` with assms show "f (coeff p n) = 0 \ coeff p n = 0" by auto ``` eberlm@63498 ` 267` ``` qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) ``` eberlm@63498 ` 268` ``` finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" . ``` eberlm@63498 ` 269` ``` } ``` eberlm@63498 ` 270` ``` thus ?thesis by (auto simp: poly_eq_iff) ``` eberlm@63498 ` 271` ```qed ``` eberlm@63498 ` 272` eberlm@63498 ` 273` ```lemma map_poly_smult: ``` eberlm@63498 ` 274` ``` assumes "f 0 = 0""\c x. f (c * x) = f c * f x" ``` eberlm@63498 ` 275` ``` shows "map_poly f (smult c p) = smult (f c) (map_poly f p)" ``` eberlm@63498 ` 276` ``` by (intro poly_eqI) (simp_all add: assms coeff_map_poly) ``` eberlm@63498 ` 277` eberlm@63498 ` 278` ```lemma map_poly_pCons: ``` eberlm@63498 ` 279` ``` assumes "f 0 = 0" ``` eberlm@63498 ` 280` ``` shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" ``` eberlm@63498 ` 281` ``` by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits) ``` eberlm@63498 ` 282` eberlm@63498 ` 283` ```lemma map_poly_map_poly: ``` eberlm@63498 ` 284` ``` assumes "f 0 = 0" "g 0 = 0" ``` eberlm@63498 ` 285` ``` shows "map_poly f (map_poly g p) = map_poly (f \ g) p" ``` eberlm@63498 ` 286` ``` by (intro poly_eqI) (simp add: coeff_map_poly assms) ``` eberlm@63498 ` 287` eberlm@63498 ` 288` ```lemma map_poly_id [simp]: "map_poly id p = p" ``` eberlm@63498 ` 289` ``` by (simp add: map_poly_def) ``` eberlm@63498 ` 290` eberlm@63498 ` 291` ```lemma map_poly_id' [simp]: "map_poly (\x. x) p = p" ``` eberlm@63498 ` 292` ``` by (simp add: map_poly_def) ``` eberlm@63498 ` 293` eberlm@63498 ` 294` ```lemma map_poly_cong: ``` eberlm@63498 ` 295` ``` assumes "(\x. x \ set (coeffs p) \ f x = g x)" ``` eberlm@63498 ` 296` ``` shows "map_poly f p = map_poly g p" ``` eberlm@63498 ` 297` ```proof - ``` eberlm@63498 ` 298` ``` from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all ``` eberlm@63498 ` 299` ``` thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly) ``` eberlm@63498 ` 300` ```qed ``` eberlm@63498 ` 301` eberlm@63498 ` 302` ```lemma map_poly_monom: "f 0 = 0 \ map_poly f (monom c n) = monom (f c) n" ``` eberlm@63498 ` 303` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 304` eberlm@63498 ` 305` ```lemma map_poly_idI: ``` eberlm@63498 ` 306` ``` assumes "\x. x \ set (coeffs p) \ f x = x" ``` eberlm@63498 ` 307` ``` shows "map_poly f p = p" ``` eberlm@63498 ` 308` ``` using map_poly_cong[OF assms, of _ id] by simp ``` eberlm@63498 ` 309` eberlm@63498 ` 310` ```lemma map_poly_idI': ``` eberlm@63498 ` 311` ``` assumes "\x. x \ set (coeffs p) \ f x = x" ``` eberlm@63498 ` 312` ``` shows "p = map_poly f p" ``` eberlm@63498 ` 313` ``` using map_poly_cong[OF assms, of _ id] by simp ``` eberlm@63498 ` 314` eberlm@63498 ` 315` ```lemma smult_conv_map_poly: "smult c p = map_poly (\x. c * x) p" ``` eberlm@63498 ` 316` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 317` eberlm@63498 ` 318` ```lemma div_const_poly_conv_map_poly: ``` eberlm@63498 ` 319` ``` assumes "[:c:] dvd p" ``` eberlm@63498 ` 320` ``` shows "p div [:c:] = map_poly (\x. x div c) p" ``` eberlm@63498 ` 321` ```proof (cases "c = 0") ``` eberlm@63498 ` 322` ``` case False ``` eberlm@63498 ` 323` ``` from assms obtain q where p: "p = [:c:] * q" by (erule dvdE) ``` eberlm@63498 ` 324` ``` moreover { ``` eberlm@63498 ` 325` ``` have "smult c q = [:c:] * q" by simp ``` eberlm@63498 ` 326` ``` also have "\ div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto) ``` eberlm@63498 ` 327` ``` finally have "smult c q div [:c:] = q" . ``` eberlm@63498 ` 328` ``` } ``` eberlm@63498 ` 329` ``` ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False) ``` eberlm@63498 ` 330` ```qed (auto intro!: poly_eqI simp: coeff_map_poly) ``` eberlm@63498 ` 331` eberlm@63498 ` 332` eberlm@63498 ` 333` eberlm@63498 ` 334` ```subsection \Various facts about polynomials\ ``` eberlm@63498 ` 335` eberlm@63498 ` 336` ```lemma msetprod_const_poly: "msetprod (image_mset (\x. [:f x:]) A) = [:msetprod (image_mset f A):]" ``` eberlm@63498 ` 337` ``` by (induction A) (simp_all add: one_poly_def mult_ac) ``` eberlm@63498 ` 338` eberlm@63498 ` 339` ```lemma degree_mod_less': "b \ 0 \ a mod b \ 0 \ degree (a mod b) < degree b" ``` eberlm@63498 ` 340` ``` using degree_mod_less[of b a] by auto ``` eberlm@63498 ` 341` ``` ``` eberlm@63498 ` 342` ```lemma is_unit_const_poly_iff: ``` eberlm@63498 ` 343` ``` "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \ c dvd 1" ``` eberlm@63498 ` 344` ``` by (auto simp: one_poly_def) ``` eberlm@63498 ` 345` eberlm@63498 ` 346` ```lemma is_unit_poly_iff: ``` eberlm@63498 ` 347` ``` fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" ``` eberlm@63498 ` 348` ``` shows "p dvd 1 \ (\c. p = [:c:] \ c dvd 1)" ``` eberlm@63498 ` 349` ```proof safe ``` eberlm@63498 ` 350` ``` assume "p dvd 1" ``` eberlm@63498 ` 351` ``` then obtain q where pq: "1 = p * q" by (erule dvdE) ``` eberlm@63498 ` 352` ``` hence "degree 1 = degree (p * q)" by simp ``` eberlm@63498 ` 353` ``` also from pq have "\ = degree p + degree q" by (intro degree_mult_eq) auto ``` eberlm@63498 ` 354` ``` finally have "degree p = 0" by simp ``` eberlm@63498 ` 355` ``` from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" . ``` eberlm@63498 ` 356` ``` with \p dvd 1\ show "\c. p = [:c:] \ c dvd 1" ``` eberlm@63498 ` 357` ``` by (auto simp: is_unit_const_poly_iff) ``` eberlm@63498 ` 358` ```qed (auto simp: is_unit_const_poly_iff) ``` eberlm@63498 ` 359` eberlm@63498 ` 360` ```lemma is_unit_polyE: ``` eberlm@63498 ` 361` ``` fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" ``` eberlm@63498 ` 362` ``` assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1" ``` eberlm@63498 ` 363` ``` using assms by (subst (asm) is_unit_poly_iff) blast ``` eberlm@63498 ` 364` eberlm@63498 ` 365` ```lemma smult_eq_iff: ``` eberlm@63498 ` 366` ``` assumes "(b :: 'a :: field) \ 0" ``` eberlm@63498 ` 367` ``` shows "smult a p = smult b q \ smult (a / b) p = q" ``` eberlm@63498 ` 368` ```proof ``` eberlm@63498 ` 369` ``` assume "smult a p = smult b q" ``` eberlm@63498 ` 370` ``` also from assms have "smult (inverse b) \ = q" by simp ``` eberlm@63498 ` 371` ``` finally show "smult (a / b) p = q" by (simp add: field_simps) ``` eberlm@63498 ` 372` ```qed (insert assms, auto) ``` eberlm@63498 ` 373` eberlm@63498 ` 374` ```lemma irreducible_const_poly_iff: ``` eberlm@63498 ` 375` ``` fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" ``` eberlm@63498 ` 376` ``` shows "irreducible [:c:] \ irreducible c" ``` eberlm@63498 ` 377` ```proof ``` eberlm@63498 ` 378` ``` assume A: "irreducible c" ``` eberlm@63498 ` 379` ``` show "irreducible [:c:]" ``` eberlm@63498 ` 380` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 381` ``` fix a b assume ab: "[:c:] = a * b" ``` eberlm@63498 ` 382` ``` hence "degree [:c:] = degree (a * b)" by (simp only: ) ``` eberlm@63498 ` 383` ``` also from A ab have "a \ 0" "b \ 0" by auto ``` eberlm@63498 ` 384` ``` hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq) ``` eberlm@63498 ` 385` ``` finally have "degree a = 0" "degree b = 0" by auto ``` eberlm@63498 ` 386` ``` then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE) ``` eberlm@63498 ` 387` ``` from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: ) ``` eberlm@63498 ` 388` ``` hence "c = a' * b'" by (simp add: ab' mult_ac) ``` eberlm@63498 ` 389` ``` from A and this have "a' dvd 1 \ b' dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 390` ``` with ab' show "a dvd 1 \ b dvd 1" by (auto simp: one_poly_def) ``` eberlm@63498 ` 391` ``` qed (insert A, auto simp: irreducible_def is_unit_poly_iff) ``` eberlm@63498 ` 392` ```next ``` eberlm@63498 ` 393` ``` assume A: "irreducible [:c:]" ``` eberlm@63498 ` 394` ``` show "irreducible c" ``` eberlm@63498 ` 395` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 396` ``` fix a b assume ab: "c = a * b" ``` eberlm@63498 ` 397` ``` hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac) ``` eberlm@63498 ` 398` ``` from A and this have "[:a:] dvd 1 \ [:b:] dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 399` ``` thus "a dvd 1 \ b dvd 1" by (simp add: one_poly_def) ``` eberlm@63498 ` 400` ``` qed (insert A, auto simp: irreducible_def one_poly_def) ``` eberlm@63498 ` 401` ```qed ``` eberlm@63498 ` 402` eberlm@63498 ` 403` ```lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c" ``` eberlm@63498 ` 404` ``` by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq) ``` eberlm@63498 ` 405` eberlm@63498 ` 406` ``` ``` eberlm@63498 ` 407` ```subsection \Normalisation of polynomials\ ``` eberlm@63498 ` 408` eberlm@63498 ` 409` ```instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom ``` eberlm@63498 ` 410` ```begin ``` eberlm@63498 ` 411` eberlm@63498 ` 412` ```definition unit_factor_poly :: "'a poly \ 'a poly" ``` eberlm@63498 ` 413` ``` where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0" ``` eberlm@63498 ` 414` eberlm@63498 ` 415` ```definition normalize_poly :: "'a poly \ 'a poly" ``` eberlm@63498 ` 416` ``` where "normalize_poly p = map_poly (\x. x div unit_factor (lead_coeff p)) p" ``` eberlm@63498 ` 417` eberlm@63498 ` 418` ```lemma normalize_poly_altdef: ``` eberlm@63498 ` 419` ``` "normalize p = p div [:unit_factor (lead_coeff p):]" ``` eberlm@63498 ` 420` ```proof (cases "p = 0") ``` eberlm@63498 ` 421` ``` case False ``` eberlm@63498 ` 422` ``` thus ?thesis ``` eberlm@63498 ` 423` ``` by (subst div_const_poly_conv_map_poly) ``` eberlm@63498 ` 424` ``` (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def ) ``` eberlm@63498 ` 425` ```qed (auto simp: normalize_poly_def) ``` eberlm@63498 ` 426` eberlm@63498 ` 427` ```instance ``` eberlm@63498 ` 428` ```proof ``` eberlm@63498 ` 429` ``` fix p :: "'a poly" ``` eberlm@63498 ` 430` ``` show "unit_factor p * normalize p = p" ``` eberlm@63498 ` 431` ``` by (cases "p = 0") ``` eberlm@63498 ` 432` ``` (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 ``` eberlm@63498 ` 433` ``` smult_conv_map_poly map_poly_map_poly o_def) ``` eberlm@63498 ` 434` ```next ``` eberlm@63498 ` 435` ``` fix p :: "'a poly" ``` eberlm@63498 ` 436` ``` assume "is_unit p" ``` eberlm@63498 ` 437` ``` then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 438` ``` thus "normalize p = 1" ``` eberlm@63498 ` 439` ``` by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def) ``` eberlm@63498 ` 440` ```next ``` eberlm@63498 ` 441` ``` fix p :: "'a poly" assume "p \ 0" ``` eberlm@63498 ` 442` ``` thus "is_unit (unit_factor p)" ``` eberlm@63498 ` 443` ``` by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff) ``` eberlm@63498 ` 444` ```qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult) ``` eberlm@63498 ` 445` eberlm@63498 ` 446` ```end ``` eberlm@63498 ` 447` eberlm@63498 ` 448` ```lemma unit_factor_pCons: ``` eberlm@63498 ` 449` ``` "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)" ``` eberlm@63498 ` 450` ``` by (simp add: unit_factor_poly_def) ``` eberlm@63498 ` 451` eberlm@63498 ` 452` ```lemma normalize_monom [simp]: ``` eberlm@63498 ` 453` ``` "normalize (monom a n) = monom (normalize a) n" ``` eberlm@63498 ` 454` ``` by (simp add: map_poly_monom normalize_poly_def) ``` eberlm@63498 ` 455` eberlm@63498 ` 456` ```lemma unit_factor_monom [simp]: ``` eberlm@63498 ` 457` ``` "unit_factor (monom a n) = monom (unit_factor a) 0" ``` eberlm@63498 ` 458` ``` by (simp add: unit_factor_poly_def ) ``` eberlm@63498 ` 459` eberlm@63498 ` 460` ```lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]" ``` eberlm@63498 ` 461` ``` by (simp add: normalize_poly_def map_poly_pCons) ``` eberlm@63498 ` 462` eberlm@63498 ` 463` ```lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)" ``` eberlm@63498 ` 464` ```proof - ``` eberlm@63498 ` 465` ``` have "smult c p = [:c:] * p" by simp ``` eberlm@63498 ` 466` ``` also have "normalize \ = smult (normalize c) (normalize p)" ``` eberlm@63498 ` 467` ``` by (subst normalize_mult) (simp add: normalize_const_poly) ``` eberlm@63498 ` 468` ``` finally show ?thesis . ``` eberlm@63498 ` 469` ```qed ``` eberlm@63498 ` 470` eberlm@63498 ` 471` ```lemma is_unit_smult_iff: "smult c p dvd 1 \ c dvd 1 \ p dvd 1" ``` eberlm@63498 ` 472` ```proof - ``` eberlm@63498 ` 473` ``` have "smult c p = [:c:] * p" by simp ``` eberlm@63498 ` 474` ``` also have "\ dvd 1 \ c dvd 1 \ p dvd 1" ``` eberlm@63498 ` 475` ``` proof safe ``` eberlm@63498 ` 476` ``` assume A: "[:c:] * p dvd 1" ``` eberlm@63498 ` 477` ``` thus "p dvd 1" by (rule dvd_mult_right) ``` eberlm@63498 ` 478` ``` from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE) ``` eberlm@63498 ` 479` ``` have "c dvd c * (coeff p 0 * coeff q 0)" by simp ``` eberlm@63498 ` 480` ``` also have "\ = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult) ``` eberlm@63498 ` 481` ``` also note B [symmetric] ``` eberlm@63498 ` 482` ``` finally show "c dvd 1" by simp ``` eberlm@63498 ` 483` ``` next ``` eberlm@63498 ` 484` ``` assume "c dvd 1" "p dvd 1" ``` eberlm@63498 ` 485` ``` from \c dvd 1\ obtain d where "1 = c * d" by (erule dvdE) ``` eberlm@63498 ` 486` ``` hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac) ``` eberlm@63498 ` 487` ``` hence "[:c:] dvd 1" by (rule dvdI) ``` eberlm@63498 ` 488` ``` from mult_dvd_mono[OF this \p dvd 1\] show "[:c:] * p dvd 1" by simp ``` eberlm@63498 ` 489` ``` qed ``` eberlm@63498 ` 490` ``` finally show ?thesis . ``` eberlm@63498 ` 491` ```qed ``` eberlm@63498 ` 492` eberlm@63498 ` 493` eberlm@63498 ` 494` ```subsection \Content and primitive part of a polynomial\ ``` eberlm@63498 ` 495` eberlm@63498 ` 496` ```definition content :: "('a :: semiring_Gcd poly) \ 'a" where ``` eberlm@63498 ` 497` ``` "content p = Gcd (set (coeffs p))" ``` eberlm@63498 ` 498` eberlm@63498 ` 499` ```lemma content_0 [simp]: "content 0 = 0" ``` eberlm@63498 ` 500` ``` by (simp add: content_def) ``` eberlm@63498 ` 501` eberlm@63498 ` 502` ```lemma content_1 [simp]: "content 1 = 1" ``` eberlm@63498 ` 503` ``` by (simp add: content_def) ``` eberlm@63498 ` 504` eberlm@63498 ` 505` ```lemma content_const [simp]: "content [:c:] = normalize c" ``` eberlm@63498 ` 506` ``` by (simp add: content_def cCons_def) ``` eberlm@63498 ` 507` eberlm@63498 ` 508` ```lemma const_poly_dvd_iff_dvd_content: ``` eberlm@63498 ` 509` ``` fixes c :: "'a :: semiring_Gcd" ``` eberlm@63498 ` 510` ``` shows "[:c:] dvd p \ c dvd content p" ``` eberlm@63498 ` 511` ```proof (cases "p = 0") ``` eberlm@63498 ` 512` ``` case [simp]: False ``` eberlm@63498 ` 513` ``` have "[:c:] dvd p \ (\n. c dvd coeff p n)" by (rule const_poly_dvd_iff) ``` eberlm@63498 ` 514` ``` also have "\ \ (\a\set (coeffs p). c dvd a)" ``` eberlm@63498 ` 515` ``` proof safe ``` eberlm@63498 ` 516` ``` fix n :: nat assume "\a\set (coeffs p). c dvd a" ``` eberlm@63498 ` 517` ``` thus "c dvd coeff p n" ``` eberlm@63498 ` 518` ``` by (cases "n \ degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits) ``` eberlm@63498 ` 519` ``` qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits) ``` eberlm@63498 ` 520` ``` also have "\ \ c dvd content p" ``` eberlm@63498 ` 521` ``` by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x] ``` eberlm@63498 ` 522` ``` dvd_mult_unit_iff lead_coeff_nonzero) ``` eberlm@63498 ` 523` ``` finally show ?thesis . ``` eberlm@63498 ` 524` ```qed simp_all ``` eberlm@63498 ` 525` eberlm@63498 ` 526` ```lemma content_dvd [simp]: "[:content p:] dvd p" ``` eberlm@63498 ` 527` ``` by (subst const_poly_dvd_iff_dvd_content) simp_all ``` eberlm@63498 ` 528` ``` ``` eberlm@63498 ` 529` ```lemma content_dvd_coeff [simp]: "content p dvd coeff p n" ``` eberlm@63498 ` 530` ``` by (cases "n \ degree p") ``` eberlm@63498 ` 531` ``` (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd) ``` eberlm@63498 ` 532` eberlm@63498 ` 533` ```lemma content_dvd_coeffs: "c \ set (coeffs p) \ content p dvd c" ``` eberlm@63498 ` 534` ``` by (simp add: content_def Gcd_dvd) ``` eberlm@63498 ` 535` eberlm@63498 ` 536` ```lemma normalize_content [simp]: "normalize (content p) = content p" ``` eberlm@63498 ` 537` ``` by (simp add: content_def) ``` eberlm@63498 ` 538` eberlm@63498 ` 539` ```lemma is_unit_content_iff [simp]: "is_unit (content p) \ content p = 1" ``` eberlm@63498 ` 540` ```proof ``` eberlm@63498 ` 541` ``` assume "is_unit (content p)" ``` eberlm@63498 ` 542` ``` hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content) ``` eberlm@63498 ` 543` ``` thus "content p = 1" by simp ``` eberlm@63498 ` 544` ```qed auto ``` eberlm@63498 ` 545` eberlm@63498 ` 546` ```lemma content_smult [simp]: "content (smult c p) = normalize c * content p" ``` eberlm@63498 ` 547` ``` by (simp add: content_def coeffs_smult Gcd_mult) ``` eberlm@63498 ` 548` eberlm@63498 ` 549` ```lemma content_eq_zero_iff [simp]: "content p = 0 \ p = 0" ``` eberlm@63498 ` 550` ``` by (auto simp: content_def simp: poly_eq_iff coeffs_def) ``` eberlm@63498 ` 551` eberlm@63498 ` 552` ```definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \ 'a poly" where ``` eberlm@63498 ` 553` ``` "primitive_part p = (if p = 0 then 0 else map_poly (\x. x div content p) p)" ``` eberlm@63498 ` 554` ``` ``` eberlm@63498 ` 555` ```lemma primitive_part_0 [simp]: "primitive_part 0 = 0" ``` eberlm@63498 ` 556` ``` by (simp add: primitive_part_def) ``` eberlm@63498 ` 557` eberlm@63498 ` 558` ```lemma content_times_primitive_part [simp]: ``` eberlm@63498 ` 559` ``` fixes p :: "'a :: {idom_divide, semiring_Gcd} poly" ``` eberlm@63498 ` 560` ``` shows "smult (content p) (primitive_part p) = p" ``` eberlm@63498 ` 561` ```proof (cases "p = 0") ``` eberlm@63498 ` 562` ``` case False ``` eberlm@63498 ` 563` ``` thus ?thesis ``` eberlm@63498 ` 564` ``` unfolding primitive_part_def ``` eberlm@63498 ` 565` ``` by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs ``` eberlm@63498 ` 566` ``` intro: map_poly_idI) ``` eberlm@63498 ` 567` ```qed simp_all ``` eberlm@63498 ` 568` eberlm@63498 ` 569` ```lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \ p = 0" ``` eberlm@63498 ` 570` ```proof (cases "p = 0") ``` eberlm@63498 ` 571` ``` case False ``` eberlm@63498 ` 572` ``` hence "primitive_part p = map_poly (\x. x div content p) p" ``` eberlm@63498 ` 573` ``` by (simp add: primitive_part_def) ``` eberlm@63498 ` 574` ``` also from False have "\ = 0 \ p = 0" ``` eberlm@63498 ` 575` ``` by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs) ``` eberlm@63498 ` 576` ``` finally show ?thesis using False by simp ``` eberlm@63498 ` 577` ```qed simp ``` eberlm@63498 ` 578` eberlm@63498 ` 579` ```lemma content_primitive_part [simp]: ``` eberlm@63498 ` 580` ``` assumes "p \ 0" ``` eberlm@63498 ` 581` ``` shows "content (primitive_part p) = 1" ``` eberlm@63498 ` 582` ```proof - ``` eberlm@63498 ` 583` ``` have "p = smult (content p) (primitive_part p)" by simp ``` eberlm@63498 ` 584` ``` also have "content \ = content p * content (primitive_part p)" ``` eberlm@63498 ` 585` ``` by (simp del: content_times_primitive_part) ``` eberlm@63498 ` 586` ``` finally show ?thesis using assms by simp ``` eberlm@63498 ` 587` ```qed ``` eberlm@63498 ` 588` eberlm@63498 ` 589` ```lemma content_decompose: ``` eberlm@63498 ` 590` ``` fixes p :: "'a :: semiring_Gcd poly" ``` eberlm@63498 ` 591` ``` obtains p' where "p = smult (content p) p'" "content p' = 1" ``` eberlm@63498 ` 592` ```proof (cases "p = 0") ``` eberlm@63498 ` 593` ``` case True ``` eberlm@63498 ` 594` ``` thus ?thesis by (intro that[of 1]) simp_all ``` eberlm@63498 ` 595` ```next ``` eberlm@63498 ` 596` ``` case False ``` eberlm@63498 ` 597` ``` from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE) ``` eberlm@63498 ` 598` ``` have "content p * 1 = content p * content r" by (subst r) simp ``` eberlm@63498 ` 599` ``` with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all ``` eberlm@63498 ` 600` ``` with r show ?thesis by (intro that[of r]) simp_all ``` eberlm@63498 ` 601` ```qed ``` eberlm@63498 ` 602` eberlm@63498 ` 603` ```lemma smult_content_normalize_primitive_part [simp]: ``` eberlm@63498 ` 604` ``` "smult (content p) (normalize (primitive_part p)) = normalize p" ``` eberlm@63498 ` 605` ```proof - ``` eberlm@63498 ` 606` ``` have "smult (content p) (normalize (primitive_part p)) = ``` eberlm@63498 ` 607` ``` normalize ([:content p:] * primitive_part p)" ``` eberlm@63498 ` 608` ``` by (subst normalize_mult) (simp_all add: normalize_const_poly) ``` eberlm@63498 ` 609` ``` also have "[:content p:] * primitive_part p = p" by simp ``` eberlm@63498 ` 610` ``` finally show ?thesis . ``` eberlm@63498 ` 611` ```qed ``` eberlm@63498 ` 612` eberlm@63498 ` 613` ```lemma content_dvd_contentI [intro]: ``` eberlm@63498 ` 614` ``` "p dvd q \ content p dvd content q" ``` eberlm@63498 ` 615` ``` using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast ``` eberlm@63498 ` 616` ``` ``` eberlm@63498 ` 617` ```lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]" ``` eberlm@63498 ` 618` ``` by (simp add: primitive_part_def map_poly_pCons) ``` eberlm@63498 ` 619` ``` ``` eberlm@63498 ` 620` ```lemma primitive_part_prim: "content p = 1 \ primitive_part p = p" ``` eberlm@63498 ` 621` ``` by (auto simp: primitive_part_def) ``` eberlm@63498 ` 622` ``` ``` eberlm@63498 ` 623` ```lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p" ``` eberlm@63498 ` 624` ```proof (cases "p = 0") ``` eberlm@63498 ` 625` ``` case False ``` eberlm@63498 ` 626` ``` have "p = smult (content p) (primitive_part p)" by simp ``` eberlm@63498 ` 627` ``` also from False have "degree \ = degree (primitive_part p)" ``` eberlm@63498 ` 628` ``` by (subst degree_smult_eq) simp_all ``` eberlm@63498 ` 629` ``` finally show ?thesis .. ``` eberlm@63498 ` 630` ```qed simp_all ``` eberlm@63498 ` 631` eberlm@63498 ` 632` eberlm@63498 ` 633` ```subsection \Lifting polynomial coefficients to the field of fractions\ ``` eberlm@63498 ` 634` eberlm@63498 ` 635` ```abbreviation (input) fract_poly ``` eberlm@63498 ` 636` ``` where "fract_poly \ map_poly to_fract" ``` eberlm@63498 ` 637` eberlm@63498 ` 638` ```abbreviation (input) unfract_poly ``` eberlm@63498 ` 639` ``` where "unfract_poly \ map_poly (fst \ quot_of_fract)" ``` eberlm@63498 ` 640` ``` ``` eberlm@63498 ` 641` ```lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)" ``` eberlm@63498 ` 642` ``` by (simp add: smult_conv_map_poly map_poly_map_poly o_def) ``` eberlm@63498 ` 643` eberlm@63498 ` 644` ```lemma fract_poly_0 [simp]: "fract_poly 0 = 0" ``` eberlm@63498 ` 645` ``` by (simp add: poly_eqI coeff_map_poly) ``` eberlm@63498 ` 646` eberlm@63498 ` 647` ```lemma fract_poly_1 [simp]: "fract_poly 1 = 1" ``` eberlm@63498 ` 648` ``` by (simp add: one_poly_def map_poly_pCons) ``` eberlm@63498 ` 649` eberlm@63498 ` 650` ```lemma fract_poly_add [simp]: ``` eberlm@63498 ` 651` ``` "fract_poly (p + q) = fract_poly p + fract_poly q" ``` eberlm@63498 ` 652` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 653` eberlm@63498 ` 654` ```lemma fract_poly_diff [simp]: ``` eberlm@63498 ` 655` ``` "fract_poly (p - q) = fract_poly p - fract_poly q" ``` eberlm@63498 ` 656` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly) ``` eberlm@63498 ` 657` eberlm@63498 ` 658` ```lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\x. to_fract (f x)) A" ``` eberlm@63498 ` 659` ``` by (cases "finite A", induction A rule: finite_induct) simp_all ``` eberlm@63498 ` 660` eberlm@63498 ` 661` ```lemma fract_poly_mult [simp]: ``` eberlm@63498 ` 662` ``` "fract_poly (p * q) = fract_poly p * fract_poly q" ``` eberlm@63498 ` 663` ``` by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult) ``` eberlm@63498 ` 664` eberlm@63498 ` 665` ```lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \ p = q" ``` eberlm@63498 ` 666` ``` by (auto simp: poly_eq_iff coeff_map_poly) ``` eberlm@63498 ` 667` eberlm@63498 ` 668` ```lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \ p = 0" ``` eberlm@63498 ` 669` ``` using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff) ``` eberlm@63498 ` 670` eberlm@63498 ` 671` ```lemma fract_poly_dvd: "p dvd q \ fract_poly p dvd fract_poly q" ``` eberlm@63498 ` 672` ``` by (auto elim!: dvdE) ``` eberlm@63498 ` 673` eberlm@63498 ` 674` ```lemma msetprod_fract_poly: ``` eberlm@63498 ` 675` ``` "msetprod (image_mset (\x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))" ``` eberlm@63498 ` 676` ``` by (induction A) (simp_all add: mult_ac) ``` eberlm@63498 ` 677` ``` ``` eberlm@63498 ` 678` ```lemma is_unit_fract_poly_iff: ``` eberlm@63498 ` 679` ``` "p dvd 1 \ fract_poly p dvd 1 \ content p = 1" ``` eberlm@63498 ` 680` ```proof safe ``` eberlm@63498 ` 681` ``` assume A: "p dvd 1" ``` eberlm@63498 ` 682` ``` with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp ``` eberlm@63498 ` 683` ``` from A show "content p = 1" ``` eberlm@63498 ` 684` ``` by (auto simp: is_unit_poly_iff normalize_1_iff) ``` eberlm@63498 ` 685` ```next ``` eberlm@63498 ` 686` ``` assume A: "fract_poly p dvd 1" and B: "content p = 1" ``` eberlm@63498 ` 687` ``` from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 688` ``` { ``` eberlm@63498 ` 689` ``` fix n :: nat assume "n > 0" ``` eberlm@63498 ` 690` ``` have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly) ``` eberlm@63498 ` 691` ``` also note c ``` eberlm@63498 ` 692` ``` also from \n > 0\ have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits) ``` eberlm@63498 ` 693` ``` finally have "coeff p n = 0" by simp ``` eberlm@63498 ` 694` ``` } ``` eberlm@63498 ` 695` ``` hence "degree p \ 0" by (intro degree_le) simp_all ``` eberlm@63498 ` 696` ``` with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE) ``` eberlm@63498 ` 697` ```qed ``` eberlm@63498 ` 698` ``` ``` eberlm@63498 ` 699` ```lemma fract_poly_is_unit: "p dvd 1 \ fract_poly p dvd 1" ``` eberlm@63498 ` 700` ``` using fract_poly_dvd[of p 1] by simp ``` eberlm@63498 ` 701` eberlm@63498 ` 702` ```lemma fract_poly_smult_eqE: ``` eberlm@63498 ` 703` ``` fixes c :: "'a :: {idom_divide,ring_gcd} fract" ``` eberlm@63498 ` 704` ``` assumes "fract_poly p = smult c (fract_poly q)" ``` eberlm@63498 ` 705` ``` obtains a b ``` eberlm@63498 ` 706` ``` where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a" ``` eberlm@63498 ` 707` ```proof - ``` eberlm@63498 ` 708` ``` define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)" ``` eberlm@63498 ` 709` ``` have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)" ``` eberlm@63498 ` 710` ``` by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms) ``` eberlm@63498 ` 711` ``` hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff) ``` eberlm@63498 ` 712` ``` hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff) ``` eberlm@63498 ` 713` ``` moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b" ``` eberlm@63498 ` 714` ``` by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute ``` eberlm@63498 ` 715` ``` normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric]) ``` eberlm@63498 ` 716` ``` ultimately show ?thesis by (intro that[of a b]) ``` eberlm@63498 ` 717` ```qed ``` eberlm@63498 ` 718` eberlm@63498 ` 719` eberlm@63498 ` 720` ```subsection \Fractional content\ ``` eberlm@63498 ` 721` eberlm@63498 ` 722` ```abbreviation (input) Lcm_coeff_denoms ``` eberlm@63498 ` 723` ``` :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \ 'a" ``` eberlm@63498 ` 724` ``` where "Lcm_coeff_denoms p \ Lcm (snd ` quot_of_fract ` set (coeffs p))" ``` eberlm@63498 ` 725` ``` ``` eberlm@63498 ` 726` ```definition fract_content :: ``` eberlm@63498 ` 727` ``` "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \ 'a fract" where ``` eberlm@63498 ` 728` ``` "fract_content p = ``` eberlm@63498 ` 729` ``` (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" ``` eberlm@63498 ` 730` eberlm@63498 ` 731` ```definition primitive_part_fract :: ``` eberlm@63498 ` 732` ``` "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \ 'a poly" where ``` eberlm@63498 ` 733` ``` "primitive_part_fract p = ``` eberlm@63498 ` 734` ``` primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))" ``` eberlm@63498 ` 735` eberlm@63498 ` 736` ```lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0" ``` eberlm@63498 ` 737` ``` by (simp add: primitive_part_fract_def) ``` eberlm@63498 ` 738` eberlm@63498 ` 739` ```lemma fract_content_eq_0_iff [simp]: ``` eberlm@63498 ` 740` ``` "fract_content p = 0 \ p = 0" ``` eberlm@63498 ` 741` ``` unfolding fract_content_def Let_def Zero_fract_def ``` eberlm@63498 ` 742` ``` by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff) ``` eberlm@63498 ` 743` eberlm@63498 ` 744` ```lemma content_primitive_part_fract [simp]: "p \ 0 \ content (primitive_part_fract p) = 1" ``` eberlm@63498 ` 745` ``` unfolding primitive_part_fract_def ``` eberlm@63498 ` 746` ``` by (rule content_primitive_part) ``` eberlm@63498 ` 747` ``` (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) ``` eberlm@63498 ` 748` eberlm@63498 ` 749` ```lemma content_times_primitive_part_fract: ``` eberlm@63498 ` 750` ``` "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p" ``` eberlm@63498 ` 751` ```proof - ``` eberlm@63498 ` 752` ``` define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)" ``` eberlm@63498 ` 753` ``` have "fract_poly p' = ``` eberlm@63498 ` 754` ``` map_poly (to_fract \ fst \ quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)" ``` eberlm@63498 ` 755` ``` unfolding primitive_part_fract_def p'_def ``` eberlm@63498 ` 756` ``` by (subst map_poly_map_poly) (simp_all add: o_assoc) ``` eberlm@63498 ` 757` ``` also have "\ = smult (to_fract (Lcm_coeff_denoms p)) p" ``` eberlm@63498 ` 758` ``` proof (intro map_poly_idI, unfold o_apply) ``` eberlm@63498 ` 759` ``` fix c assume "c \ set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))" ``` eberlm@63498 ` 760` ``` then obtain c' where c: "c' \ set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'" ``` eberlm@63498 ` 761` ``` by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits) ``` eberlm@63498 ` 762` ``` note c(2) ``` eberlm@63498 ` 763` ``` also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))" ``` eberlm@63498 ` 764` ``` by simp ``` eberlm@63498 ` 765` ``` also have "to_fract (Lcm_coeff_denoms p) * \ = ``` eberlm@63498 ` 766` ``` Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))" ``` eberlm@63498 ` 767` ``` unfolding to_fract_def by (subst mult_fract) simp_all ``` eberlm@63498 ` 768` ``` also have "snd (quot_of_fract \) = 1" ``` eberlm@63498 ` 769` ``` by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto) ``` eberlm@63498 ` 770` ``` finally show "to_fract (fst (quot_of_fract c)) = c" ``` eberlm@63498 ` 771` ``` by (rule to_fract_quot_of_fract) ``` eberlm@63498 ` 772` ``` qed ``` eberlm@63498 ` 773` ``` also have "p' = smult (content p') (primitive_part p')" ``` eberlm@63498 ` 774` ``` by (rule content_times_primitive_part [symmetric]) ``` eberlm@63498 ` 775` ``` also have "primitive_part p' = primitive_part_fract p" ``` eberlm@63498 ` 776` ``` by (simp add: primitive_part_fract_def p'_def) ``` eberlm@63498 ` 777` ``` also have "fract_poly (smult (content p') (primitive_part_fract p)) = ``` eberlm@63498 ` 778` ``` smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp ``` eberlm@63498 ` 779` ``` finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) = ``` eberlm@63498 ` 780` ``` smult (to_fract (Lcm_coeff_denoms p)) p" . ``` eberlm@63498 ` 781` ``` thus ?thesis ``` eberlm@63498 ` 782` ``` by (subst (asm) smult_eq_iff) ``` eberlm@63498 ` 783` ``` (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def) ``` eberlm@63498 ` 784` ```qed ``` eberlm@63498 ` 785` eberlm@63498 ` 786` ```lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)" ``` eberlm@63498 ` 787` ```proof - ``` eberlm@63498 ` 788` ``` have "Lcm_coeff_denoms (fract_poly p) = 1" ``` eberlm@63498 ` 789` ``` by (auto simp: Lcm_1_iff set_coeffs_map_poly) ``` eberlm@63498 ` 790` ``` hence "fract_content (fract_poly p) = ``` eberlm@63498 ` 791` ``` to_fract (content (map_poly (fst \ quot_of_fract \ to_fract) p))" ``` eberlm@63498 ` 792` ``` by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff) ``` eberlm@63498 ` 793` ``` also have "map_poly (fst \ quot_of_fract \ to_fract) p = p" ``` eberlm@63498 ` 794` ``` by (intro map_poly_idI) simp_all ``` eberlm@63498 ` 795` ``` finally show ?thesis . ``` eberlm@63498 ` 796` ```qed ``` eberlm@63498 ` 797` eberlm@63498 ` 798` ```lemma content_decompose_fract: ``` eberlm@63498 ` 799` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly" ``` eberlm@63498 ` 800` ``` obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1" ``` eberlm@63498 ` 801` ```proof (cases "p = 0") ``` eberlm@63498 ` 802` ``` case True ``` eberlm@63498 ` 803` ``` hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all ``` eberlm@63498 ` 804` ``` thus ?thesis .. ``` eberlm@63498 ` 805` ```next ``` eberlm@63498 ` 806` ``` case False ``` eberlm@63498 ` 807` ``` thus ?thesis ``` eberlm@63498 ` 808` ``` by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract]) ``` eberlm@63498 ` 809` ```qed ``` eberlm@63498 ` 810` eberlm@63498 ` 811` eberlm@63498 ` 812` ```subsection \More properties of content and primitive part\ ``` eberlm@63498 ` 813` eberlm@63498 ` 814` ```lemma lift_prime_elem_poly: ``` eberlm@63633 ` 815` ``` assumes "prime_elem (c :: 'a :: semidom)" ``` eberlm@63633 ` 816` ``` shows "prime_elem [:c:]" ``` eberlm@63633 ` 817` ```proof (rule prime_elemI) ``` eberlm@63498 ` 818` ``` fix a b assume *: "[:c:] dvd a * b" ``` eberlm@63498 ` 819` ``` from * have dvd: "c dvd coeff (a * b) n" for n ``` eberlm@63498 ` 820` ``` by (subst (asm) const_poly_dvd_iff) blast ``` eberlm@63498 ` 821` ``` { ``` eberlm@63498 ` 822` ``` define m where "m = (GREATEST m. \c dvd coeff b m)" ``` eberlm@63498 ` 823` ``` assume "\[:c:] dvd b" ``` eberlm@63498 ` 824` ``` hence A: "\i. \c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast ``` eberlm@63498 ` 825` ``` have B: "\i. \c dvd coeff b i \ i < Suc (degree b)" ``` eberlm@63498 ` 826` ``` by (auto intro: le_degree simp: less_Suc_eq_le) ``` eberlm@63498 ` 827` ``` have coeff_m: "\c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B]) ``` eberlm@63498 ` 828` ``` have "i \ m" if "\c dvd coeff b i" for i ``` eberlm@63498 ` 829` ``` unfolding m_def by (rule Greatest_le[OF that B]) ``` eberlm@63498 ` 830` ``` hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force ``` eberlm@63498 ` 831` eberlm@63498 ` 832` ``` have "c dvd coeff a i" for i ``` eberlm@63498 ` 833` ``` proof (induction i rule: nat_descend_induct[of "degree a"]) ``` eberlm@63498 ` 834` ``` case (base i) ``` eberlm@63498 ` 835` ``` thus ?case by (simp add: coeff_eq_0) ``` eberlm@63498 ` 836` ``` next ``` eberlm@63498 ` 837` ``` case (descend i) ``` eberlm@63498 ` 838` ``` let ?A = "{..i+m} - {i}" ``` eberlm@63498 ` 839` ``` have "c dvd coeff (a * b) (i + m)" by (rule dvd) ``` eberlm@63498 ` 840` ``` also have "coeff (a * b) (i + m) = (\k\i + m. coeff a k * coeff b (i + m - k))" ``` eberlm@63498 ` 841` ``` by (simp add: coeff_mult) ``` eberlm@63498 ` 842` ``` also have "{..i+m} = insert i ?A" by auto ``` eberlm@63498 ` 843` ``` also have "(\k\\. coeff a k * coeff b (i + m - k)) = ``` eberlm@63498 ` 844` ``` coeff a i * coeff b m + (\k\?A. coeff a k * coeff b (i + m - k))" ``` eberlm@63498 ` 845` ``` (is "_ = _ + ?S") ``` eberlm@63498 ` 846` ``` by (subst setsum.insert) simp_all ``` eberlm@63498 ` 847` ``` finally have eq: "c dvd coeff a i * coeff b m + ?S" . ``` eberlm@63498 ` 848` ``` moreover have "c dvd ?S" ``` eberlm@63498 ` 849` ``` proof (rule dvd_setsum) ``` eberlm@63498 ` 850` ``` fix k assume k: "k \ {..i+m} - {i}" ``` eberlm@63498 ` 851` ``` show "c dvd coeff a k * coeff b (i + m - k)" ``` eberlm@63498 ` 852` ``` proof (cases "k < i") ``` eberlm@63498 ` 853` ``` case False ``` eberlm@63498 ` 854` ``` with k have "c dvd coeff a k" by (intro descend.IH) simp ``` eberlm@63498 ` 855` ``` thus ?thesis by simp ``` eberlm@63498 ` 856` ``` next ``` eberlm@63498 ` 857` ``` case True ``` eberlm@63498 ` 858` ``` hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp ``` eberlm@63498 ` 859` ``` thus ?thesis by simp ``` eberlm@63498 ` 860` ``` qed ``` eberlm@63498 ` 861` ``` qed ``` eberlm@63498 ` 862` ``` ultimately have "c dvd coeff a i * coeff b m" ``` eberlm@63498 ` 863` ``` by (simp add: dvd_add_left_iff) ``` eberlm@63498 ` 864` ``` with assms coeff_m show "c dvd coeff a i" ``` eberlm@63633 ` 865` ``` by (simp add: prime_elem_dvd_mult_iff) ``` eberlm@63498 ` 866` ``` qed ``` eberlm@63498 ` 867` ``` hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast ``` eberlm@63498 ` 868` ``` } ``` eberlm@63498 ` 869` ``` thus "[:c:] dvd a \ [:c:] dvd b" by blast ``` eberlm@63633 ` 870` ```qed (insert assms, simp_all add: prime_elem_def one_poly_def) ``` eberlm@63498 ` 871` eberlm@63498 ` 872` ```lemma prime_elem_const_poly_iff: ``` eberlm@63498 ` 873` ``` fixes c :: "'a :: semidom" ``` eberlm@63633 ` 874` ``` shows "prime_elem [:c:] \ prime_elem c" ``` eberlm@63498 ` 875` ```proof ``` eberlm@63633 ` 876` ``` assume A: "prime_elem [:c:]" ``` eberlm@63633 ` 877` ``` show "prime_elem c" ``` eberlm@63633 ` 878` ``` proof (rule prime_elemI) ``` eberlm@63498 ` 879` ``` fix a b assume "c dvd a * b" ``` eberlm@63498 ` 880` ``` hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac) ``` eberlm@63633 ` 881` ``` from A and this have "[:c:] dvd [:a:] \ [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD) ``` eberlm@63498 ` 882` ``` thus "c dvd a \ c dvd b" by simp ``` eberlm@63633 ` 883` ``` qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) ``` eberlm@63498 ` 884` ```qed (auto intro: lift_prime_elem_poly) ``` eberlm@63498 ` 885` eberlm@63498 ` 886` ```context ``` eberlm@63498 ` 887` ```begin ``` eberlm@63498 ` 888` eberlm@63498 ` 889` ```private lemma content_1_mult: ``` eberlm@63498 ` 890` ``` fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly" ``` eberlm@63498 ` 891` ``` assumes "content f = 1" "content g = 1" ``` eberlm@63498 ` 892` ``` shows "content (f * g) = 1" ``` eberlm@63498 ` 893` ```proof (cases "f * g = 0") ``` eberlm@63498 ` 894` ``` case False ``` eberlm@63498 ` 895` ``` from assms have "f \ 0" "g \ 0" by auto ``` eberlm@63498 ` 896` eberlm@63498 ` 897` ``` hence "f * g \ 0" by auto ``` eberlm@63498 ` 898` ``` { ``` eberlm@63498 ` 899` ``` assume "\is_unit (content (f * g))" ``` eberlm@63633 ` 900` ``` with False have "\p. p dvd content (f * g) \ prime p" ``` eberlm@63498 ` 901` ``` by (intro prime_divisor_exists) simp_all ``` eberlm@63633 ` 902` ``` then obtain p where "p dvd content (f * g)" "prime p" by blast ``` eberlm@63498 ` 903` ``` from \p dvd content (f * g)\ have "[:p:] dvd f * g" ``` eberlm@63498 ` 904` ``` by (simp add: const_poly_dvd_iff_dvd_content) ``` eberlm@63633 ` 905` ``` moreover from \prime p\ have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) ``` eberlm@63498 ` 906` ``` ultimately have "[:p:] dvd f \ [:p:] dvd g" ``` eberlm@63633 ` 907` ``` by (simp add: prime_elem_dvd_mult_iff) ``` eberlm@63498 ` 908` ``` with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) ``` eberlm@63633 ` 909` ``` with \prime p\ have False by simp ``` eberlm@63498 ` 910` ``` } ``` eberlm@63498 ` 911` ``` hence "is_unit (content (f * g))" by blast ``` eberlm@63498 ` 912` ``` hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) ``` eberlm@63498 ` 913` ``` thus ?thesis by simp ``` eberlm@63498 ` 914` ```qed (insert assms, auto) ``` eberlm@63498 ` 915` eberlm@63498 ` 916` ```lemma content_mult: ``` eberlm@63498 ` 917` ``` fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" ``` eberlm@63498 ` 918` ``` shows "content (p * q) = content p * content q" ``` eberlm@63498 ` 919` ```proof - ``` eberlm@63498 ` 920` ``` from content_decompose[of p] guess p' . note p = this ``` eberlm@63498 ` 921` ``` from content_decompose[of q] guess q' . note q = this ``` eberlm@63498 ` 922` ``` have "content (p * q) = content p * content q * content (p' * q')" ``` eberlm@63498 ` 923` ``` by (subst p, subst q) (simp add: mult_ac normalize_mult) ``` eberlm@63498 ` 924` ``` also from p q have "content (p' * q') = 1" by (intro content_1_mult) ``` eberlm@63498 ` 925` ``` finally show ?thesis by simp ``` eberlm@63498 ` 926` ```qed ``` eberlm@63498 ` 927` eberlm@63498 ` 928` ```lemma primitive_part_mult: ``` eberlm@63498 ` 929` ``` fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" ``` eberlm@63498 ` 930` ``` shows "primitive_part (p * q) = primitive_part p * primitive_part q" ``` eberlm@63498 ` 931` ```proof - ``` eberlm@63498 ` 932` ``` have "primitive_part (p * q) = p * q div [:content (p * q):]" ``` eberlm@63498 ` 933` ``` by (simp add: primitive_part_def div_const_poly_conv_map_poly) ``` eberlm@63498 ` 934` ``` also have "\ = (p div [:content p:]) * (q div [:content q:])" ``` eberlm@63498 ` 935` ``` by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac) ``` eberlm@63498 ` 936` ``` also have "\ = primitive_part p * primitive_part q" ``` eberlm@63498 ` 937` ``` by (simp add: primitive_part_def div_const_poly_conv_map_poly) ``` eberlm@63498 ` 938` ``` finally show ?thesis . ``` eberlm@63498 ` 939` ```qed ``` eberlm@63498 ` 940` eberlm@63498 ` 941` ```lemma primitive_part_smult: ``` eberlm@63498 ` 942` ``` fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" ``` eberlm@63498 ` 943` ``` shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)" ``` eberlm@63498 ` 944` ```proof - ``` eberlm@63498 ` 945` ``` have "smult a p = [:a:] * p" by simp ``` eberlm@63498 ` 946` ``` also have "primitive_part \ = smult (unit_factor a) (primitive_part p)" ``` eberlm@63498 ` 947` ``` by (subst primitive_part_mult) simp_all ``` eberlm@63498 ` 948` ``` finally show ?thesis . ``` eberlm@63498 ` 949` ```qed ``` eberlm@63498 ` 950` eberlm@63498 ` 951` ```lemma primitive_part_dvd_primitive_partI [intro]: ``` eberlm@63498 ` 952` ``` fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" ``` eberlm@63498 ` 953` ``` shows "p dvd q \ primitive_part p dvd primitive_part q" ``` eberlm@63498 ` 954` ``` by (auto elim!: dvdE simp: primitive_part_mult) ``` eberlm@63498 ` 955` eberlm@63498 ` 956` ```lemma content_msetprod: ``` eberlm@63498 ` 957` ``` fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset" ``` eberlm@63498 ` 958` ``` shows "content (msetprod A) = msetprod (image_mset content A)" ``` eberlm@63498 ` 959` ``` by (induction A) (simp_all add: content_mult mult_ac) ``` eberlm@63498 ` 960` eberlm@63498 ` 961` ```lemma fract_poly_dvdD: ``` eberlm@63498 ` 962` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 963` ``` assumes "fract_poly p dvd fract_poly q" "content p = 1" ``` eberlm@63498 ` 964` ``` shows "p dvd q" ``` eberlm@63498 ` 965` ```proof - ``` eberlm@63498 ` 966` ``` from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE) ``` eberlm@63498 ` 967` ``` from content_decompose_fract[of r] guess c r' . note r' = this ``` eberlm@63498 ` 968` ``` from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp ``` eberlm@63498 ` 969` ``` from fract_poly_smult_eqE[OF this] guess a b . note ab = this ``` eberlm@63498 ` 970` ``` have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2)) ``` eberlm@63498 ` 971` ``` hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4)) ``` eberlm@63498 ` 972` ``` have "1 = gcd a (normalize b)" by (simp add: ab) ``` eberlm@63498 ` 973` ``` also note eq' ``` eberlm@63498 ` 974` ``` also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4)) ``` eberlm@63498 ` 975` ``` finally have [simp]: "a = 1" by simp ``` eberlm@63498 ` 976` ``` from eq ab have "q = p * ([:b:] * r')" by simp ``` eberlm@63498 ` 977` ``` thus ?thesis by (rule dvdI) ``` eberlm@63498 ` 978` ```qed ``` eberlm@63498 ` 979` eberlm@63498 ` 980` ```lemma content_prod_eq_1_iff: ``` eberlm@63498 ` 981` ``` fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" ``` eberlm@63498 ` 982` ``` shows "content (p * q) = 1 \ content p = 1 \ content q = 1" ``` eberlm@63498 ` 983` ```proof safe ``` eberlm@63498 ` 984` ``` assume A: "content (p * q) = 1" ``` eberlm@63498 ` 985` ``` { ``` eberlm@63498 ` 986` ``` fix p q :: "'a poly" assume "content p * content q = 1" ``` eberlm@63498 ` 987` ``` hence "1 = content p * content q" by simp ``` eberlm@63498 ` 988` ``` hence "content p dvd 1" by (rule dvdI) ``` eberlm@63498 ` 989` ``` hence "content p = 1" by simp ``` eberlm@63498 ` 990` ``` } note B = this ``` eberlm@63498 ` 991` ``` from A B[of p q] B [of q p] show "content p = 1" "content q = 1" ``` eberlm@63498 ` 992` ``` by (simp_all add: content_mult mult_ac) ``` eberlm@63498 ` 993` ```qed (auto simp: content_mult) ``` eberlm@63498 ` 994` eberlm@63498 ` 995` ```end ``` eberlm@63498 ` 996` eberlm@63498 ` 997` eberlm@63498 ` 998` ```subsection \Polynomials over a field are a Euclidean ring\ ``` eberlm@63498 ` 999` eberlm@63498 ` 1000` ```context ``` eberlm@63498 ` 1001` ```begin ``` eberlm@63498 ` 1002` eberlm@63498 ` 1003` ```private definition unit_factor_field_poly :: "'a :: field poly \ 'a poly" where ``` eberlm@63498 ` 1004` ``` "unit_factor_field_poly p = [:lead_coeff p:]" ``` eberlm@63498 ` 1005` eberlm@63498 ` 1006` ```private definition normalize_field_poly :: "'a :: field poly \ 'a poly" where ``` eberlm@63498 ` 1007` ``` "normalize_field_poly p = smult (inverse (lead_coeff p)) p" ``` eberlm@63498 ` 1008` eberlm@63498 ` 1009` ```private definition euclidean_size_field_poly :: "'a :: field poly \ nat" where ``` eberlm@63498 ` 1010` ``` "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" ``` eberlm@63498 ` 1011` eberlm@63498 ` 1012` ```private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \ _) = op dvd" ``` eberlm@63498 ` 1013` ``` by (intro ext) (simp_all add: dvd.dvd_def dvd_def) ``` eberlm@63498 ` 1014` eberlm@63498 ` 1015` ```interpretation field_poly: ``` eberlm@63498 ` 1016` ``` euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" ``` eberlm@63498 ` 1017` ``` normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus ``` eberlm@63498 ` 1018` ```proof (standard, unfold dvd_field_poly) ``` eberlm@63498 ` 1019` ``` fix p :: "'a poly" ``` eberlm@63498 ` 1020` ``` show "unit_factor_field_poly p * normalize_field_poly p = p" ``` eberlm@63498 ` 1021` ``` by (cases "p = 0") ``` eberlm@63498 ` 1022` ``` (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero) ``` eberlm@63498 ` 1023` ```next ``` eberlm@63498 ` 1024` ``` fix p :: "'a poly" assume "is_unit p" ``` eberlm@63498 ` 1025` ``` thus "normalize_field_poly p = 1" ``` eberlm@63498 ` 1026` ``` by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps) ``` eberlm@63498 ` 1027` ```next ``` eberlm@63498 ` 1028` ``` fix p :: "'a poly" assume "p \ 0" ``` eberlm@63498 ` 1029` ``` thus "is_unit (unit_factor_field_poly p)" ``` eberlm@63498 ` 1030` ``` by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff) ``` eberlm@63498 ` 1031` ```qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult ``` eberlm@63498 ` 1032` ``` euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le) ``` eberlm@63498 ` 1033` eberlm@63498 ` 1034` ```private lemma field_poly_irreducible_imp_prime: ``` eberlm@63498 ` 1035` ``` assumes "irreducible (p :: 'a :: field poly)" ``` eberlm@63633 ` 1036` ``` shows "prime_elem p" ``` eberlm@63498 ` 1037` ```proof - ``` eberlm@63498 ` 1038` ``` have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. ``` eberlm@63633 ` 1039` ``` from field_poly.irreducible_imp_prime_elem[of p] assms ``` eberlm@63633 ` 1040` ``` show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly ``` eberlm@63633 ` 1041` ``` comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast ``` eberlm@63498 ` 1042` ```qed ``` eberlm@63498 ` 1043` eberlm@63498 ` 1044` ```private lemma field_poly_msetprod_prime_factorization: ``` eberlm@63498 ` 1045` ``` assumes "(x :: 'a :: field poly) \ 0" ``` eberlm@63498 ` 1046` ``` shows "msetprod (field_poly.prime_factorization x) = normalize_field_poly x" ``` eberlm@63498 ` 1047` ```proof - ``` eberlm@63498 ` 1048` ``` have A: "class.comm_monoid_mult op * (1 :: 'a poly)" .. ``` eberlm@63498 ` 1049` ``` have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod" ``` eberlm@63498 ` 1050` ``` by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def) ``` eberlm@63498 ` 1051` ``` with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp ``` eberlm@63498 ` 1052` ```qed ``` eberlm@63498 ` 1053` eberlm@63498 ` 1054` ```private lemma field_poly_in_prime_factorization_imp_prime: ``` eberlm@63498 ` 1055` ``` assumes "(p :: 'a :: field poly) \# field_poly.prime_factorization x" ``` eberlm@63633 ` 1056` ``` shows "prime_elem p" ``` eberlm@63498 ` 1057` ```proof - ``` eberlm@63498 ` 1058` ``` have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. ``` eberlm@63498 ` 1059` ``` have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 ``` eberlm@63498 ` 1060` ``` normalize_field_poly unit_factor_field_poly" .. ``` eberlm@63498 ` 1061` ``` from field_poly.in_prime_factorization_imp_prime[of p x] assms ``` eberlm@63633 ` 1062` ``` show ?thesis unfolding prime_elem_def dvd_field_poly ``` eberlm@63633 ` 1063` ``` comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast ``` eberlm@63498 ` 1064` ```qed ``` eberlm@63498 ` 1065` eberlm@63498 ` 1066` eberlm@63498 ` 1067` ```subsection \Primality and irreducibility in polynomial rings\ ``` eberlm@63498 ` 1068` eberlm@63498 ` 1069` ```lemma nonconst_poly_irreducible_iff: ``` eberlm@63498 ` 1070` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 1071` ``` assumes "degree p \ 0" ``` eberlm@63498 ` 1072` ``` shows "irreducible p \ irreducible (fract_poly p) \ content p = 1" ``` eberlm@63498 ` 1073` ```proof safe ``` eberlm@63498 ` 1074` ``` assume p: "irreducible p" ``` eberlm@63498 ` 1075` eberlm@63498 ` 1076` ``` from content_decompose[of p] guess p' . note p' = this ``` eberlm@63498 ` 1077` ``` hence "p = [:content p:] * p'" by simp ``` eberlm@63498 ` 1078` ``` from p this have "[:content p:] dvd 1 \ p' dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 1079` ``` moreover have "\p' dvd 1" ``` eberlm@63498 ` 1080` ``` proof ``` eberlm@63498 ` 1081` ``` assume "p' dvd 1" ``` eberlm@63498 ` 1082` ``` hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 1083` ``` with assms show False by contradiction ``` eberlm@63498 ` 1084` ``` qed ``` eberlm@63498 ` 1085` ``` ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff) ``` eberlm@63498 ` 1086` ``` ``` eberlm@63498 ` 1087` ``` show "irreducible (map_poly to_fract p)" ``` eberlm@63498 ` 1088` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 1089` ``` have "fract_poly p = 0 \ p = 0" by (intro map_poly_eq_0_iff) auto ``` eberlm@63498 ` 1090` ``` with assms show "map_poly to_fract p \ 0" by auto ``` eberlm@63498 ` 1091` ``` next ``` eberlm@63498 ` 1092` ``` show "\is_unit (fract_poly p)" ``` eberlm@63498 ` 1093` ``` proof ``` eberlm@63498 ` 1094` ``` assume "is_unit (map_poly to_fract p)" ``` eberlm@63498 ` 1095` ``` hence "degree (map_poly to_fract p) = 0" ``` eberlm@63498 ` 1096` ``` by (auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 1097` ``` hence "degree p = 0" by (simp add: degree_map_poly) ``` eberlm@63498 ` 1098` ``` with assms show False by contradiction ``` eberlm@63498 ` 1099` ``` qed ``` eberlm@63498 ` 1100` ``` next ``` eberlm@63498 ` 1101` ``` fix q r assume qr: "fract_poly p = q * r" ``` eberlm@63498 ` 1102` ``` from content_decompose_fract[of q] guess cg q' . note q = this ``` eberlm@63498 ` 1103` ``` from content_decompose_fract[of r] guess cr r' . note r = this ``` eberlm@63498 ` 1104` ``` from qr q r p have nz: "cg \ 0" "cr \ 0" by auto ``` eberlm@63498 ` 1105` ``` from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))" ``` eberlm@63498 ` 1106` ``` by (simp add: q r) ``` eberlm@63498 ` 1107` ``` from fract_poly_smult_eqE[OF this] guess a b . note ab = this ``` eberlm@63498 ` 1108` ``` hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:) ``` eberlm@63498 ` 1109` ``` with ab(4) have a: "a = normalize b" by (simp add: content_mult q r) ``` eberlm@63498 ` 1110` ``` hence "normalize b = gcd a b" by simp ``` eberlm@63498 ` 1111` ``` also from ab(3) have "\ = 1" . ``` eberlm@63498 ` 1112` ``` finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff) ``` eberlm@63498 ` 1113` ``` ``` eberlm@63498 ` 1114` ``` note eq ``` eberlm@63498 ` 1115` ``` also from ab(1) \a = 1\ have "cr * cg = to_fract b" by simp ``` eberlm@63498 ` 1116` ``` also have "smult \ (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp ``` eberlm@63498 ` 1117` ``` finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult) ``` eberlm@63498 ` 1118` ``` from p and this have "([:b:] * q') dvd 1 \ r' dvd 1" by (rule irreducibleD) ``` eberlm@63498 ` 1119` ``` hence "q' dvd 1 \ r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left) ``` eberlm@63498 ` 1120` ``` hence "fract_poly q' dvd 1 \ fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit) ``` eberlm@63498 ` 1121` ``` with q r show "is_unit q \ is_unit r" ``` eberlm@63498 ` 1122` ``` by (auto simp add: is_unit_smult_iff dvd_field_iff nz) ``` eberlm@63498 ` 1123` ``` qed ``` eberlm@63498 ` 1124` eberlm@63498 ` 1125` ```next ``` eberlm@63498 ` 1126` eberlm@63498 ` 1127` ``` assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1" ``` eberlm@63498 ` 1128` ``` show "irreducible p" ``` eberlm@63498 ` 1129` ``` proof (rule irreducibleI) ``` eberlm@63498 ` 1130` ``` from irred show "p \ 0" by auto ``` eberlm@63498 ` 1131` ``` next ``` eberlm@63498 ` 1132` ``` from irred show "\p dvd 1" ``` eberlm@63498 ` 1133` ``` by (auto simp: irreducible_def dest: fract_poly_is_unit) ``` eberlm@63498 ` 1134` ``` next ``` eberlm@63498 ` 1135` ``` fix q r assume qr: "p = q * r" ``` eberlm@63498 ` 1136` ``` hence "fract_poly p = fract_poly q * fract_poly r" by simp ``` eberlm@63498 ` 1137` ``` from irred and this have "fract_poly q dvd 1 \ fract_poly r dvd 1" ``` eberlm@63498 ` 1138` ``` by (rule irreducibleD) ``` eberlm@63498 ` 1139` ``` with primitive qr show "q dvd 1 \ r dvd 1" ``` eberlm@63498 ` 1140` ``` by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) ``` eberlm@63498 ` 1141` ``` qed ``` eberlm@63498 ` 1142` ```qed ``` eberlm@63498 ` 1143` eberlm@63498 ` 1144` ```private lemma irreducible_imp_prime_poly: ``` eberlm@63498 ` 1145` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 1146` ``` assumes "irreducible p" ``` eberlm@63633 ` 1147` ``` shows "prime_elem p" ``` eberlm@63498 ` 1148` ```proof (cases "degree p = 0") ``` eberlm@63498 ` 1149` ``` case True ``` eberlm@63498 ` 1150` ``` with assms show ?thesis ``` eberlm@63498 ` 1151` ``` by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff ``` eberlm@63633 ` 1152` ``` intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE) ``` eberlm@63498 ` 1153` ```next ``` eberlm@63498 ` 1154` ``` case False ``` eberlm@63498 ` 1155` ``` from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1" ``` eberlm@63498 ` 1156` ``` by (simp_all add: nonconst_poly_irreducible_iff) ``` eberlm@63633 ` 1157` ``` from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime) ``` eberlm@63498 ` 1158` ``` show ?thesis ``` eberlm@63633 ` 1159` ``` proof (rule prime_elemI) ``` eberlm@63498 ` 1160` ``` fix q r assume "p dvd q * r" ``` eberlm@63498 ` 1161` ``` hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd) ``` eberlm@63498 ` 1162` ``` hence "fract_poly p dvd fract_poly q * fract_poly r" by simp ``` eberlm@63498 ` 1163` ``` from prime and this have "fract_poly p dvd fract_poly q \ fract_poly p dvd fract_poly r" ``` eberlm@63633 ` 1164` ``` by (rule prime_elem_dvd_multD) ``` eberlm@63498 ` 1165` ``` with primitive show "p dvd q \ p dvd r" by (auto dest: fract_poly_dvdD) ``` eberlm@63498 ` 1166` ``` qed (insert assms, auto simp: irreducible_def) ``` eberlm@63498 ` 1167` ```qed ``` eberlm@63498 ` 1168` eberlm@63498 ` 1169` eberlm@63498 ` 1170` ```lemma degree_primitive_part_fract [simp]: ``` eberlm@63498 ` 1171` ``` "degree (primitive_part_fract p) = degree p" ``` eberlm@63498 ` 1172` ```proof - ``` eberlm@63498 ` 1173` ``` have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))" ``` eberlm@63498 ` 1174` ``` by (simp add: content_times_primitive_part_fract) ``` eberlm@63498 ` 1175` ``` also have "degree \ = degree (primitive_part_fract p)" ``` eberlm@63498 ` 1176` ``` by (auto simp: degree_map_poly) ``` eberlm@63498 ` 1177` ``` finally show ?thesis .. ``` eberlm@63498 ` 1178` ```qed ``` eberlm@63498 ` 1179` eberlm@63498 ` 1180` ```lemma irreducible_primitive_part_fract: ``` eberlm@63498 ` 1181` ``` fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" ``` eberlm@63498 ` 1182` ``` assumes "irreducible p" ``` eberlm@63498 ` 1183` ``` shows "irreducible (primitive_part_fract p)" ``` eberlm@63498 ` 1184` ```proof - ``` eberlm@63498 ` 1185` ``` from assms have deg: "degree (primitive_part_fract p) \ 0" ``` eberlm@63498 ` 1186` ``` by (intro notI) ``` eberlm@63498 ` 1187` ``` (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff) ``` eberlm@63498 ` 1188` ``` hence [simp]: "p \ 0" by auto ``` eberlm@63498 ` 1189` eberlm@63498 ` 1190` ``` note \irreducible p\ ``` eberlm@63498 ` 1191` ``` also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" ``` eberlm@63498 ` 1192` ``` by (simp add: content_times_primitive_part_fract) ``` eberlm@63498 ` 1193` ``` also have "irreducible \ \ irreducible (fract_poly (primitive_part_fract p))" ``` eberlm@63498 ` 1194` ``` by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff) ``` eberlm@63498 ` 1195` ``` finally show ?thesis using deg ``` eberlm@63498 ` 1196` ``` by (simp add: nonconst_poly_irreducible_iff) ``` eberlm@63498 ` 1197` ```qed ``` eberlm@63498 ` 1198` eberlm@63633 ` 1199` ```lemma prime_elem_primitive_part_fract: ``` eberlm@63498 ` 1200` ``` fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" ``` eberlm@63633 ` 1201` ``` shows "irreducible p \ prime_elem (primitive_part_fract p)" ``` eberlm@63498 ` 1202` ``` by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) ``` eberlm@63498 ` 1203` eberlm@63498 ` 1204` ```lemma irreducible_linear_field_poly: ``` eberlm@63498 ` 1205` ``` fixes a b :: "'a::field" ``` eberlm@63498 ` 1206` ``` assumes "b \ 0" ``` eberlm@63498 ` 1207` ``` shows "irreducible [:a,b:]" ``` eberlm@63498 ` 1208` ```proof (rule irreducibleI) ``` eberlm@63498 ` 1209` ``` fix p q assume pq: "[:a,b:] = p * q" ``` wenzelm@63539 ` 1210` ``` also from pq assms have "degree \ = degree p + degree q" ``` eberlm@63498 ` 1211` ``` by (intro degree_mult_eq) auto ``` eberlm@63498 ` 1212` ``` finally have "degree p = 0 \ degree q = 0" using assms by auto ``` eberlm@63498 ` 1213` ``` with assms pq show "is_unit p \ is_unit q" ``` eberlm@63498 ` 1214` ``` by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE) ``` eberlm@63498 ` 1215` ```qed (insert assms, auto simp: is_unit_poly_iff) ``` eberlm@63498 ` 1216` eberlm@63633 ` 1217` ```lemma prime_elem_linear_field_poly: ``` eberlm@63633 ` 1218` ``` "(b :: 'a :: field) \ 0 \ prime_elem [:a,b:]" ``` eberlm@63498 ` 1219` ``` by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) ``` eberlm@63498 ` 1220` eberlm@63498 ` 1221` ```lemma irreducible_linear_poly: ``` eberlm@63498 ` 1222` ``` fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" ``` eberlm@63498 ` 1223` ``` shows "b \ 0 \ coprime a b \ irreducible [:a,b:]" ``` eberlm@63498 ` 1224` ``` by (auto intro!: irreducible_linear_field_poly ``` eberlm@63498 ` 1225` ``` simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) ``` eberlm@63498 ` 1226` eberlm@63633 ` 1227` ```lemma prime_elem_linear_poly: ``` eberlm@63498 ` 1228` ``` fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" ``` eberlm@63633 ` 1229` ``` shows "b \ 0 \ coprime a b \ prime_elem [:a,b:]" ``` eberlm@63498 ` 1230` ``` by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly) ``` eberlm@63498 ` 1231` eberlm@63498 ` 1232` ``` ``` eberlm@63498 ` 1233` ```subsection \Prime factorisation of polynomials\ ``` eberlm@63498 ` 1234` eberlm@63498 ` 1235` ```private lemma poly_prime_factorization_exists_content_1: ``` eberlm@63498 ` 1236` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 1237` ``` assumes "p \ 0" "content p = 1" ``` eberlm@63633 ` 1238` ``` shows "\A. (\p. p \# A \ prime_elem p) \ msetprod A = normalize p" ``` eberlm@63498 ` 1239` ```proof - ``` eberlm@63498 ` 1240` ``` let ?P = "field_poly.prime_factorization (fract_poly p)" ``` eberlm@63498 ` 1241` ``` define c where "c = msetprod (image_mset fract_content ?P)" ``` eberlm@63498 ` 1242` ``` define c' where "c' = c * to_fract (lead_coeff p)" ``` eberlm@63498 ` 1243` ``` define e where "e = msetprod (image_mset primitive_part_fract ?P)" ``` eberlm@63498 ` 1244` ``` define A where "A = image_mset (normalize \ primitive_part_fract) ?P" ``` eberlm@63498 ` 1245` ``` have "content e = (\x\#field_poly.prime_factorization (map_poly to_fract p). ``` eberlm@63498 ` 1246` ``` content (primitive_part_fract x))" ``` eberlm@63498 ` 1247` ``` by (simp add: e_def content_msetprod multiset.map_comp o_def) ``` eberlm@63498 ` 1248` ``` also have "image_mset (\x. content (primitive_part_fract x)) ?P = image_mset (\_. 1) ?P" ``` eberlm@63498 ` 1249` ``` by (intro image_mset_cong content_primitive_part_fract) auto ``` eberlm@63498 ` 1250` ``` finally have content_e: "content e = 1" by (simp add: msetprod_const) ``` eberlm@63498 ` 1251` ``` ``` eberlm@63498 ` 1252` ``` have "fract_poly p = unit_factor_field_poly (fract_poly p) * ``` eberlm@63498 ` 1253` ``` normalize_field_poly (fract_poly p)" by simp ``` eberlm@63498 ` 1254` ``` also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" ``` eberlm@63498 ` 1255` ``` by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly) ``` eberlm@63498 ` 1256` ``` also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" ``` eberlm@63498 ` 1257` ``` by (subst field_poly_msetprod_prime_factorization) simp_all ``` eberlm@63498 ` 1258` ``` also have "\ = msetprod (image_mset id ?P)" by simp ``` eberlm@63498 ` 1259` ``` also have "image_mset id ?P = ``` eberlm@63498 ` 1260` ``` image_mset (\x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P" ``` eberlm@63498 ` 1261` ``` by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract) ``` eberlm@63498 ` 1262` ``` also have "msetprod \ = smult c (fract_poly e)" ``` eberlm@63498 ` 1263` ``` by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def) ``` eberlm@63498 ` 1264` ``` also have "[:to_fract (lead_coeff p):] * \ = smult c' (fract_poly e)" ``` eberlm@63498 ` 1265` ``` by (simp add: c'_def) ``` eberlm@63498 ` 1266` ``` finally have eq: "fract_poly p = smult c' (fract_poly e)" . ``` eberlm@63498 ` 1267` ``` also obtain b where b: "c' = to_fract b" "is_unit b" ``` eberlm@63498 ` 1268` ``` proof - ``` eberlm@63498 ` 1269` ``` from fract_poly_smult_eqE[OF eq] guess a b . note ab = this ``` eberlm@63498 ` 1270` ``` from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: ) ``` eberlm@63498 ` 1271` ``` with assms content_e have "a = normalize b" by (simp add: ab(4)) ``` eberlm@63498 ` 1272` ``` with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff) ``` eberlm@63498 ` 1273` ``` with ab ab' have "c' = to_fract b" by auto ``` eberlm@63498 ` 1274` ``` from this and \is_unit b\ show ?thesis by (rule that) ``` eberlm@63498 ` 1275` ``` qed ``` eberlm@63498 ` 1276` ``` hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp ``` eberlm@63498 ` 1277` ``` finally have "p = smult b e" by (simp only: fract_poly_eq_iff) ``` eberlm@63498 ` 1278` ``` hence "p = [:b:] * e" by simp ``` eberlm@63498 ` 1279` ``` with b have "normalize p = normalize e" ``` eberlm@63498 ` 1280` ``` by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff) ``` eberlm@63498 ` 1281` ``` also have "normalize e = msetprod A" ``` eberlm@63498 ` 1282` ``` by (simp add: multiset.map_comp e_def A_def normalize_msetprod) ``` eberlm@63498 ` 1283` ``` finally have "msetprod A = normalize p" .. ``` eberlm@63498 ` 1284` ``` ``` eberlm@63633 ` 1285` ``` have "prime_elem p" if "p \# A" for p ``` eberlm@63633 ` 1286` ``` using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible ``` eberlm@63498 ` 1287` ``` dest!: field_poly_in_prime_factorization_imp_prime ) ``` eberlm@63498 ` 1288` ``` from this and \msetprod A = normalize p\ show ?thesis ``` eberlm@63498 ` 1289` ``` by (intro exI[of _ A]) blast ``` eberlm@63498 ` 1290` ```qed ``` eberlm@63498 ` 1291` eberlm@63498 ` 1292` ```lemma poly_prime_factorization_exists: ``` eberlm@63498 ` 1293` ``` fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" ``` eberlm@63498 ` 1294` ``` assumes "p \ 0" ``` eberlm@63633 ` 1295` ``` shows "\A. (\p. p \# A \ prime_elem p) \ msetprod A = normalize p" ``` eberlm@63498 ` 1296` ```proof - ``` eberlm@63498 ` 1297` ``` define B where "B = image_mset (\x. [:x:]) (prime_factorization (content p))" ``` eberlm@63633 ` 1298` ``` have "\A. (\p. p \# A \ prime_elem p) \ msetprod A = normalize (primitive_part p)" ``` eberlm@63498 ` 1299` ``` by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all) ``` eberlm@63498 ` 1300` ``` then guess A by (elim exE conjE) note A = this ``` eberlm@63498 ` 1301` ``` moreover from assms have "msetprod B = [:content p:]" ``` eberlm@63498 ` 1302` ``` by (simp add: B_def msetprod_const_poly msetprod_prime_factorization) ``` eberlm@63633 ` 1303` ``` moreover have "\p. p \# B \ prime_elem p" ``` eberlm@63498 ` 1304` ``` by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime) ``` eberlm@63498 ` 1305` ``` ultimately show ?thesis by (intro exI[of _ "B + A"]) auto ``` eberlm@63498 ` 1306` ```qed ``` eberlm@63498 ` 1307` eberlm@63498 ` 1308` ```end ``` eberlm@63498 ` 1309` eberlm@63498 ` 1310` eberlm@63498 ` 1311` ```subsection \Typeclass instances\ ``` eberlm@63498 ` 1312` eberlm@63498 ` 1313` ```instance poly :: (factorial_ring_gcd) factorial_semiring ``` eberlm@63498 ` 1314` ``` by standard (rule poly_prime_factorization_exists) ``` eberlm@63498 ` 1315` eberlm@63498 ` 1316` ```instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd ``` eberlm@63498 ` 1317` ```begin ``` eberlm@63498 ` 1318` eberlm@63498 ` 1319` ```definition gcd_poly :: "'a poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 1320` ``` [code del]: "gcd_poly = gcd_factorial" ``` eberlm@63498 ` 1321` eberlm@63498 ` 1322` ```definition lcm_poly :: "'a poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 1323` ``` [code del]: "lcm_poly = lcm_factorial" ``` eberlm@63498 ` 1324` ``` ``` eberlm@63498 ` 1325` ```definition Gcd_poly :: "'a poly set \ 'a poly" where ``` eberlm@63498 ` 1326` ``` [code del]: "Gcd_poly = Gcd_factorial" ``` eberlm@63498 ` 1327` eberlm@63498 ` 1328` ```definition Lcm_poly :: "'a poly set \ 'a poly" where ``` eberlm@63498 ` 1329` ``` [code del]: "Lcm_poly = Lcm_factorial" ``` eberlm@63498 ` 1330` ``` ``` eberlm@63498 ` 1331` ```instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) ``` eberlm@63498 ` 1332` eberlm@63498 ` 1333` ```end ``` eberlm@63498 ` 1334` eberlm@63498 ` 1335` ```instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring ``` eberlm@63498 ` 1336` ```begin ``` eberlm@63498 ` 1337` eberlm@63498 ` 1338` ```definition euclidean_size_poly :: "'a poly \ nat" where ``` eberlm@63498 ` 1339` ``` "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" ``` eberlm@63498 ` 1340` eberlm@63498 ` 1341` ```instance ``` eberlm@63498 ` 1342` ``` by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le) ``` eberlm@63498 ` 1343` ```end ``` eberlm@63498 ` 1344` eberlm@63499 ` 1345` eberlm@63498 ` 1346` ```instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd ``` eberlm@63498 ` 1347` ``` by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial) ``` eberlm@63498 ` 1348` eberlm@63498 ` 1349` ``` ``` eberlm@63498 ` 1350` ```subsection \Polynomial GCD\ ``` eberlm@63498 ` 1351` eberlm@63498 ` 1352` ```lemma gcd_poly_decompose: ``` eberlm@63498 ` 1353` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 1354` ``` shows "gcd p q = ``` eberlm@63498 ` 1355` ``` smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" ``` eberlm@63498 ` 1356` ```proof (rule sym, rule gcdI) ``` eberlm@63498 ` 1357` ``` have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd ``` eberlm@63498 ` 1358` ``` [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all ``` eberlm@63498 ` 1359` ``` thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p" ``` eberlm@63498 ` 1360` ``` by simp ``` eberlm@63498 ` 1361` ```next ``` eberlm@63498 ` 1362` ``` have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd ``` eberlm@63498 ` 1363` ``` [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all ``` eberlm@63498 ` 1364` ``` thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q" ``` eberlm@63498 ` 1365` ``` by simp ``` eberlm@63498 ` 1366` ```next ``` eberlm@63498 ` 1367` ``` fix d assume "d dvd p" "d dvd q" ``` eberlm@63498 ` 1368` ``` hence "[:content d:] * primitive_part d dvd ``` eberlm@63498 ` 1369` ``` [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)" ``` eberlm@63498 ` 1370` ``` by (intro mult_dvd_mono) auto ``` eberlm@63498 ` 1371` ``` thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" ``` eberlm@63498 ` 1372` ``` by simp ``` eberlm@63498 ` 1373` ```qed (auto simp: normalize_smult) ``` eberlm@63498 ` 1374` ``` ``` eberlm@63498 ` 1375` eberlm@63498 ` 1376` ```lemma gcd_poly_pseudo_mod: ``` eberlm@63498 ` 1377` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 1378` ``` assumes nz: "q \ 0" and prim: "content p = 1" "content q = 1" ``` eberlm@63498 ` 1379` ``` shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 1380` ```proof - ``` eberlm@63498 ` 1381` ``` define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)" ``` eberlm@63498 ` 1382` ``` define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]" ``` eberlm@63498 ` 1383` ``` have [simp]: "primitive_part a = unit_factor a" ``` eberlm@63498 ` 1384` ``` by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0) ``` eberlm@63498 ` 1385` ``` from nz have [simp]: "a \ 0" by (auto simp: a_def) ``` eberlm@63498 ` 1386` ``` ``` eberlm@63498 ` 1387` ``` have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def) ``` eberlm@63498 ` 1388` ``` have "gcd (q * r + s) q = gcd q s" ``` eberlm@63498 ` 1389` ``` using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac) ``` eberlm@63498 ` 1390` ``` with pseudo_divmod(1)[OF nz rs] ``` eberlm@63498 ` 1391` ``` have "gcd (p * a) q = gcd q s" by (simp add: a_def) ``` eberlm@63498 ` 1392` ``` also from prim have "gcd (p * a) q = gcd p q" ``` eberlm@63498 ` 1393` ``` by (subst gcd_poly_decompose) ``` eberlm@63498 ` 1394` ``` (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim ``` eberlm@63498 ` 1395` ``` simp del: mult_pCons_right ) ``` eberlm@63498 ` 1396` ``` also from prim have "gcd q s = gcd q (primitive_part s)" ``` eberlm@63498 ` 1397` ``` by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim) ``` eberlm@63498 ` 1398` ``` also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def) ``` eberlm@63498 ` 1399` ``` finally show ?thesis . ``` eberlm@63498 ` 1400` ```qed ``` eberlm@63498 ` 1401` eberlm@63498 ` 1402` ```lemma degree_pseudo_mod_less: ``` eberlm@63498 ` 1403` ``` assumes "q \ 0" "pseudo_mod p q \ 0" ``` eberlm@63498 ` 1404` ``` shows "degree (pseudo_mod p q) < degree q" ``` eberlm@63498 ` 1405` ``` using pseudo_mod(2)[of q p] assms by auto ``` eberlm@63498 ` 1406` eberlm@63498 ` 1407` ```function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \ 'a poly \ 'a poly" where ``` eberlm@63498 ` 1408` ``` "gcd_poly_code_aux p q = ``` eberlm@63498 ` 1409` ``` (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" ``` eberlm@63498 ` 1410` ```by auto ``` eberlm@63498 ` 1411` ```termination ``` eberlm@63498 ` 1412` ``` by (relation "measure ((\p. if p = 0 then 0 else Suc (degree p)) \ snd)") ``` eberlm@63498 ` 1413` ``` (auto simp: degree_primitive_part degree_pseudo_mod_less) ``` eberlm@63498 ` 1414` eberlm@63498 ` 1415` ```declare gcd_poly_code_aux.simps [simp del] ``` eberlm@63498 ` 1416` eberlm@63498 ` 1417` ```lemma gcd_poly_code_aux_correct: ``` eberlm@63498 ` 1418` ``` assumes "content p = 1" "q = 0 \ content q = 1" ``` eberlm@63498 ` 1419` ``` shows "gcd_poly_code_aux p q = gcd p q" ``` eberlm@63498 ` 1420` ``` using assms ``` eberlm@63498 ` 1421` ```proof (induction p q rule: gcd_poly_code_aux.induct) ``` eberlm@63498 ` 1422` ``` case (1 p q) ``` eberlm@63498 ` 1423` ``` show ?case ``` eberlm@63498 ` 1424` ``` proof (cases "q = 0") ``` eberlm@63498 ` 1425` ``` case True ``` eberlm@63498 ` 1426` ``` thus ?thesis by (subst gcd_poly_code_aux.simps) auto ``` eberlm@63498 ` 1427` ``` next ``` eberlm@63498 ` 1428` ``` case False ``` eberlm@63498 ` 1429` ``` hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 1430` ``` by (subst gcd_poly_code_aux.simps) simp_all ``` eberlm@63498 ` 1431` ``` also from "1.prems" False ``` eberlm@63498 ` 1432` ``` have "primitive_part (pseudo_mod p q) = 0 \ ``` eberlm@63498 ` 1433` ``` content (primitive_part (pseudo_mod p q)) = 1" ``` eberlm@63498 ` 1434` ``` by (cases "pseudo_mod p q = 0") auto ``` eberlm@63498 ` 1435` ``` with "1.prems" False ``` eberlm@63498 ` 1436` ``` have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = ``` eberlm@63498 ` 1437` ``` gcd q (primitive_part (pseudo_mod p q))" ``` eberlm@63498 ` 1438` ``` by (intro 1) simp_all ``` eberlm@63498 ` 1439` ``` also from "1.prems" False ``` eberlm@63498 ` 1440` ``` have "\ = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto ``` eberlm@63498 ` 1441` ``` finally show ?thesis . ``` eberlm@63498 ` 1442` ``` qed ``` eberlm@63498 ` 1443` ```qed ``` eberlm@63498 ` 1444` eberlm@63498 ` 1445` ```definition gcd_poly_code ``` eberlm@63498 ` 1446` ``` :: "'a :: factorial_ring_gcd poly \ 'a poly \ 'a poly" ``` eberlm@63498 ` 1447` ``` where "gcd_poly_code p q = ``` eberlm@63498 ` 1448` ``` (if p = 0 then normalize q else if q = 0 then normalize p else ``` eberlm@63498 ` 1449` ``` smult (gcd (content p) (content q)) ``` eberlm@63498 ` 1450` ``` (gcd_poly_code_aux (primitive_part p) (primitive_part q)))" ``` eberlm@63498 ` 1451` eberlm@63498 ` 1452` ```lemma lcm_poly_code [code]: ``` eberlm@63498 ` 1453` ``` fixes p q :: "'a :: factorial_ring_gcd poly" ``` eberlm@63498 ` 1454` ``` shows "lcm p q = normalize (p * q) div gcd p q" ``` eberlm@63498 ` 1455` ``` by (rule lcm_gcd) ``` eberlm@63498 ` 1456` eberlm@63498 ` 1457` ```lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q" ``` eberlm@63498 ` 1458` ``` by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric]) ``` eberlm@63498 ` 1459` eberlm@63498 ` 1460` ```declare Gcd_set ``` eberlm@63498 ` 1461` ``` [where ?'a = "'a :: factorial_ring_gcd poly", code] ``` eberlm@63498 ` 1462` eberlm@63498 ` 1463` ```declare Lcm_set ``` eberlm@63498 ` 1464` ``` [where ?'a = "'a :: factorial_ring_gcd poly", code] ``` eberlm@63498 ` 1465` ``` ``` eberlm@63498 ` 1466` ```value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}" ``` eberlm@63498 ` 1467` eberlm@63498 ` 1468` ```end ```