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