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