src/HOL/Library/Polynomial_Factorial.thy
author haftmann
Wed Jan 04 21:28:29 2017 +0100 (2017-01-04)
changeset 64786 340db65fd2c1
parent 64784 5cb5e7ecb284
child 64794 6f7391f28197
permissions -rw-r--r--
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
     1 (*  Title:      HOL/Library/Polynomial_Factorial.thy
     2     Author:     Brian Huffman
     3     Author:     Clemens Ballarin
     4     Author:     Amine Chaieb
     5     Author:     Florian Haftmann
     6     Author:     Manuel Eberl
     7 *)
     8 
     9 theory Polynomial_Factorial
    10 imports 
    11   Complex_Main
    12   "~~/src/HOL/Library/Polynomial"
    13   "~~/src/HOL/Library/Normalized_Fraction"
    14   "~~/src/HOL/Library/Field_as_Ring"
    15 begin
    16 
    17 subsection \<open>Various facts about polynomials\<close>
    18 
    19 lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
    20   by (induction A) (simp_all add: one_poly_def mult_ac)
    21 
    22 lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
    23 proof -
    24   have "smult c p = [:c:] * p" by simp
    25   also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
    26   proof safe
    27     assume A: "[:c:] * p dvd 1"
    28     thus "p dvd 1" by (rule dvd_mult_right)
    29     from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
    30     have "c dvd c * (coeff p 0 * coeff q 0)" by simp
    31     also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
    32     also note B [symmetric]
    33     finally show "c dvd 1" by simp
    34   next
    35     assume "c dvd 1" "p dvd 1"
    36     from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
    37     hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
    38     hence "[:c:] dvd 1" by (rule dvdI)
    39     from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
    40   qed
    41   finally show ?thesis .
    42 qed
    43 
    44 lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
    45   using degree_mod_less[of b a] by auto
    46   
    47 lemma smult_eq_iff:
    48   assumes "(b :: 'a :: field) \<noteq> 0"
    49   shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
    50 proof
    51   assume "smult a p = smult b q"
    52   also from assms have "smult (inverse b) \<dots> = q" by simp
    53   finally show "smult (a / b) p = q" by (simp add: field_simps)
    54 qed (insert assms, auto)
    55 
    56 lemma irreducible_const_poly_iff:
    57   fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
    58   shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
    59 proof
    60   assume A: "irreducible c"
    61   show "irreducible [:c:]"
    62   proof (rule irreducibleI)
    63     fix a b assume ab: "[:c:] = a * b"
    64     hence "degree [:c:] = degree (a * b)" by (simp only: )
    65     also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
    66     hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
    67     finally have "degree a = 0" "degree b = 0" by auto
    68     then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
    69     from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
    70     hence "c = a' * b'" by (simp add: ab' mult_ac)
    71     from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
    72     with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
    73   qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
    74 next
    75   assume A: "irreducible [:c:]"
    76   show "irreducible c"
    77   proof (rule irreducibleI)
    78     fix a b assume ab: "c = a * b"
    79     hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
    80     from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
    81     thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
    82   qed (insert A, auto simp: irreducible_def one_poly_def)
    83 qed
    84 
    85 
    86 subsection \<open>Lifting elements into the field of fractions\<close>
    87 
    88 definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
    89   -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
    90 
    91 lemma to_fract_0 [simp]: "to_fract 0 = 0"
    92   by (simp add: to_fract_def eq_fract Zero_fract_def)
    93 
    94 lemma to_fract_1 [simp]: "to_fract 1 = 1"
    95   by (simp add: to_fract_def eq_fract One_fract_def)
    96 
    97 lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
    98   by (simp add: to_fract_def)
    99 
   100 lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
   101   by (simp add: to_fract_def)
   102   
   103 lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
   104   by (simp add: to_fract_def)
   105   
   106 lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
   107   by (simp add: to_fract_def)
   108 
   109 lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
   110   by (simp add: to_fract_def eq_fract)
   111   
   112 lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
   113   by (simp add: to_fract_def Zero_fract_def eq_fract)
   114 
   115 lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
   116   by transfer simp
   117 
   118 lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
   119   by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
   120 
   121 lemma to_fract_quot_of_fract:
   122   assumes "snd (quot_of_fract x) = 1"
   123   shows   "to_fract (fst (quot_of_fract x)) = x"
   124 proof -
   125   have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
   126   also note assms
   127   finally show ?thesis by (simp add: to_fract_def)
   128 qed
   129 
   130 lemma snd_quot_of_fract_Fract_whole:
   131   assumes "y dvd x"
   132   shows   "snd (quot_of_fract (Fract x y)) = 1"
   133   using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
   134   
   135 lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
   136   by (simp add: to_fract_def)
   137 
   138 lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
   139   unfolding to_fract_def by transfer (simp add: normalize_quot_def)
   140 
   141 lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
   142   by transfer simp
   143  
   144 lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
   145   unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
   146 
   147 lemma coprime_quot_of_fract:
   148   "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
   149   by transfer (simp add: coprime_normalize_quot)
   150 
   151 lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
   152   using quot_of_fract_in_normalized_fracts[of x] 
   153   by (simp add: normalized_fracts_def case_prod_unfold)  
   154 
   155 lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
   156   by (subst (2) normalize_mult_unit_factor [symmetric, of x])
   157      (simp del: normalize_mult_unit_factor)
   158   
   159 lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
   160   by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
   161 
   162 
   163 subsection \<open>Content and primitive part of a polynomial\<close>
   164 
   165 definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
   166   "content p = Gcd (set (coeffs p))"
   167 
   168 lemma content_0 [simp]: "content 0 = 0"
   169   by (simp add: content_def)
   170 
   171 lemma content_1 [simp]: "content 1 = 1"
   172   by (simp add: content_def)
   173 
   174 lemma content_const [simp]: "content [:c:] = normalize c"
   175   by (simp add: content_def cCons_def)
   176 
   177 lemma const_poly_dvd_iff_dvd_content:
   178   fixes c :: "'a :: semiring_Gcd"
   179   shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
   180 proof (cases "p = 0")
   181   case [simp]: False
   182   have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
   183   also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
   184   proof safe
   185     fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
   186     thus "c dvd coeff p n"
   187       by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
   188   qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
   189   also have "\<dots> \<longleftrightarrow> c dvd content p"
   190     by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
   191           dvd_mult_unit_iff lead_coeff_nonzero)
   192   finally show ?thesis .
   193 qed simp_all
   194 
   195 lemma content_dvd [simp]: "[:content p:] dvd p"
   196   by (subst const_poly_dvd_iff_dvd_content) simp_all
   197   
   198 lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
   199   by (cases "n \<le> degree p") 
   200      (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
   201 
   202 lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
   203   by (simp add: content_def Gcd_dvd)
   204 
   205 lemma normalize_content [simp]: "normalize (content p) = content p"
   206   by (simp add: content_def)
   207 
   208 lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
   209 proof
   210   assume "is_unit (content p)"
   211   hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
   212   thus "content p = 1" by simp
   213 qed auto
   214 
   215 lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
   216   by (simp add: content_def coeffs_smult Gcd_mult)
   217 
   218 lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   219   by (auto simp: content_def simp: poly_eq_iff coeffs_def)
   220 
   221 definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
   222   "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
   223   
   224 lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
   225   by (simp add: primitive_part_def)
   226 
   227 lemma content_times_primitive_part [simp]:
   228   fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
   229   shows "smult (content p) (primitive_part p) = p"
   230 proof (cases "p = 0")
   231   case False
   232   thus ?thesis
   233   unfolding primitive_part_def
   234   by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
   235            intro: map_poly_idI)
   236 qed simp_all
   237 
   238 lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   239 proof (cases "p = 0")
   240   case False
   241   hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   242     by (simp add:  primitive_part_def)
   243   also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   244     by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   245   finally show ?thesis using False by simp
   246 qed simp
   247 
   248 lemma content_primitive_part [simp]:
   249   assumes "p \<noteq> 0"
   250   shows   "content (primitive_part p) = 1"
   251 proof -
   252   have "p = smult (content p) (primitive_part p)" by simp
   253   also have "content \<dots> = content p * content (primitive_part p)" 
   254     by (simp del: content_times_primitive_part)
   255   finally show ?thesis using assms by simp
   256 qed
   257 
   258 lemma content_decompose:
   259   fixes p :: "'a :: semiring_Gcd poly"
   260   obtains p' where "p = smult (content p) p'" "content p' = 1"
   261 proof (cases "p = 0")
   262   case True
   263   thus ?thesis by (intro that[of 1]) simp_all
   264 next
   265   case False
   266   from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
   267   have "content p * 1 = content p * content r" by (subst r) simp
   268   with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
   269   with r show ?thesis by (intro that[of r]) simp_all
   270 qed
   271 
   272 lemma smult_content_normalize_primitive_part [simp]:
   273   "smult (content p) (normalize (primitive_part p)) = normalize p"
   274 proof -
   275   have "smult (content p) (normalize (primitive_part p)) = 
   276           normalize ([:content p:] * primitive_part p)" 
   277     by (subst normalize_mult) (simp_all add: normalize_const_poly)
   278   also have "[:content p:] * primitive_part p = p" by simp
   279   finally show ?thesis .
   280 qed
   281 
   282 lemma content_dvd_contentI [intro]:
   283   "p dvd q \<Longrightarrow> content p dvd content q"
   284   using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   285   
   286 lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   287   by (simp add: primitive_part_def map_poly_pCons)
   288  
   289 lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   290   by (auto simp: primitive_part_def)
   291   
   292 lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   293 proof (cases "p = 0")
   294   case False
   295   have "p = smult (content p) (primitive_part p)" by simp
   296   also from False have "degree \<dots> = degree (primitive_part p)"
   297     by (subst degree_smult_eq) simp_all
   298   finally show ?thesis ..
   299 qed simp_all
   300 
   301 
   302 subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
   303 
   304 abbreviation (input) fract_poly 
   305   where "fract_poly \<equiv> map_poly to_fract"
   306 
   307 abbreviation (input) unfract_poly 
   308   where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
   309   
   310 lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
   311   by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
   312 
   313 lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
   314   by (simp add: poly_eqI coeff_map_poly)
   315 
   316 lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
   317   by (simp add: one_poly_def map_poly_pCons)
   318 
   319 lemma fract_poly_add [simp]:
   320   "fract_poly (p + q) = fract_poly p + fract_poly q"
   321   by (intro poly_eqI) (simp_all add: coeff_map_poly)
   322 
   323 lemma fract_poly_diff [simp]:
   324   "fract_poly (p - q) = fract_poly p - fract_poly q"
   325   by (intro poly_eqI) (simp_all add: coeff_map_poly)
   326 
   327 lemma to_fract_sum [simp]: "to_fract (sum f A) = sum (\<lambda>x. to_fract (f x)) A"
   328   by (cases "finite A", induction A rule: finite_induct) simp_all 
   329 
   330 lemma fract_poly_mult [simp]:
   331   "fract_poly (p * q) = fract_poly p * fract_poly q"
   332   by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
   333 
   334 lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
   335   by (auto simp: poly_eq_iff coeff_map_poly)
   336 
   337 lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
   338   using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
   339 
   340 lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
   341   by (auto elim!: dvdE)
   342 
   343 lemma prod_mset_fract_poly: 
   344   "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
   345   by (induction A) (simp_all add: mult_ac)
   346   
   347 lemma is_unit_fract_poly_iff:
   348   "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
   349 proof safe
   350   assume A: "p dvd 1"
   351   with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
   352   from A show "content p = 1"
   353     by (auto simp: is_unit_poly_iff normalize_1_iff)
   354 next
   355   assume A: "fract_poly p dvd 1" and B: "content p = 1"
   356   from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
   357   {
   358     fix n :: nat assume "n > 0"
   359     have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
   360     also note c
   361     also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
   362     finally have "coeff p n = 0" by simp
   363   }
   364   hence "degree p \<le> 0" by (intro degree_le) simp_all
   365   with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
   366 qed
   367   
   368 lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
   369   using fract_poly_dvd[of p 1] by simp
   370 
   371 lemma fract_poly_smult_eqE:
   372   fixes c :: "'a :: {idom_divide,ring_gcd} fract"
   373   assumes "fract_poly p = smult c (fract_poly q)"
   374   obtains a b 
   375     where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
   376 proof -
   377   define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
   378   have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
   379     by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
   380   hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
   381   hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
   382   moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
   383     by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
   384           normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
   385   ultimately show ?thesis by (intro that[of a b])
   386 qed
   387 
   388 
   389 subsection \<open>Fractional content\<close>
   390 
   391 abbreviation (input) Lcm_coeff_denoms 
   392     :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
   393   where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
   394   
   395 definition fract_content :: 
   396       "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
   397   "fract_content p = 
   398      (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
   399 
   400 definition primitive_part_fract :: 
   401       "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
   402   "primitive_part_fract p = 
   403      primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
   404 
   405 lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
   406   by (simp add: primitive_part_fract_def)
   407 
   408 lemma fract_content_eq_0_iff [simp]:
   409   "fract_content p = 0 \<longleftrightarrow> p = 0"
   410   unfolding fract_content_def Let_def Zero_fract_def
   411   by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
   412 
   413 lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
   414   unfolding primitive_part_fract_def
   415   by (rule content_primitive_part)
   416      (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
   417 
   418 lemma content_times_primitive_part_fract:
   419   "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
   420 proof -
   421   define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
   422   have "fract_poly p' = 
   423           map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
   424     unfolding primitive_part_fract_def p'_def 
   425     by (subst map_poly_map_poly) (simp_all add: o_assoc)
   426   also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
   427   proof (intro map_poly_idI, unfold o_apply)
   428     fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
   429     then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
   430       by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
   431     note c(2)
   432     also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   433       by simp
   434     also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
   435                  Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   436       unfolding to_fract_def by (subst mult_fract) simp_all
   437     also have "snd (quot_of_fract \<dots>) = 1"
   438       by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
   439     finally show "to_fract (fst (quot_of_fract c)) = c"
   440       by (rule to_fract_quot_of_fract)
   441   qed
   442   also have "p' = smult (content p') (primitive_part p')" 
   443     by (rule content_times_primitive_part [symmetric])
   444   also have "primitive_part p' = primitive_part_fract p"
   445     by (simp add: primitive_part_fract_def p'_def)
   446   also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
   447                smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
   448   finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
   449                       smult (to_fract (Lcm_coeff_denoms p)) p" .
   450   thus ?thesis
   451     by (subst (asm) smult_eq_iff)
   452        (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
   453 qed
   454 
   455 lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
   456 proof -
   457   have "Lcm_coeff_denoms (fract_poly p) = 1"
   458     by (auto simp: set_coeffs_map_poly)
   459   hence "fract_content (fract_poly p) = 
   460            to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
   461     by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
   462   also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
   463     by (intro map_poly_idI) simp_all
   464   finally show ?thesis .
   465 qed
   466 
   467 lemma content_decompose_fract:
   468   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
   469   obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
   470 proof (cases "p = 0")
   471   case True
   472   hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
   473   thus ?thesis ..
   474 next
   475   case False
   476   thus ?thesis
   477     by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
   478 qed
   479 
   480 
   481 subsection \<open>More properties of content and primitive part\<close>
   482 
   483 lemma lift_prime_elem_poly:
   484   assumes "prime_elem (c :: 'a :: semidom)"
   485   shows   "prime_elem [:c:]"
   486 proof (rule prime_elemI)
   487   fix a b assume *: "[:c:] dvd a * b"
   488   from * have dvd: "c dvd coeff (a * b) n" for n
   489     by (subst (asm) const_poly_dvd_iff) blast
   490   {
   491     define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
   492     assume "\<not>[:c:] dvd b"
   493     hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
   494     have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
   495       by (auto intro: le_degree simp: less_Suc_eq_le)
   496     have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
   497     have "i \<le> m" if "\<not>c dvd coeff b i" for i
   498       unfolding m_def by (rule Greatest_le[OF that B])
   499     hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
   500 
   501     have "c dvd coeff a i" for i
   502     proof (induction i rule: nat_descend_induct[of "degree a"])
   503       case (base i)
   504       thus ?case by (simp add: coeff_eq_0)
   505     next
   506       case (descend i)
   507       let ?A = "{..i+m} - {i}"
   508       have "c dvd coeff (a * b) (i + m)" by (rule dvd)
   509       also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
   510         by (simp add: coeff_mult)
   511       also have "{..i+m} = insert i ?A" by auto
   512       also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
   513                    coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
   514         (is "_ = _ + ?S")
   515         by (subst sum.insert) simp_all
   516       finally have eq: "c dvd coeff a i * coeff b m + ?S" .
   517       moreover have "c dvd ?S"
   518       proof (rule dvd_sum)
   519         fix k assume k: "k \<in> {..i+m} - {i}"
   520         show "c dvd coeff a k * coeff b (i + m - k)"
   521         proof (cases "k < i")
   522           case False
   523           with k have "c dvd coeff a k" by (intro descend.IH) simp
   524           thus ?thesis by simp
   525         next
   526           case True
   527           hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
   528           thus ?thesis by simp
   529         qed
   530       qed
   531       ultimately have "c dvd coeff a i * coeff b m"
   532         by (simp add: dvd_add_left_iff)
   533       with assms coeff_m show "c dvd coeff a i"
   534         by (simp add: prime_elem_dvd_mult_iff)
   535     qed
   536     hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
   537   }
   538   thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
   539 qed (insert assms, simp_all add: prime_elem_def one_poly_def)
   540 
   541 lemma prime_elem_const_poly_iff:
   542   fixes c :: "'a :: semidom"
   543   shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
   544 proof
   545   assume A: "prime_elem [:c:]"
   546   show "prime_elem c"
   547   proof (rule prime_elemI)
   548     fix a b assume "c dvd a * b"
   549     hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
   550     from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
   551     thus "c dvd a \<or> c dvd b" by simp
   552   qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
   553 qed (auto intro: lift_prime_elem_poly)
   554 
   555 context
   556 begin
   557 
   558 private lemma content_1_mult:
   559   fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
   560   assumes "content f = 1" "content g = 1"
   561   shows   "content (f * g) = 1"
   562 proof (cases "f * g = 0")
   563   case False
   564   from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
   565 
   566   hence "f * g \<noteq> 0" by auto
   567   {
   568     assume "\<not>is_unit (content (f * g))"
   569     with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
   570       by (intro prime_divisor_exists) simp_all
   571     then obtain p where "p dvd content (f * g)" "prime p" by blast
   572     from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
   573       by (simp add: const_poly_dvd_iff_dvd_content)
   574     moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
   575     ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
   576       by (simp add: prime_elem_dvd_mult_iff)
   577     with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
   578     with \<open>prime p\<close> have False by simp
   579   }
   580   hence "is_unit (content (f * g))" by blast
   581   hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
   582   thus ?thesis by simp
   583 qed (insert assms, auto)
   584 
   585 lemma content_mult:
   586   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   587   shows "content (p * q) = content p * content q"
   588 proof -
   589   from content_decompose[of p] guess p' . note p = this
   590   from content_decompose[of q] guess q' . note q = this
   591   have "content (p * q) = content p * content q * content (p' * q')"
   592     by (subst p, subst q) (simp add: mult_ac normalize_mult)
   593   also from p q have "content (p' * q') = 1" by (intro content_1_mult)
   594   finally show ?thesis by simp
   595 qed
   596 
   597 lemma primitive_part_mult:
   598   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   599   shows "primitive_part (p * q) = primitive_part p * primitive_part q"
   600 proof -
   601   have "primitive_part (p * q) = p * q div [:content (p * q):]"
   602     by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   603   also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
   604     by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
   605   also have "\<dots> = primitive_part p * primitive_part q"
   606     by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   607   finally show ?thesis .
   608 qed
   609 
   610 lemma primitive_part_smult:
   611   fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   612   shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
   613 proof -
   614   have "smult a p = [:a:] * p" by simp
   615   also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
   616     by (subst primitive_part_mult) simp_all
   617   finally show ?thesis .
   618 qed  
   619 
   620 lemma primitive_part_dvd_primitive_partI [intro]:
   621   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   622   shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
   623   by (auto elim!: dvdE simp: primitive_part_mult)
   624 
   625 lemma content_prod_mset: 
   626   fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
   627   shows "content (prod_mset A) = prod_mset (image_mset content A)"
   628   by (induction A) (simp_all add: content_mult mult_ac)
   629 
   630 lemma fract_poly_dvdD:
   631   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   632   assumes "fract_poly p dvd fract_poly q" "content p = 1"
   633   shows   "p dvd q"
   634 proof -
   635   from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
   636   from content_decompose_fract[of r] guess c r' . note r' = this
   637   from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
   638   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
   639   have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
   640   hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
   641   have "1 = gcd a (normalize b)" by (simp add: ab)
   642   also note eq'
   643   also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
   644   finally have [simp]: "a = 1" by simp
   645   from eq ab have "q = p * ([:b:] * r')" by simp
   646   thus ?thesis by (rule dvdI)
   647 qed
   648 
   649 lemma content_prod_eq_1_iff: 
   650   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   651   shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
   652 proof safe
   653   assume A: "content (p * q) = 1"
   654   {
   655     fix p q :: "'a poly" assume "content p * content q = 1"
   656     hence "1 = content p * content q" by simp
   657     hence "content p dvd 1" by (rule dvdI)
   658     hence "content p = 1" by simp
   659   } note B = this
   660   from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
   661     by (simp_all add: content_mult mult_ac)
   662 qed (auto simp: content_mult)
   663 
   664 end
   665 
   666 
   667 subsection \<open>Polynomials over a field are a Euclidean ring\<close>
   668 
   669 definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
   670   "unit_factor_field_poly p = [:lead_coeff p:]"
   671 
   672 definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
   673   "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
   674 
   675 definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
   676   "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
   677 
   678 lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
   679   by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
   680 
   681 interpretation field_poly: 
   682   unique_euclidean_ring where zero = "0 :: 'a :: field poly"
   683     and one = 1 and plus = plus and uminus = uminus and minus = minus
   684     and times = times
   685     and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
   686     and euclidean_size = euclidean_size_field_poly
   687     and uniqueness_constraint = top
   688     and divide = divide and modulo = modulo
   689 proof (standard, unfold dvd_field_poly)
   690   fix p :: "'a poly"
   691   show "unit_factor_field_poly p * normalize_field_poly p = p"
   692     by (cases "p = 0") 
   693        (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
   694 next
   695   fix p :: "'a poly" assume "is_unit p"
   696   thus "normalize_field_poly p = 1"
   697     by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
   698 next
   699   fix p :: "'a poly" assume "p \<noteq> 0"
   700   thus "is_unit (unit_factor_field_poly p)"
   701     by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
   702 next
   703   fix p q s :: "'a poly" assume "s \<noteq> 0"
   704   moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q"
   705   ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)"
   706     by (auto simp add: euclidean_size_field_poly_def degree_mult_eq)
   707 next
   708   fix p q r :: "'a poly" assume "p \<noteq> 0"
   709   moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p"
   710   ultimately show "(q * p + r) div p = q"
   711     by (cases "r = 0")
   712       (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less)
   713 qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
   714        euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
   715 
   716 lemma field_poly_irreducible_imp_prime:
   717   assumes "irreducible (p :: 'a :: field poly)"
   718   shows   "prime_elem p"
   719 proof -
   720   have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   721   from field_poly.irreducible_imp_prime_elem[of p] assms
   722     show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
   723       comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
   724 qed
   725 
   726 lemma field_poly_prod_mset_prime_factorization:
   727   assumes "(x :: 'a :: field poly) \<noteq> 0"
   728   shows   "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x"
   729 proof -
   730   have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
   731   have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset"
   732     by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def)
   733   with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp
   734 qed
   735 
   736 lemma field_poly_in_prime_factorization_imp_prime:
   737   assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
   738   shows   "prime_elem p"
   739 proof -
   740   have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   741   have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
   742              normalize_field_poly unit_factor_field_poly" ..
   743   from field_poly.in_prime_factors_imp_prime [of p x] assms
   744     show ?thesis unfolding prime_elem_def dvd_field_poly
   745       comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
   746 qed
   747 
   748 
   749 subsection \<open>Primality and irreducibility in polynomial rings\<close>
   750 
   751 lemma nonconst_poly_irreducible_iff:
   752   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   753   assumes "degree p \<noteq> 0"
   754   shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
   755 proof safe
   756   assume p: "irreducible p"
   757 
   758   from content_decompose[of p] guess p' . note p' = this
   759   hence "p = [:content p:] * p'" by simp
   760   from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
   761   moreover have "\<not>p' dvd 1"
   762   proof
   763     assume "p' dvd 1"
   764     hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
   765     with assms show False by contradiction
   766   qed
   767   ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
   768   
   769   show "irreducible (map_poly to_fract p)"
   770   proof (rule irreducibleI)
   771     have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
   772     with assms show "map_poly to_fract p \<noteq> 0" by auto
   773   next
   774     show "\<not>is_unit (fract_poly p)"
   775     proof
   776       assume "is_unit (map_poly to_fract p)"
   777       hence "degree (map_poly to_fract p) = 0"
   778         by (auto simp: is_unit_poly_iff)
   779       hence "degree p = 0" by (simp add: degree_map_poly)
   780       with assms show False by contradiction
   781    qed
   782  next
   783    fix q r assume qr: "fract_poly p = q * r"
   784    from content_decompose_fract[of q] guess cg q' . note q = this
   785    from content_decompose_fract[of r] guess cr r' . note r = this
   786    from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
   787    from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
   788      by (simp add: q r)
   789    from fract_poly_smult_eqE[OF this] guess a b . note ab = this
   790    hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
   791    with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
   792    hence "normalize b = gcd a b" by simp
   793    also from ab(3) have "\<dots> = 1" .
   794    finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
   795    
   796    note eq
   797    also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
   798    also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
   799    finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
   800    from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
   801    hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
   802    hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
   803    with q r show "is_unit q \<or> is_unit r"
   804      by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
   805  qed
   806 
   807 next
   808 
   809   assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
   810   show "irreducible p"
   811   proof (rule irreducibleI)
   812     from irred show "p \<noteq> 0" by auto
   813   next
   814     from irred show "\<not>p dvd 1"
   815       by (auto simp: irreducible_def dest: fract_poly_is_unit)
   816   next
   817     fix q r assume qr: "p = q * r"
   818     hence "fract_poly p = fract_poly q * fract_poly r" by simp
   819     from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
   820       by (rule irreducibleD)
   821     with primitive qr show "q dvd 1 \<or> r dvd 1"
   822       by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
   823   qed
   824 qed
   825 
   826 context
   827 begin
   828 
   829 private lemma irreducible_imp_prime_poly:
   830   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   831   assumes "irreducible p"
   832   shows   "prime_elem p"
   833 proof (cases "degree p = 0")
   834   case True
   835   with assms show ?thesis
   836     by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
   837              intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
   838 next
   839   case False
   840   from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
   841     by (simp_all add: nonconst_poly_irreducible_iff)
   842   from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
   843   show ?thesis
   844   proof (rule prime_elemI)
   845     fix q r assume "p dvd q * r"
   846     hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
   847     hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
   848     from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
   849       by (rule prime_elem_dvd_multD)
   850     with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
   851   qed (insert assms, auto simp: irreducible_def)
   852 qed
   853 
   854 
   855 lemma degree_primitive_part_fract [simp]:
   856   "degree (primitive_part_fract p) = degree p"
   857 proof -
   858   have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
   859     by (simp add: content_times_primitive_part_fract)
   860   also have "degree \<dots> = degree (primitive_part_fract p)"
   861     by (auto simp: degree_map_poly)
   862   finally show ?thesis ..
   863 qed
   864 
   865 lemma irreducible_primitive_part_fract:
   866   fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
   867   assumes "irreducible p"
   868   shows   "irreducible (primitive_part_fract p)"
   869 proof -
   870   from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
   871     by (intro notI) 
   872        (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
   873   hence [simp]: "p \<noteq> 0" by auto
   874 
   875   note \<open>irreducible p\<close>
   876   also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
   877     by (simp add: content_times_primitive_part_fract)
   878   also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
   879     by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
   880   finally show ?thesis using deg
   881     by (simp add: nonconst_poly_irreducible_iff)
   882 qed
   883 
   884 lemma prime_elem_primitive_part_fract:
   885   fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
   886   shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
   887   by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
   888 
   889 lemma irreducible_linear_field_poly:
   890   fixes a b :: "'a::field"
   891   assumes "b \<noteq> 0"
   892   shows "irreducible [:a,b:]"
   893 proof (rule irreducibleI)
   894   fix p q assume pq: "[:a,b:] = p * q"
   895   also from pq assms have "degree \<dots> = degree p + degree q" 
   896     by (intro degree_mult_eq) auto
   897   finally have "degree p = 0 \<or> degree q = 0" using assms by auto
   898   with assms pq show "is_unit p \<or> is_unit q"
   899     by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
   900 qed (insert assms, auto simp: is_unit_poly_iff)
   901 
   902 lemma prime_elem_linear_field_poly:
   903   "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
   904   by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
   905 
   906 lemma irreducible_linear_poly:
   907   fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
   908   shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
   909   by (auto intro!: irreducible_linear_field_poly 
   910            simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
   911 
   912 lemma prime_elem_linear_poly:
   913   fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
   914   shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
   915   by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
   916 
   917 end
   918 
   919  
   920 subsection \<open>Prime factorisation of polynomials\<close>   
   921 
   922 context
   923 begin 
   924 
   925 private lemma poly_prime_factorization_exists_content_1:
   926   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   927   assumes "p \<noteq> 0" "content p = 1"
   928   shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
   929 proof -
   930   let ?P = "field_poly.prime_factorization (fract_poly p)"
   931   define c where "c = prod_mset (image_mset fract_content ?P)"
   932   define c' where "c' = c * to_fract (lead_coeff p)"
   933   define e where "e = prod_mset (image_mset primitive_part_fract ?P)"
   934   define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
   935   have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
   936                       content (primitive_part_fract x))"
   937     by (simp add: e_def content_prod_mset multiset.map_comp o_def)
   938   also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
   939     by (intro image_mset_cong content_primitive_part_fract) auto
   940   finally have content_e: "content e = 1"
   941     by simp    
   942   
   943   have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
   944           normalize_field_poly (fract_poly p)" by simp
   945   also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
   946     by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
   947   also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
   948     by (subst field_poly_prod_mset_prime_factorization) simp_all
   949   also have "\<dots> = prod_mset (image_mset id ?P)" by simp
   950   also have "image_mset id ?P = 
   951                image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
   952     by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
   953   also have "prod_mset \<dots> = smult c (fract_poly e)"
   954     by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
   955   also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
   956     by (simp add: c'_def)
   957   finally have eq: "fract_poly p = smult c' (fract_poly e)" .
   958   also obtain b where b: "c' = to_fract b" "is_unit b"
   959   proof -
   960     from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
   961     from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
   962     with assms content_e have "a = normalize b" by (simp add: ab(4))
   963     with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
   964     with ab ab' have "c' = to_fract b" by auto
   965     from this and \<open>is_unit b\<close> show ?thesis by (rule that)
   966   qed
   967   hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
   968   finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
   969   hence "p = [:b:] * e" by simp
   970   with b have "normalize p = normalize e" 
   971     by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
   972   also have "normalize e = prod_mset A"
   973     by (simp add: multiset.map_comp e_def A_def normalize_prod_mset)
   974   finally have "prod_mset A = normalize p" ..
   975   
   976   have "prime_elem p" if "p \<in># A" for p
   977     using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
   978                         dest!: field_poly_in_prime_factorization_imp_prime )
   979   from this and \<open>prod_mset A = normalize p\<close> show ?thesis
   980     by (intro exI[of _ A]) blast
   981 qed
   982 
   983 lemma poly_prime_factorization_exists:
   984   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   985   assumes "p \<noteq> 0"
   986   shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
   987 proof -
   988   define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
   989   have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
   990     by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
   991   then guess A by (elim exE conjE) note A = this
   992   moreover from assms have "prod_mset B = [:content p:]"
   993     by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
   994   moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
   995     by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
   996   ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
   997 qed
   998 
   999 end
  1000 
  1001 
  1002 subsection \<open>Typeclass instances\<close>
  1003 
  1004 instance poly :: (factorial_ring_gcd) factorial_semiring
  1005   by standard (rule poly_prime_factorization_exists)  
  1006 
  1007 instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
  1008 begin
  1009 
  1010 definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1011   [code del]: "gcd_poly = gcd_factorial"
  1012 
  1013 definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1014   [code del]: "lcm_poly = lcm_factorial"
  1015   
  1016 definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
  1017  [code del]: "Gcd_poly = Gcd_factorial"
  1018 
  1019 definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
  1020  [code del]: "Lcm_poly = Lcm_factorial"
  1021  
  1022 instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
  1023 
  1024 end
  1025 
  1026 instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
  1027 begin
  1028 
  1029 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
  1030   where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
  1031 
  1032 definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
  1033   where [simp]: "uniqueness_constraint_poly = top"
  1034 
  1035 instance 
  1036   by standard
  1037    (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
  1038     split: if_splits)
  1039 
  1040 end
  1041 
  1042 instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
  1043   by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI)
  1044     standard
  1045 
  1046   
  1047 subsection \<open>Polynomial GCD\<close>
  1048 
  1049 lemma gcd_poly_decompose:
  1050   fixes p q :: "'a :: factorial_ring_gcd poly"
  1051   shows "gcd p q = 
  1052            smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  1053 proof (rule sym, rule gcdI)
  1054   have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  1055           [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
  1056   thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
  1057     by simp
  1058 next
  1059   have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  1060           [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
  1061   thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
  1062     by simp
  1063 next
  1064   fix d assume "d dvd p" "d dvd q"
  1065   hence "[:content d:] * primitive_part d dvd 
  1066            [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
  1067     by (intro mult_dvd_mono) auto
  1068   thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  1069     by simp
  1070 qed (auto simp: normalize_smult)
  1071   
  1072 
  1073 lemma gcd_poly_pseudo_mod:
  1074   fixes p q :: "'a :: factorial_ring_gcd poly"
  1075   assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
  1076   shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
  1077 proof -
  1078   define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
  1079   define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
  1080   have [simp]: "primitive_part a = unit_factor a"
  1081     by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
  1082   from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
  1083   
  1084   have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
  1085   have "gcd (q * r + s) q = gcd q s"
  1086     using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
  1087   with pseudo_divmod(1)[OF nz rs]
  1088     have "gcd (p * a) q = gcd q s" by (simp add: a_def)
  1089   also from prim have "gcd (p * a) q = gcd p q"
  1090     by (subst gcd_poly_decompose)
  1091        (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
  1092              simp del: mult_pCons_right )
  1093   also from prim have "gcd q s = gcd q (primitive_part s)"
  1094     by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
  1095   also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
  1096   finally show ?thesis .
  1097 qed
  1098 
  1099 lemma degree_pseudo_mod_less:
  1100   assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
  1101   shows   "degree (pseudo_mod p q) < degree q"
  1102   using pseudo_mod(2)[of q p] assms by auto
  1103 
  1104 function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1105   "gcd_poly_code_aux p q = 
  1106      (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
  1107 by auto
  1108 termination
  1109   by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
  1110      (auto simp: degree_pseudo_mod_less)
  1111 
  1112 declare gcd_poly_code_aux.simps [simp del]
  1113 
  1114 lemma gcd_poly_code_aux_correct:
  1115   assumes "content p = 1" "q = 0 \<or> content q = 1"
  1116   shows   "gcd_poly_code_aux p q = gcd p q"
  1117   using assms
  1118 proof (induction p q rule: gcd_poly_code_aux.induct)
  1119   case (1 p q)
  1120   show ?case
  1121   proof (cases "q = 0")
  1122     case True
  1123     thus ?thesis by (subst gcd_poly_code_aux.simps) auto
  1124   next
  1125     case False
  1126     hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
  1127       by (subst gcd_poly_code_aux.simps) simp_all
  1128     also from "1.prems" False 
  1129       have "primitive_part (pseudo_mod p q) = 0 \<or> 
  1130               content (primitive_part (pseudo_mod p q)) = 1"
  1131       by (cases "pseudo_mod p q = 0") auto
  1132     with "1.prems" False 
  1133       have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
  1134               gcd q (primitive_part (pseudo_mod p q))"
  1135       by (intro 1) simp_all
  1136     also from "1.prems" False 
  1137       have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
  1138     finally show ?thesis .
  1139   qed
  1140 qed
  1141 
  1142 definition gcd_poly_code 
  1143     :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
  1144   where "gcd_poly_code p q = 
  1145            (if p = 0 then normalize q else if q = 0 then normalize p else
  1146               smult (gcd (content p) (content q)) 
  1147                 (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
  1148 
  1149 lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
  1150   by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
  1151 
  1152 lemma lcm_poly_code [code]: 
  1153   fixes p q :: "'a :: factorial_ring_gcd poly"
  1154   shows "lcm p q = normalize (p * q) div gcd p q"
  1155   by (fact lcm_gcd)
  1156 
  1157 declare Gcd_set
  1158   [where ?'a = "'a :: factorial_ring_gcd poly", code]
  1159 
  1160 declare Lcm_set
  1161   [where ?'a = "'a :: factorial_ring_gcd poly", code]
  1162 
  1163 text \<open>Example:
  1164   @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
  1165 \<close>
  1166   
  1167 end