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