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