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