Polynomial algebra cleanup
authoreberlm <eberlm@in.tum.de>
Tue Aug 16 12:02:09 2016 +0200 (2016-08-16)
changeset 637046209c06d776f
parent 63703 ec095a532a2b
child 63705 7d371a18b6a2
Polynomial algebra cleanup
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Library/Polynomial_GCD_euclidean.thy
src/HOL/Number_Theory/Polynomial_Factorial.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Aug 14 23:35:16 2016 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Aug 16 12:02:09 2016 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    "~~/src/HOL/Library/Library"
     1.5    "~~/src/HOL/Library/Sublist_Order"
     1.6    "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
     1.7 -  "~~/src/HOL/Number_Theory/Polynomial_Factorial"
     1.8 +  "~~/src/HOL/Library/Polynomial_Factorial"
     1.9    "~~/src/HOL/Data_Structures/Tree_Map"
    1.10    "~~/src/HOL/Data_Structures/Tree_Set"
    1.11    "~~/src/HOL/Number_Theory/Eratosthenes"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Tue Aug 16 12:02:09 2016 +0200
     2.3 @@ -0,0 +1,1468 @@
     2.4 +theory Polynomial_Factorial
     2.5 +imports 
     2.6 +  Complex_Main
     2.7 +  Euclidean_Algorithm 
     2.8 +  "~~/src/HOL/Library/Polynomial"
     2.9 +  "~~/src/HOL/Library/Normalized_Fraction"
    2.10 +begin
    2.11 +
    2.12 +subsection \<open>Prelude\<close>
    2.13 +
    2.14 +lemma msetprod_mult: 
    2.15 +  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
    2.16 +  by (induction A) (simp_all add: mult_ac)
    2.17 +  
    2.18 +lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
    2.19 +  by (induction A) (simp_all add: mult_ac)
    2.20 +  
    2.21 +lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
    2.22 +proof safe
    2.23 +  assume "x \<noteq> 0"
    2.24 +  hence "y = x * (y / x)" by (simp add: field_simps)
    2.25 +  thus "x dvd y" by (rule dvdI)
    2.26 +qed auto
    2.27 +
    2.28 +lemma nat_descend_induct [case_names base descend]:
    2.29 +  assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
    2.30 +  assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
    2.31 +  shows   "P m"
    2.32 +  using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
    2.33 +
    2.34 +lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
    2.35 +  by (metis GreatestI)
    2.36 +
    2.37 +
    2.38 +context field
    2.39 +begin
    2.40 +
    2.41 +subclass idom_divide ..
    2.42 +
    2.43 +end
    2.44 +
    2.45 +context field
    2.46 +begin
    2.47 +
    2.48 +definition normalize_field :: "'a \<Rightarrow> 'a" 
    2.49 +  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
    2.50 +definition unit_factor_field :: "'a \<Rightarrow> 'a" 
    2.51 +  where [simp]: "unit_factor_field x = x"
    2.52 +definition euclidean_size_field :: "'a \<Rightarrow> nat" 
    2.53 +  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
    2.54 +definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.55 +  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
    2.56 +
    2.57 +end
    2.58 +
    2.59 +instantiation real :: euclidean_ring
    2.60 +begin
    2.61 +
    2.62 +definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    2.63 +definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    2.64 +definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    2.65 +definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
    2.66 +
    2.67 +instance by standard (simp_all add: dvd_field_iff divide_simps)
    2.68 +end
    2.69 +
    2.70 +instantiation real :: euclidean_ring_gcd
    2.71 +begin
    2.72 +
    2.73 +definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    2.74 +  "gcd_real = gcd_eucl"
    2.75 +definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    2.76 +  "lcm_real = lcm_eucl"
    2.77 +definition Gcd_real :: "real set \<Rightarrow> real" where
    2.78 + "Gcd_real = Gcd_eucl"
    2.79 +definition Lcm_real :: "real set \<Rightarrow> real" where
    2.80 + "Lcm_real = Lcm_eucl"
    2.81 +
    2.82 +instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    2.83 +
    2.84 +end
    2.85 +
    2.86 +instantiation rat :: euclidean_ring
    2.87 +begin
    2.88 +
    2.89 +definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    2.90 +definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    2.91 +definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    2.92 +definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
    2.93 +
    2.94 +instance by standard (simp_all add: dvd_field_iff divide_simps)
    2.95 +end
    2.96 +
    2.97 +instantiation rat :: euclidean_ring_gcd
    2.98 +begin
    2.99 +
   2.100 +definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   2.101 +  "gcd_rat = gcd_eucl"
   2.102 +definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   2.103 +  "lcm_rat = lcm_eucl"
   2.104 +definition Gcd_rat :: "rat set \<Rightarrow> rat" where
   2.105 + "Gcd_rat = Gcd_eucl"
   2.106 +definition Lcm_rat :: "rat set \<Rightarrow> rat" where
   2.107 + "Lcm_rat = Lcm_eucl"
   2.108 +
   2.109 +instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
   2.110 +
   2.111 +end
   2.112 +
   2.113 +instantiation complex :: euclidean_ring
   2.114 +begin
   2.115 +
   2.116 +definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
   2.117 +definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
   2.118 +definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
   2.119 +definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
   2.120 +
   2.121 +instance by standard (simp_all add: dvd_field_iff divide_simps)
   2.122 +end
   2.123 +
   2.124 +instantiation complex :: euclidean_ring_gcd
   2.125 +begin
   2.126 +
   2.127 +definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   2.128 +  "gcd_complex = gcd_eucl"
   2.129 +definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   2.130 +  "lcm_complex = lcm_eucl"
   2.131 +definition Gcd_complex :: "complex set \<Rightarrow> complex" where
   2.132 + "Gcd_complex = Gcd_eucl"
   2.133 +definition Lcm_complex :: "complex set \<Rightarrow> complex" where
   2.134 + "Lcm_complex = Lcm_eucl"
   2.135 +
   2.136 +instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
   2.137 +
   2.138 +end
   2.139 +
   2.140 +
   2.141 +
   2.142 +subsection \<open>Lifting elements into the field of fractions\<close>
   2.143 +
   2.144 +definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
   2.145 +
   2.146 +lemma to_fract_0 [simp]: "to_fract 0 = 0"
   2.147 +  by (simp add: to_fract_def eq_fract Zero_fract_def)
   2.148 +
   2.149 +lemma to_fract_1 [simp]: "to_fract 1 = 1"
   2.150 +  by (simp add: to_fract_def eq_fract One_fract_def)
   2.151 +
   2.152 +lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
   2.153 +  by (simp add: to_fract_def)
   2.154 +
   2.155 +lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
   2.156 +  by (simp add: to_fract_def)
   2.157 +  
   2.158 +lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
   2.159 +  by (simp add: to_fract_def)
   2.160 +  
   2.161 +lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
   2.162 +  by (simp add: to_fract_def)
   2.163 +
   2.164 +lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
   2.165 +  by (simp add: to_fract_def eq_fract)
   2.166 +  
   2.167 +lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
   2.168 +  by (simp add: to_fract_def Zero_fract_def eq_fract)
   2.169 +
   2.170 +lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
   2.171 +  by transfer simp
   2.172 +
   2.173 +lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
   2.174 +  by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
   2.175 +
   2.176 +lemma to_fract_quot_of_fract:
   2.177 +  assumes "snd (quot_of_fract x) = 1"
   2.178 +  shows   "to_fract (fst (quot_of_fract x)) = x"
   2.179 +proof -
   2.180 +  have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
   2.181 +  also note assms
   2.182 +  finally show ?thesis by (simp add: to_fract_def)
   2.183 +qed
   2.184 +
   2.185 +lemma snd_quot_of_fract_Fract_whole:
   2.186 +  assumes "y dvd x"
   2.187 +  shows   "snd (quot_of_fract (Fract x y)) = 1"
   2.188 +  using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
   2.189 +  
   2.190 +lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
   2.191 +  by (simp add: to_fract_def)
   2.192 +
   2.193 +lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
   2.194 +  unfolding to_fract_def by transfer (simp add: normalize_quot_def)
   2.195 +
   2.196 +lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
   2.197 +  by transfer simp
   2.198 + 
   2.199 +lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
   2.200 +  unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
   2.201 +
   2.202 +lemma coprime_quot_of_fract:
   2.203 +  "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
   2.204 +  by transfer (simp add: coprime_normalize_quot)
   2.205 +
   2.206 +lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
   2.207 +  using quot_of_fract_in_normalized_fracts[of x] 
   2.208 +  by (simp add: normalized_fracts_def case_prod_unfold)  
   2.209 +
   2.210 +lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
   2.211 +  by (subst (2) normalize_mult_unit_factor [symmetric, of x])
   2.212 +     (simp del: normalize_mult_unit_factor)
   2.213 +  
   2.214 +lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
   2.215 +  by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
   2.216 +
   2.217 +  
   2.218 +subsection \<open>Mapping polynomials\<close>
   2.219 +
   2.220 +definition map_poly 
   2.221 +     :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
   2.222 +  "map_poly f p = Poly (map f (coeffs p))"
   2.223 +
   2.224 +lemma map_poly_0 [simp]: "map_poly f 0 = 0"
   2.225 +  by (simp add: map_poly_def)
   2.226 +
   2.227 +lemma map_poly_1: "map_poly f 1 = [:f 1:]"
   2.228 +  by (simp add: map_poly_def)
   2.229 +
   2.230 +lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
   2.231 +  by (simp add: map_poly_def one_poly_def)
   2.232 +
   2.233 +lemma coeff_map_poly:
   2.234 +  assumes "f 0 = 0"
   2.235 +  shows   "coeff (map_poly f p) n = f (coeff p n)"
   2.236 +  by (auto simp: map_poly_def nth_default_def coeffs_def assms
   2.237 +        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
   2.238 +
   2.239 +lemma coeffs_map_poly [code abstract]: 
   2.240 +    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
   2.241 +  by (simp add: map_poly_def)
   2.242 +
   2.243 +lemma set_coeffs_map_poly:
   2.244 +  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
   2.245 +  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
   2.246 +
   2.247 +lemma coeffs_map_poly': 
   2.248 +  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
   2.249 +  shows   "coeffs (map_poly f p) = map f (coeffs p)"
   2.250 +  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
   2.251 +                           intro!: strip_while_not_last split: if_splits)
   2.252 +
   2.253 +lemma degree_map_poly:
   2.254 +  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   2.255 +  shows   "degree (map_poly f p) = degree p"
   2.256 +  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
   2.257 +
   2.258 +lemma map_poly_eq_0_iff:
   2.259 +  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   2.260 +  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
   2.261 +proof -
   2.262 +  {
   2.263 +    fix n :: nat
   2.264 +    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
   2.265 +    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
   2.266 +    proof (cases "n < length (coeffs p)")
   2.267 +      case True
   2.268 +      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
   2.269 +      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
   2.270 +    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
   2.271 +    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
   2.272 +  }
   2.273 +  thus ?thesis by (auto simp: poly_eq_iff)
   2.274 +qed
   2.275 +
   2.276 +lemma map_poly_smult:
   2.277 +  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
   2.278 +  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
   2.279 +  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
   2.280 +
   2.281 +lemma map_poly_pCons:
   2.282 +  assumes "f 0 = 0"
   2.283 +  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
   2.284 +  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
   2.285 +
   2.286 +lemma map_poly_map_poly:
   2.287 +  assumes "f 0 = 0" "g 0 = 0"
   2.288 +  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
   2.289 +  by (intro poly_eqI) (simp add: coeff_map_poly assms)
   2.290 +
   2.291 +lemma map_poly_id [simp]: "map_poly id p = p"
   2.292 +  by (simp add: map_poly_def)
   2.293 +
   2.294 +lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
   2.295 +  by (simp add: map_poly_def)
   2.296 +
   2.297 +lemma map_poly_cong: 
   2.298 +  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
   2.299 +  shows   "map_poly f p = map_poly g p"
   2.300 +proof -
   2.301 +  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
   2.302 +  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
   2.303 +qed
   2.304 +
   2.305 +lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
   2.306 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   2.307 +
   2.308 +lemma map_poly_idI:
   2.309 +  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   2.310 +  shows   "map_poly f p = p"
   2.311 +  using map_poly_cong[OF assms, of _ id] by simp
   2.312 +
   2.313 +lemma map_poly_idI':
   2.314 +  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   2.315 +  shows   "p = map_poly f p"
   2.316 +  using map_poly_cong[OF assms, of _ id] by simp
   2.317 +
   2.318 +lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
   2.319 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   2.320 +
   2.321 +lemma div_const_poly_conv_map_poly: 
   2.322 +  assumes "[:c:] dvd p"
   2.323 +  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
   2.324 +proof (cases "c = 0")
   2.325 +  case False
   2.326 +  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   2.327 +  moreover {
   2.328 +    have "smult c q = [:c:] * q" by simp
   2.329 +    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
   2.330 +    finally have "smult c q div [:c:] = q" .
   2.331 +  }
   2.332 +  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
   2.333 +qed (auto intro!: poly_eqI simp: coeff_map_poly)
   2.334 +
   2.335 +
   2.336 +
   2.337 +subsection \<open>Various facts about polynomials\<close>
   2.338 +
   2.339 +lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
   2.340 +  by (induction A) (simp_all add: one_poly_def mult_ac)
   2.341 +
   2.342 +lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
   2.343 +  using degree_mod_less[of b a] by auto
   2.344 +  
   2.345 +lemma is_unit_const_poly_iff: 
   2.346 +    "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
   2.347 +  by (auto simp: one_poly_def)
   2.348 +
   2.349 +lemma is_unit_poly_iff:
   2.350 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   2.351 +  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
   2.352 +proof safe
   2.353 +  assume "p dvd 1"
   2.354 +  then obtain q where pq: "1 = p * q" by (erule dvdE)
   2.355 +  hence "degree 1 = degree (p * q)" by simp
   2.356 +  also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
   2.357 +  finally have "degree p = 0" by simp
   2.358 +  from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
   2.359 +  with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
   2.360 +    by (auto simp: is_unit_const_poly_iff)
   2.361 +qed (auto simp: is_unit_const_poly_iff)
   2.362 +
   2.363 +lemma is_unit_polyE:
   2.364 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   2.365 +  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
   2.366 +  using assms by (subst (asm) is_unit_poly_iff) blast
   2.367 +
   2.368 +lemma smult_eq_iff:
   2.369 +  assumes "(b :: 'a :: field) \<noteq> 0"
   2.370 +  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   2.371 +proof
   2.372 +  assume "smult a p = smult b q"
   2.373 +  also from assms have "smult (inverse b) \<dots> = q" by simp
   2.374 +  finally show "smult (a / b) p = q" by (simp add: field_simps)
   2.375 +qed (insert assms, auto)
   2.376 +
   2.377 +lemma irreducible_const_poly_iff:
   2.378 +  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   2.379 +  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
   2.380 +proof
   2.381 +  assume A: "irreducible c"
   2.382 +  show "irreducible [:c:]"
   2.383 +  proof (rule irreducibleI)
   2.384 +    fix a b assume ab: "[:c:] = a * b"
   2.385 +    hence "degree [:c:] = degree (a * b)" by (simp only: )
   2.386 +    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
   2.387 +    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
   2.388 +    finally have "degree a = 0" "degree b = 0" by auto
   2.389 +    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
   2.390 +    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
   2.391 +    hence "c = a' * b'" by (simp add: ab' mult_ac)
   2.392 +    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
   2.393 +    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
   2.394 +  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
   2.395 +next
   2.396 +  assume A: "irreducible [:c:]"
   2.397 +  show "irreducible c"
   2.398 +  proof (rule irreducibleI)
   2.399 +    fix a b assume ab: "c = a * b"
   2.400 +    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
   2.401 +    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
   2.402 +    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
   2.403 +  qed (insert A, auto simp: irreducible_def one_poly_def)
   2.404 +qed
   2.405 +
   2.406 +lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   2.407 +  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
   2.408 +
   2.409 +  
   2.410 +subsection \<open>Normalisation of polynomials\<close>
   2.411 +
   2.412 +instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
   2.413 +begin
   2.414 +
   2.415 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   2.416 +  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
   2.417 +
   2.418 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
   2.419 +  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   2.420 +
   2.421 +lemma normalize_poly_altdef:
   2.422 +  "normalize p = p div [:unit_factor (lead_coeff p):]"
   2.423 +proof (cases "p = 0")
   2.424 +  case False
   2.425 +  thus ?thesis
   2.426 +    by (subst div_const_poly_conv_map_poly)
   2.427 +       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
   2.428 +qed (auto simp: normalize_poly_def)
   2.429 +
   2.430 +instance
   2.431 +proof
   2.432 +  fix p :: "'a poly"
   2.433 +  show "unit_factor p * normalize p = p"
   2.434 +    by (cases "p = 0")
   2.435 +       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
   2.436 +          smult_conv_map_poly map_poly_map_poly o_def)
   2.437 +next
   2.438 +  fix p :: "'a poly"
   2.439 +  assume "is_unit p"
   2.440 +  then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
   2.441 +  thus "normalize p = 1"
   2.442 +    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
   2.443 +next
   2.444 +  fix p :: "'a poly" assume "p \<noteq> 0"
   2.445 +  thus "is_unit (unit_factor p)"
   2.446 +    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
   2.447 +qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
   2.448 +
   2.449 +end
   2.450 +
   2.451 +lemma unit_factor_pCons:
   2.452 +  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   2.453 +  by (simp add: unit_factor_poly_def)
   2.454 +
   2.455 +lemma normalize_monom [simp]:
   2.456 +  "normalize (monom a n) = monom (normalize a) n"
   2.457 +  by (simp add: map_poly_monom normalize_poly_def)
   2.458 +
   2.459 +lemma unit_factor_monom [simp]:
   2.460 +  "unit_factor (monom a n) = monom (unit_factor a) 0"
   2.461 +  by (simp add: unit_factor_poly_def )
   2.462 +
   2.463 +lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   2.464 +  by (simp add: normalize_poly_def map_poly_pCons)
   2.465 +
   2.466 +lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   2.467 +proof -
   2.468 +  have "smult c p = [:c:] * p" by simp
   2.469 +  also have "normalize \<dots> = smult (normalize c) (normalize p)"
   2.470 +    by (subst normalize_mult) (simp add: normalize_const_poly)
   2.471 +  finally show ?thesis .
   2.472 +qed
   2.473 +
   2.474 +lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   2.475 +proof -
   2.476 +  have "smult c p = [:c:] * p" by simp
   2.477 +  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   2.478 +  proof safe
   2.479 +    assume A: "[:c:] * p dvd 1"
   2.480 +    thus "p dvd 1" by (rule dvd_mult_right)
   2.481 +    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
   2.482 +    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
   2.483 +    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
   2.484 +    also note B [symmetric]
   2.485 +    finally show "c dvd 1" by simp
   2.486 +  next
   2.487 +    assume "c dvd 1" "p dvd 1"
   2.488 +    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
   2.489 +    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
   2.490 +    hence "[:c:] dvd 1" by (rule dvdI)
   2.491 +    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
   2.492 +  qed
   2.493 +  finally show ?thesis .
   2.494 +qed
   2.495 +
   2.496 +
   2.497 +subsection \<open>Content and primitive part of a polynomial\<close>
   2.498 +
   2.499 +definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
   2.500 +  "content p = Gcd (set (coeffs p))"
   2.501 +
   2.502 +lemma content_0 [simp]: "content 0 = 0"
   2.503 +  by (simp add: content_def)
   2.504 +
   2.505 +lemma content_1 [simp]: "content 1 = 1"
   2.506 +  by (simp add: content_def)
   2.507 +
   2.508 +lemma content_const [simp]: "content [:c:] = normalize c"
   2.509 +  by (simp add: content_def cCons_def)
   2.510 +
   2.511 +lemma const_poly_dvd_iff_dvd_content:
   2.512 +  fixes c :: "'a :: semiring_Gcd"
   2.513 +  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
   2.514 +proof (cases "p = 0")
   2.515 +  case [simp]: False
   2.516 +  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
   2.517 +  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
   2.518 +  proof safe
   2.519 +    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
   2.520 +    thus "c dvd coeff p n"
   2.521 +      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
   2.522 +  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
   2.523 +  also have "\<dots> \<longleftrightarrow> c dvd content p"
   2.524 +    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
   2.525 +          dvd_mult_unit_iff lead_coeff_nonzero)
   2.526 +  finally show ?thesis .
   2.527 +qed simp_all
   2.528 +
   2.529 +lemma content_dvd [simp]: "[:content p:] dvd p"
   2.530 +  by (subst const_poly_dvd_iff_dvd_content) simp_all
   2.531 +  
   2.532 +lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
   2.533 +  by (cases "n \<le> degree p") 
   2.534 +     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
   2.535 +
   2.536 +lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
   2.537 +  by (simp add: content_def Gcd_dvd)
   2.538 +
   2.539 +lemma normalize_content [simp]: "normalize (content p) = content p"
   2.540 +  by (simp add: content_def)
   2.541 +
   2.542 +lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
   2.543 +proof
   2.544 +  assume "is_unit (content p)"
   2.545 +  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
   2.546 +  thus "content p = 1" by simp
   2.547 +qed auto
   2.548 +
   2.549 +lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
   2.550 +  by (simp add: content_def coeffs_smult Gcd_mult)
   2.551 +
   2.552 +lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   2.553 +  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
   2.554 +
   2.555 +definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
   2.556 +  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
   2.557 +  
   2.558 +lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
   2.559 +  by (simp add: primitive_part_def)
   2.560 +
   2.561 +lemma content_times_primitive_part [simp]:
   2.562 +  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
   2.563 +  shows "smult (content p) (primitive_part p) = p"
   2.564 +proof (cases "p = 0")
   2.565 +  case False
   2.566 +  thus ?thesis
   2.567 +  unfolding primitive_part_def
   2.568 +  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
   2.569 +           intro: map_poly_idI)
   2.570 +qed simp_all
   2.571 +
   2.572 +lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   2.573 +proof (cases "p = 0")
   2.574 +  case False
   2.575 +  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   2.576 +    by (simp add:  primitive_part_def)
   2.577 +  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   2.578 +    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   2.579 +  finally show ?thesis using False by simp
   2.580 +qed simp
   2.581 +
   2.582 +lemma content_primitive_part [simp]:
   2.583 +  assumes "p \<noteq> 0"
   2.584 +  shows   "content (primitive_part p) = 1"
   2.585 +proof -
   2.586 +  have "p = smult (content p) (primitive_part p)" by simp
   2.587 +  also have "content \<dots> = content p * content (primitive_part p)" 
   2.588 +    by (simp del: content_times_primitive_part)
   2.589 +  finally show ?thesis using assms by simp
   2.590 +qed
   2.591 +
   2.592 +lemma content_decompose:
   2.593 +  fixes p :: "'a :: semiring_Gcd poly"
   2.594 +  obtains p' where "p = smult (content p) p'" "content p' = 1"
   2.595 +proof (cases "p = 0")
   2.596 +  case True
   2.597 +  thus ?thesis by (intro that[of 1]) simp_all
   2.598 +next
   2.599 +  case False
   2.600 +  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
   2.601 +  have "content p * 1 = content p * content r" by (subst r) simp
   2.602 +  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
   2.603 +  with r show ?thesis by (intro that[of r]) simp_all
   2.604 +qed
   2.605 +
   2.606 +lemma smult_content_normalize_primitive_part [simp]:
   2.607 +  "smult (content p) (normalize (primitive_part p)) = normalize p"
   2.608 +proof -
   2.609 +  have "smult (content p) (normalize (primitive_part p)) = 
   2.610 +          normalize ([:content p:] * primitive_part p)" 
   2.611 +    by (subst normalize_mult) (simp_all add: normalize_const_poly)
   2.612 +  also have "[:content p:] * primitive_part p = p" by simp
   2.613 +  finally show ?thesis .
   2.614 +qed
   2.615 +
   2.616 +lemma content_dvd_contentI [intro]:
   2.617 +  "p dvd q \<Longrightarrow> content p dvd content q"
   2.618 +  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   2.619 +  
   2.620 +lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   2.621 +  by (simp add: primitive_part_def map_poly_pCons)
   2.622 + 
   2.623 +lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   2.624 +  by (auto simp: primitive_part_def)
   2.625 +  
   2.626 +lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   2.627 +proof (cases "p = 0")
   2.628 +  case False
   2.629 +  have "p = smult (content p) (primitive_part p)" by simp
   2.630 +  also from False have "degree \<dots> = degree (primitive_part p)"
   2.631 +    by (subst degree_smult_eq) simp_all
   2.632 +  finally show ?thesis ..
   2.633 +qed simp_all
   2.634 +
   2.635 +
   2.636 +subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
   2.637 +
   2.638 +abbreviation (input) fract_poly 
   2.639 +  where "fract_poly \<equiv> map_poly to_fract"
   2.640 +
   2.641 +abbreviation (input) unfract_poly 
   2.642 +  where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
   2.643 +  
   2.644 +lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
   2.645 +  by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
   2.646 +
   2.647 +lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
   2.648 +  by (simp add: poly_eqI coeff_map_poly)
   2.649 +
   2.650 +lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
   2.651 +  by (simp add: one_poly_def map_poly_pCons)
   2.652 +
   2.653 +lemma fract_poly_add [simp]:
   2.654 +  "fract_poly (p + q) = fract_poly p + fract_poly q"
   2.655 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   2.656 +
   2.657 +lemma fract_poly_diff [simp]:
   2.658 +  "fract_poly (p - q) = fract_poly p - fract_poly q"
   2.659 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   2.660 +
   2.661 +lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A"
   2.662 +  by (cases "finite A", induction A rule: finite_induct) simp_all 
   2.663 +
   2.664 +lemma fract_poly_mult [simp]:
   2.665 +  "fract_poly (p * q) = fract_poly p * fract_poly q"
   2.666 +  by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
   2.667 +
   2.668 +lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
   2.669 +  by (auto simp: poly_eq_iff coeff_map_poly)
   2.670 +
   2.671 +lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
   2.672 +  using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
   2.673 +
   2.674 +lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
   2.675 +  by (auto elim!: dvdE)
   2.676 +
   2.677 +lemma msetprod_fract_poly: 
   2.678 +  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
   2.679 +  by (induction A) (simp_all add: mult_ac)
   2.680 +  
   2.681 +lemma is_unit_fract_poly_iff:
   2.682 +  "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
   2.683 +proof safe
   2.684 +  assume A: "p dvd 1"
   2.685 +  with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
   2.686 +  from A show "content p = 1"
   2.687 +    by (auto simp: is_unit_poly_iff normalize_1_iff)
   2.688 +next
   2.689 +  assume A: "fract_poly p dvd 1" and B: "content p = 1"
   2.690 +  from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
   2.691 +  {
   2.692 +    fix n :: nat assume "n > 0"
   2.693 +    have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
   2.694 +    also note c
   2.695 +    also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
   2.696 +    finally have "coeff p n = 0" by simp
   2.697 +  }
   2.698 +  hence "degree p \<le> 0" by (intro degree_le) simp_all
   2.699 +  with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
   2.700 +qed
   2.701 +  
   2.702 +lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
   2.703 +  using fract_poly_dvd[of p 1] by simp
   2.704 +
   2.705 +lemma fract_poly_smult_eqE:
   2.706 +  fixes c :: "'a :: {idom_divide,ring_gcd} fract"
   2.707 +  assumes "fract_poly p = smult c (fract_poly q)"
   2.708 +  obtains a b 
   2.709 +    where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
   2.710 +proof -
   2.711 +  define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
   2.712 +  have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
   2.713 +    by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
   2.714 +  hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
   2.715 +  hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
   2.716 +  moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
   2.717 +    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
   2.718 +          normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
   2.719 +  ultimately show ?thesis by (intro that[of a b])
   2.720 +qed
   2.721 +
   2.722 +
   2.723 +subsection \<open>Fractional content\<close>
   2.724 +
   2.725 +abbreviation (input) Lcm_coeff_denoms 
   2.726 +    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
   2.727 +  where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
   2.728 +  
   2.729 +definition fract_content :: 
   2.730 +      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
   2.731 +  "fract_content p = 
   2.732 +     (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
   2.733 +
   2.734 +definition primitive_part_fract :: 
   2.735 +      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
   2.736 +  "primitive_part_fract p = 
   2.737 +     primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
   2.738 +
   2.739 +lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
   2.740 +  by (simp add: primitive_part_fract_def)
   2.741 +
   2.742 +lemma fract_content_eq_0_iff [simp]:
   2.743 +  "fract_content p = 0 \<longleftrightarrow> p = 0"
   2.744 +  unfolding fract_content_def Let_def Zero_fract_def
   2.745 +  by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
   2.746 +
   2.747 +lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
   2.748 +  unfolding primitive_part_fract_def
   2.749 +  by (rule content_primitive_part)
   2.750 +     (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
   2.751 +
   2.752 +lemma content_times_primitive_part_fract:
   2.753 +  "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
   2.754 +proof -
   2.755 +  define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
   2.756 +  have "fract_poly p' = 
   2.757 +          map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
   2.758 +    unfolding primitive_part_fract_def p'_def 
   2.759 +    by (subst map_poly_map_poly) (simp_all add: o_assoc)
   2.760 +  also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
   2.761 +  proof (intro map_poly_idI, unfold o_apply)
   2.762 +    fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
   2.763 +    then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
   2.764 +      by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
   2.765 +    note c(2)
   2.766 +    also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   2.767 +      by simp
   2.768 +    also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
   2.769 +                 Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   2.770 +      unfolding to_fract_def by (subst mult_fract) simp_all
   2.771 +    also have "snd (quot_of_fract \<dots>) = 1"
   2.772 +      by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
   2.773 +    finally show "to_fract (fst (quot_of_fract c)) = c"
   2.774 +      by (rule to_fract_quot_of_fract)
   2.775 +  qed
   2.776 +  also have "p' = smult (content p') (primitive_part p')" 
   2.777 +    by (rule content_times_primitive_part [symmetric])
   2.778 +  also have "primitive_part p' = primitive_part_fract p"
   2.779 +    by (simp add: primitive_part_fract_def p'_def)
   2.780 +  also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
   2.781 +               smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
   2.782 +  finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
   2.783 +                      smult (to_fract (Lcm_coeff_denoms p)) p" .
   2.784 +  thus ?thesis
   2.785 +    by (subst (asm) smult_eq_iff)
   2.786 +       (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
   2.787 +qed
   2.788 +
   2.789 +lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
   2.790 +proof -
   2.791 +  have "Lcm_coeff_denoms (fract_poly p) = 1"
   2.792 +    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
   2.793 +  hence "fract_content (fract_poly p) = 
   2.794 +           to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
   2.795 +    by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
   2.796 +  also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
   2.797 +    by (intro map_poly_idI) simp_all
   2.798 +  finally show ?thesis .
   2.799 +qed
   2.800 +
   2.801 +lemma content_decompose_fract:
   2.802 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
   2.803 +  obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
   2.804 +proof (cases "p = 0")
   2.805 +  case True
   2.806 +  hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
   2.807 +  thus ?thesis ..
   2.808 +next
   2.809 +  case False
   2.810 +  thus ?thesis
   2.811 +    by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
   2.812 +qed
   2.813 +
   2.814 +
   2.815 +subsection \<open>More properties of content and primitive part\<close>
   2.816 +
   2.817 +lemma lift_prime_elem_poly:
   2.818 +  assumes "prime_elem (c :: 'a :: semidom)"
   2.819 +  shows   "prime_elem [:c:]"
   2.820 +proof (rule prime_elemI)
   2.821 +  fix a b assume *: "[:c:] dvd a * b"
   2.822 +  from * have dvd: "c dvd coeff (a * b) n" for n
   2.823 +    by (subst (asm) const_poly_dvd_iff) blast
   2.824 +  {
   2.825 +    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
   2.826 +    assume "\<not>[:c:] dvd b"
   2.827 +    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
   2.828 +    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
   2.829 +      by (auto intro: le_degree simp: less_Suc_eq_le)
   2.830 +    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
   2.831 +    have "i \<le> m" if "\<not>c dvd coeff b i" for i
   2.832 +      unfolding m_def by (rule Greatest_le[OF that B])
   2.833 +    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
   2.834 +
   2.835 +    have "c dvd coeff a i" for i
   2.836 +    proof (induction i rule: nat_descend_induct[of "degree a"])
   2.837 +      case (base i)
   2.838 +      thus ?case by (simp add: coeff_eq_0)
   2.839 +    next
   2.840 +      case (descend i)
   2.841 +      let ?A = "{..i+m} - {i}"
   2.842 +      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
   2.843 +      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
   2.844 +        by (simp add: coeff_mult)
   2.845 +      also have "{..i+m} = insert i ?A" by auto
   2.846 +      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
   2.847 +                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
   2.848 +        (is "_ = _ + ?S")
   2.849 +        by (subst setsum.insert) simp_all
   2.850 +      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
   2.851 +      moreover have "c dvd ?S"
   2.852 +      proof (rule dvd_setsum)
   2.853 +        fix k assume k: "k \<in> {..i+m} - {i}"
   2.854 +        show "c dvd coeff a k * coeff b (i + m - k)"
   2.855 +        proof (cases "k < i")
   2.856 +          case False
   2.857 +          with k have "c dvd coeff a k" by (intro descend.IH) simp
   2.858 +          thus ?thesis by simp
   2.859 +        next
   2.860 +          case True
   2.861 +          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
   2.862 +          thus ?thesis by simp
   2.863 +        qed
   2.864 +      qed
   2.865 +      ultimately have "c dvd coeff a i * coeff b m"
   2.866 +        by (simp add: dvd_add_left_iff)
   2.867 +      with assms coeff_m show "c dvd coeff a i"
   2.868 +        by (simp add: prime_elem_dvd_mult_iff)
   2.869 +    qed
   2.870 +    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
   2.871 +  }
   2.872 +  thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
   2.873 +qed (insert assms, simp_all add: prime_elem_def one_poly_def)
   2.874 +
   2.875 +lemma prime_elem_const_poly_iff:
   2.876 +  fixes c :: "'a :: semidom"
   2.877 +  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
   2.878 +proof
   2.879 +  assume A: "prime_elem [:c:]"
   2.880 +  show "prime_elem c"
   2.881 +  proof (rule prime_elemI)
   2.882 +    fix a b assume "c dvd a * b"
   2.883 +    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
   2.884 +    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
   2.885 +    thus "c dvd a \<or> c dvd b" by simp
   2.886 +  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
   2.887 +qed (auto intro: lift_prime_elem_poly)
   2.888 +
   2.889 +context
   2.890 +begin
   2.891 +
   2.892 +private lemma content_1_mult:
   2.893 +  fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
   2.894 +  assumes "content f = 1" "content g = 1"
   2.895 +  shows   "content (f * g) = 1"
   2.896 +proof (cases "f * g = 0")
   2.897 +  case False
   2.898 +  from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
   2.899 +
   2.900 +  hence "f * g \<noteq> 0" by auto
   2.901 +  {
   2.902 +    assume "\<not>is_unit (content (f * g))"
   2.903 +    with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
   2.904 +      by (intro prime_divisor_exists) simp_all
   2.905 +    then obtain p where "p dvd content (f * g)" "prime p" by blast
   2.906 +    from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
   2.907 +      by (simp add: const_poly_dvd_iff_dvd_content)
   2.908 +    moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
   2.909 +    ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
   2.910 +      by (simp add: prime_elem_dvd_mult_iff)
   2.911 +    with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
   2.912 +    with \<open>prime p\<close> have False by simp
   2.913 +  }
   2.914 +  hence "is_unit (content (f * g))" by blast
   2.915 +  hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
   2.916 +  thus ?thesis by simp
   2.917 +qed (insert assms, auto)
   2.918 +
   2.919 +lemma content_mult:
   2.920 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   2.921 +  shows "content (p * q) = content p * content q"
   2.922 +proof -
   2.923 +  from content_decompose[of p] guess p' . note p = this
   2.924 +  from content_decompose[of q] guess q' . note q = this
   2.925 +  have "content (p * q) = content p * content q * content (p' * q')"
   2.926 +    by (subst p, subst q) (simp add: mult_ac normalize_mult)
   2.927 +  also from p q have "content (p' * q') = 1" by (intro content_1_mult)
   2.928 +  finally show ?thesis by simp
   2.929 +qed
   2.930 +
   2.931 +lemma primitive_part_mult:
   2.932 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   2.933 +  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
   2.934 +proof -
   2.935 +  have "primitive_part (p * q) = p * q div [:content (p * q):]"
   2.936 +    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   2.937 +  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
   2.938 +    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
   2.939 +  also have "\<dots> = primitive_part p * primitive_part q"
   2.940 +    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   2.941 +  finally show ?thesis .
   2.942 +qed
   2.943 +
   2.944 +lemma primitive_part_smult:
   2.945 +  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   2.946 +  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
   2.947 +proof -
   2.948 +  have "smult a p = [:a:] * p" by simp
   2.949 +  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
   2.950 +    by (subst primitive_part_mult) simp_all
   2.951 +  finally show ?thesis .
   2.952 +qed  
   2.953 +
   2.954 +lemma primitive_part_dvd_primitive_partI [intro]:
   2.955 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   2.956 +  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
   2.957 +  by (auto elim!: dvdE simp: primitive_part_mult)
   2.958 +
   2.959 +lemma content_msetprod: 
   2.960 +  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
   2.961 +  shows "content (msetprod A) = msetprod (image_mset content A)"
   2.962 +  by (induction A) (simp_all add: content_mult mult_ac)
   2.963 +
   2.964 +lemma fract_poly_dvdD:
   2.965 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   2.966 +  assumes "fract_poly p dvd fract_poly q" "content p = 1"
   2.967 +  shows   "p dvd q"
   2.968 +proof -
   2.969 +  from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
   2.970 +  from content_decompose_fract[of r] guess c r' . note r' = this
   2.971 +  from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
   2.972 +  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
   2.973 +  have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
   2.974 +  hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
   2.975 +  have "1 = gcd a (normalize b)" by (simp add: ab)
   2.976 +  also note eq'
   2.977 +  also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
   2.978 +  finally have [simp]: "a = 1" by simp
   2.979 +  from eq ab have "q = p * ([:b:] * r')" by simp
   2.980 +  thus ?thesis by (rule dvdI)
   2.981 +qed
   2.982 +
   2.983 +lemma content_prod_eq_1_iff: 
   2.984 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   2.985 +  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
   2.986 +proof safe
   2.987 +  assume A: "content (p * q) = 1"
   2.988 +  {
   2.989 +    fix p q :: "'a poly" assume "content p * content q = 1"
   2.990 +    hence "1 = content p * content q" by simp
   2.991 +    hence "content p dvd 1" by (rule dvdI)
   2.992 +    hence "content p = 1" by simp
   2.993 +  } note B = this
   2.994 +  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
   2.995 +    by (simp_all add: content_mult mult_ac)
   2.996 +qed (auto simp: content_mult)
   2.997 +
   2.998 +end
   2.999 +
  2.1000 +
  2.1001 +subsection \<open>Polynomials over a field are a Euclidean ring\<close>
  2.1002 +
  2.1003 +context
  2.1004 +begin
  2.1005 +
  2.1006 +private definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
  2.1007 +  "unit_factor_field_poly p = [:lead_coeff p:]"
  2.1008 +
  2.1009 +private definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
  2.1010 +  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
  2.1011 +
  2.1012 +private definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
  2.1013 +  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
  2.1014 +
  2.1015 +private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
  2.1016 +    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
  2.1017 +
  2.1018 +interpretation field_poly: 
  2.1019 +  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" 
  2.1020 +    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
  2.1021 +proof (standard, unfold dvd_field_poly)
  2.1022 +  fix p :: "'a poly"
  2.1023 +  show "unit_factor_field_poly p * normalize_field_poly p = p"
  2.1024 +    by (cases "p = 0") 
  2.1025 +       (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
  2.1026 +next
  2.1027 +  fix p :: "'a poly" assume "is_unit p"
  2.1028 +  thus "normalize_field_poly p = 1"
  2.1029 +    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
  2.1030 +next
  2.1031 +  fix p :: "'a poly" assume "p \<noteq> 0"
  2.1032 +  thus "is_unit (unit_factor_field_poly p)"
  2.1033 +    by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
  2.1034 +qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
  2.1035 +       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
  2.1036 +
  2.1037 +private lemma field_poly_irreducible_imp_prime:
  2.1038 +  assumes "irreducible (p :: 'a :: field poly)"
  2.1039 +  shows   "prime_elem p"
  2.1040 +proof -
  2.1041 +  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
  2.1042 +  from field_poly.irreducible_imp_prime_elem[of p] assms
  2.1043 +    show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
  2.1044 +      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
  2.1045 +qed
  2.1046 +
  2.1047 +private lemma field_poly_msetprod_prime_factorization:
  2.1048 +  assumes "(x :: 'a :: field poly) \<noteq> 0"
  2.1049 +  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
  2.1050 +proof -
  2.1051 +  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
  2.1052 +  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
  2.1053 +    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
  2.1054 +  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
  2.1055 +qed
  2.1056 +
  2.1057 +private lemma field_poly_in_prime_factorization_imp_prime:
  2.1058 +  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
  2.1059 +  shows   "prime_elem p"
  2.1060 +proof -
  2.1061 +  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
  2.1062 +  have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
  2.1063 +             normalize_field_poly unit_factor_field_poly" ..
  2.1064 +  from field_poly.in_prime_factorization_imp_prime[of p x] assms
  2.1065 +    show ?thesis unfolding prime_elem_def dvd_field_poly
  2.1066 +      comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
  2.1067 +qed
  2.1068 +
  2.1069 +
  2.1070 +subsection \<open>Primality and irreducibility in polynomial rings\<close>
  2.1071 +
  2.1072 +lemma nonconst_poly_irreducible_iff:
  2.1073 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  2.1074 +  assumes "degree p \<noteq> 0"
  2.1075 +  shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
  2.1076 +proof safe
  2.1077 +  assume p: "irreducible p"
  2.1078 +
  2.1079 +  from content_decompose[of p] guess p' . note p' = this
  2.1080 +  hence "p = [:content p:] * p'" by simp
  2.1081 +  from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
  2.1082 +  moreover have "\<not>p' dvd 1"
  2.1083 +  proof
  2.1084 +    assume "p' dvd 1"
  2.1085 +    hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
  2.1086 +    with assms show False by contradiction
  2.1087 +  qed
  2.1088 +  ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
  2.1089 +  
  2.1090 +  show "irreducible (map_poly to_fract p)"
  2.1091 +  proof (rule irreducibleI)
  2.1092 +    have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
  2.1093 +    with assms show "map_poly to_fract p \<noteq> 0" by auto
  2.1094 +  next
  2.1095 +    show "\<not>is_unit (fract_poly p)"
  2.1096 +    proof
  2.1097 +      assume "is_unit (map_poly to_fract p)"
  2.1098 +      hence "degree (map_poly to_fract p) = 0"
  2.1099 +        by (auto simp: is_unit_poly_iff)
  2.1100 +      hence "degree p = 0" by (simp add: degree_map_poly)
  2.1101 +      with assms show False by contradiction
  2.1102 +   qed
  2.1103 + next
  2.1104 +   fix q r assume qr: "fract_poly p = q * r"
  2.1105 +   from content_decompose_fract[of q] guess cg q' . note q = this
  2.1106 +   from content_decompose_fract[of r] guess cr r' . note r = this
  2.1107 +   from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
  2.1108 +   from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
  2.1109 +     by (simp add: q r)
  2.1110 +   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
  2.1111 +   hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
  2.1112 +   with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
  2.1113 +   hence "normalize b = gcd a b" by simp
  2.1114 +   also from ab(3) have "\<dots> = 1" .
  2.1115 +   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
  2.1116 +   
  2.1117 +   note eq
  2.1118 +   also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
  2.1119 +   also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
  2.1120 +   finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
  2.1121 +   from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
  2.1122 +   hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
  2.1123 +   hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
  2.1124 +   with q r show "is_unit q \<or> is_unit r"
  2.1125 +     by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
  2.1126 + qed
  2.1127 +
  2.1128 +next
  2.1129 +
  2.1130 +  assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
  2.1131 +  show "irreducible p"
  2.1132 +  proof (rule irreducibleI)
  2.1133 +    from irred show "p \<noteq> 0" by auto
  2.1134 +  next
  2.1135 +    from irred show "\<not>p dvd 1"
  2.1136 +      by (auto simp: irreducible_def dest: fract_poly_is_unit)
  2.1137 +  next
  2.1138 +    fix q r assume qr: "p = q * r"
  2.1139 +    hence "fract_poly p = fract_poly q * fract_poly r" by simp
  2.1140 +    from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
  2.1141 +      by (rule irreducibleD)
  2.1142 +    with primitive qr show "q dvd 1 \<or> r dvd 1"
  2.1143 +      by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
  2.1144 +  qed
  2.1145 +qed
  2.1146 +
  2.1147 +private lemma irreducible_imp_prime_poly:
  2.1148 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  2.1149 +  assumes "irreducible p"
  2.1150 +  shows   "prime_elem p"
  2.1151 +proof (cases "degree p = 0")
  2.1152 +  case True
  2.1153 +  with assms show ?thesis
  2.1154 +    by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
  2.1155 +             intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
  2.1156 +next
  2.1157 +  case False
  2.1158 +  from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
  2.1159 +    by (simp_all add: nonconst_poly_irreducible_iff)
  2.1160 +  from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
  2.1161 +  show ?thesis
  2.1162 +  proof (rule prime_elemI)
  2.1163 +    fix q r assume "p dvd q * r"
  2.1164 +    hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
  2.1165 +    hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
  2.1166 +    from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
  2.1167 +      by (rule prime_elem_dvd_multD)
  2.1168 +    with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
  2.1169 +  qed (insert assms, auto simp: irreducible_def)
  2.1170 +qed
  2.1171 +
  2.1172 +
  2.1173 +lemma degree_primitive_part_fract [simp]:
  2.1174 +  "degree (primitive_part_fract p) = degree p"
  2.1175 +proof -
  2.1176 +  have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
  2.1177 +    by (simp add: content_times_primitive_part_fract)
  2.1178 +  also have "degree \<dots> = degree (primitive_part_fract p)"
  2.1179 +    by (auto simp: degree_map_poly)
  2.1180 +  finally show ?thesis ..
  2.1181 +qed
  2.1182 +
  2.1183 +lemma irreducible_primitive_part_fract:
  2.1184 +  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
  2.1185 +  assumes "irreducible p"
  2.1186 +  shows   "irreducible (primitive_part_fract p)"
  2.1187 +proof -
  2.1188 +  from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
  2.1189 +    by (intro notI) 
  2.1190 +       (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
  2.1191 +  hence [simp]: "p \<noteq> 0" by auto
  2.1192 +
  2.1193 +  note \<open>irreducible p\<close>
  2.1194 +  also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
  2.1195 +    by (simp add: content_times_primitive_part_fract)
  2.1196 +  also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
  2.1197 +    by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
  2.1198 +  finally show ?thesis using deg
  2.1199 +    by (simp add: nonconst_poly_irreducible_iff)
  2.1200 +qed
  2.1201 +
  2.1202 +lemma prime_elem_primitive_part_fract:
  2.1203 +  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
  2.1204 +  shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
  2.1205 +  by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
  2.1206 +
  2.1207 +lemma irreducible_linear_field_poly:
  2.1208 +  fixes a b :: "'a::field"
  2.1209 +  assumes "b \<noteq> 0"
  2.1210 +  shows "irreducible [:a,b:]"
  2.1211 +proof (rule irreducibleI)
  2.1212 +  fix p q assume pq: "[:a,b:] = p * q"
  2.1213 +  also from pq assms have "degree \<dots> = degree p + degree q" 
  2.1214 +    by (intro degree_mult_eq) auto
  2.1215 +  finally have "degree p = 0 \<or> degree q = 0" using assms by auto
  2.1216 +  with assms pq show "is_unit p \<or> is_unit q"
  2.1217 +    by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
  2.1218 +qed (insert assms, auto simp: is_unit_poly_iff)
  2.1219 +
  2.1220 +lemma prime_elem_linear_field_poly:
  2.1221 +  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
  2.1222 +  by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
  2.1223 +
  2.1224 +lemma irreducible_linear_poly:
  2.1225 +  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
  2.1226 +  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
  2.1227 +  by (auto intro!: irreducible_linear_field_poly 
  2.1228 +           simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
  2.1229 +
  2.1230 +lemma prime_elem_linear_poly:
  2.1231 +  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
  2.1232 +  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
  2.1233 +  by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
  2.1234 +
  2.1235 +  
  2.1236 +subsection \<open>Prime factorisation of polynomials\<close>   
  2.1237 +
  2.1238 +private lemma poly_prime_factorization_exists_content_1:
  2.1239 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  2.1240 +  assumes "p \<noteq> 0" "content p = 1"
  2.1241 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  2.1242 +proof -
  2.1243 +  let ?P = "field_poly.prime_factorization (fract_poly p)"
  2.1244 +  define c where "c = msetprod (image_mset fract_content ?P)"
  2.1245 +  define c' where "c' = c * to_fract (lead_coeff p)"
  2.1246 +  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
  2.1247 +  define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
  2.1248 +  have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
  2.1249 +                      content (primitive_part_fract x))"
  2.1250 +    by (simp add: e_def content_msetprod multiset.map_comp o_def)
  2.1251 +  also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
  2.1252 +    by (intro image_mset_cong content_primitive_part_fract) auto
  2.1253 +  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
  2.1254 +  
  2.1255 +  have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
  2.1256 +          normalize_field_poly (fract_poly p)" by simp
  2.1257 +  also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
  2.1258 +    by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
  2.1259 +  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
  2.1260 +    by (subst field_poly_msetprod_prime_factorization) simp_all
  2.1261 +  also have "\<dots> = msetprod (image_mset id ?P)" by simp
  2.1262 +  also have "image_mset id ?P = 
  2.1263 +               image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
  2.1264 +    by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
  2.1265 +  also have "msetprod \<dots> = smult c (fract_poly e)"
  2.1266 +    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
  2.1267 +  also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
  2.1268 +    by (simp add: c'_def)
  2.1269 +  finally have eq: "fract_poly p = smult c' (fract_poly e)" .
  2.1270 +  also obtain b where b: "c' = to_fract b" "is_unit b"
  2.1271 +  proof -
  2.1272 +    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
  2.1273 +    from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
  2.1274 +    with assms content_e have "a = normalize b" by (simp add: ab(4))
  2.1275 +    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
  2.1276 +    with ab ab' have "c' = to_fract b" by auto
  2.1277 +    from this and \<open>is_unit b\<close> show ?thesis by (rule that)
  2.1278 +  qed
  2.1279 +  hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
  2.1280 +  finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
  2.1281 +  hence "p = [:b:] * e" by simp
  2.1282 +  with b have "normalize p = normalize e" 
  2.1283 +    by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
  2.1284 +  also have "normalize e = msetprod A"
  2.1285 +    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
  2.1286 +  finally have "msetprod A = normalize p" ..
  2.1287 +  
  2.1288 +  have "prime_elem p" if "p \<in># A" for p
  2.1289 +    using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
  2.1290 +                        dest!: field_poly_in_prime_factorization_imp_prime )
  2.1291 +  from this and \<open>msetprod A = normalize p\<close> show ?thesis
  2.1292 +    by (intro exI[of _ A]) blast
  2.1293 +qed
  2.1294 +
  2.1295 +lemma poly_prime_factorization_exists:
  2.1296 +  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  2.1297 +  assumes "p \<noteq> 0"
  2.1298 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  2.1299 +proof -
  2.1300 +  define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
  2.1301 +  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
  2.1302 +    by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
  2.1303 +  then guess A by (elim exE conjE) note A = this
  2.1304 +  moreover from assms have "msetprod B = [:content p:]"
  2.1305 +    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
  2.1306 +  moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
  2.1307 +    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
  2.1308 +  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
  2.1309 +qed
  2.1310 +
  2.1311 +end
  2.1312 +
  2.1313 +
  2.1314 +subsection \<open>Typeclass instances\<close>
  2.1315 +
  2.1316 +instance poly :: (factorial_ring_gcd) factorial_semiring
  2.1317 +  by standard (rule poly_prime_factorization_exists)  
  2.1318 +
  2.1319 +instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
  2.1320 +begin
  2.1321 +
  2.1322 +definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  2.1323 +  [code del]: "gcd_poly = gcd_factorial"
  2.1324 +
  2.1325 +definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  2.1326 +  [code del]: "lcm_poly = lcm_factorial"
  2.1327 +  
  2.1328 +definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
  2.1329 + [code del]: "Gcd_poly = Gcd_factorial"
  2.1330 +
  2.1331 +definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
  2.1332 + [code del]: "Lcm_poly = Lcm_factorial"
  2.1333 + 
  2.1334 +instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
  2.1335 +
  2.1336 +end
  2.1337 +
  2.1338 +instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
  2.1339 +begin
  2.1340 +
  2.1341 +definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
  2.1342 +  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
  2.1343 +
  2.1344 +instance 
  2.1345 +  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
  2.1346 +end
  2.1347 +
  2.1348 +
  2.1349 +instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
  2.1350 +  by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
  2.1351 +
  2.1352 +  
  2.1353 +subsection \<open>Polynomial GCD\<close>
  2.1354 +
  2.1355 +lemma gcd_poly_decompose:
  2.1356 +  fixes p q :: "'a :: factorial_ring_gcd poly"
  2.1357 +  shows "gcd p q = 
  2.1358 +           smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  2.1359 +proof (rule sym, rule gcdI)
  2.1360 +  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  2.1361 +          [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
  2.1362 +  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
  2.1363 +    by simp
  2.1364 +next
  2.1365 +  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  2.1366 +          [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
  2.1367 +  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
  2.1368 +    by simp
  2.1369 +next
  2.1370 +  fix d assume "d dvd p" "d dvd q"
  2.1371 +  hence "[:content d:] * primitive_part d dvd 
  2.1372 +           [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
  2.1373 +    by (intro mult_dvd_mono) auto
  2.1374 +  thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  2.1375 +    by simp
  2.1376 +qed (auto simp: normalize_smult)
  2.1377 +  
  2.1378 +
  2.1379 +lemma gcd_poly_pseudo_mod:
  2.1380 +  fixes p q :: "'a :: factorial_ring_gcd poly"
  2.1381 +  assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
  2.1382 +  shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
  2.1383 +proof -
  2.1384 +  define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
  2.1385 +  define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
  2.1386 +  have [simp]: "primitive_part a = unit_factor a"
  2.1387 +    by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
  2.1388 +  from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
  2.1389 +  
  2.1390 +  have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
  2.1391 +  have "gcd (q * r + s) q = gcd q s"
  2.1392 +    using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
  2.1393 +  with pseudo_divmod(1)[OF nz rs]
  2.1394 +    have "gcd (p * a) q = gcd q s" by (simp add: a_def)
  2.1395 +  also from prim have "gcd (p * a) q = gcd p q"
  2.1396 +    by (subst gcd_poly_decompose)
  2.1397 +       (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
  2.1398 +             simp del: mult_pCons_right )
  2.1399 +  also from prim have "gcd q s = gcd q (primitive_part s)"
  2.1400 +    by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
  2.1401 +  also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
  2.1402 +  finally show ?thesis .
  2.1403 +qed
  2.1404 +
  2.1405 +lemma degree_pseudo_mod_less:
  2.1406 +  assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
  2.1407 +  shows   "degree (pseudo_mod p q) < degree q"
  2.1408 +  using pseudo_mod(2)[of q p] assms by auto
  2.1409 +
  2.1410 +function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  2.1411 +  "gcd_poly_code_aux p q = 
  2.1412 +     (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
  2.1413 +by auto
  2.1414 +termination
  2.1415 +  by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
  2.1416 +     (auto simp: degree_primitive_part degree_pseudo_mod_less)
  2.1417 +
  2.1418 +declare gcd_poly_code_aux.simps [simp del]
  2.1419 +
  2.1420 +lemma gcd_poly_code_aux_correct:
  2.1421 +  assumes "content p = 1" "q = 0 \<or> content q = 1"
  2.1422 +  shows   "gcd_poly_code_aux p q = gcd p q"
  2.1423 +  using assms
  2.1424 +proof (induction p q rule: gcd_poly_code_aux.induct)
  2.1425 +  case (1 p q)
  2.1426 +  show ?case
  2.1427 +  proof (cases "q = 0")
  2.1428 +    case True
  2.1429 +    thus ?thesis by (subst gcd_poly_code_aux.simps) auto
  2.1430 +  next
  2.1431 +    case False
  2.1432 +    hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
  2.1433 +      by (subst gcd_poly_code_aux.simps) simp_all
  2.1434 +    also from "1.prems" False 
  2.1435 +      have "primitive_part (pseudo_mod p q) = 0 \<or> 
  2.1436 +              content (primitive_part (pseudo_mod p q)) = 1"
  2.1437 +      by (cases "pseudo_mod p q = 0") auto
  2.1438 +    with "1.prems" False 
  2.1439 +      have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
  2.1440 +              gcd q (primitive_part (pseudo_mod p q))"
  2.1441 +      by (intro 1) simp_all
  2.1442 +    also from "1.prems" False 
  2.1443 +      have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
  2.1444 +    finally show ?thesis .
  2.1445 +  qed
  2.1446 +qed
  2.1447 +
  2.1448 +definition gcd_poly_code 
  2.1449 +    :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
  2.1450 +  where "gcd_poly_code p q = 
  2.1451 +           (if p = 0 then normalize q else if q = 0 then normalize p else
  2.1452 +              smult (gcd (content p) (content q)) 
  2.1453 +                (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
  2.1454 +
  2.1455 +lemma lcm_poly_code [code]: 
  2.1456 +  fixes p q :: "'a :: factorial_ring_gcd poly"
  2.1457 +  shows "lcm p q = normalize (p * q) div gcd p q"
  2.1458 +  by (rule lcm_gcd)
  2.1459 +
  2.1460 +lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
  2.1461 +  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
  2.1462 +
  2.1463 +declare Gcd_set
  2.1464 +  [where ?'a = "'a :: factorial_ring_gcd poly", code]
  2.1465 +
  2.1466 +declare Lcm_set
  2.1467 +  [where ?'a = "'a :: factorial_ring_gcd poly", code]
  2.1468 +  
  2.1469 +value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
  2.1470 +
  2.1471 +end
     3.1 --- a/src/HOL/Library/Polynomial_GCD_euclidean.thy	Sun Aug 14 23:35:16 2016 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,140 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Polynomial_GCD_euclidean.thy
     3.5 -    Author:     Brian Huffman
     3.6 -    Author:     Clemens Ballarin
     3.7 -    Author:     Amine Chaieb
     3.8 -    Author:     Florian Haftmann
     3.9 -*)
    3.10 -
    3.11 -section \<open>GCD and LCM on polynomials over a field\<close>
    3.12 -
    3.13 -theory Polynomial_GCD_euclidean
    3.14 -imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
    3.15 -begin
    3.16 -
    3.17 -subsection \<open>GCD of polynomials\<close>
    3.18 -
    3.19 -instantiation poly :: (field) gcd
    3.20 -begin
    3.21 -
    3.22 -function gcd_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    3.23 -where
    3.24 -  "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"
    3.25 -| "y \<noteq> 0 \<Longrightarrow> gcd (x::'a poly) y = gcd y (x mod y)"
    3.26 -by auto
    3.27 -
    3.28 -termination "gcd :: _ poly \<Rightarrow> _"
    3.29 -by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
    3.30 -   (auto dest: degree_mod_less)
    3.31 -
    3.32 -declare gcd_poly.simps [simp del]
    3.33 -
    3.34 -definition lcm_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    3.35 -where
    3.36 -  "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)"
    3.37 -
    3.38 -instance ..
    3.39 -
    3.40 -end
    3.41 -
    3.42 -lemma
    3.43 -  fixes x y :: "_ poly"
    3.44 -  shows poly_gcd_dvd1 [iff]: "gcd x y dvd x"
    3.45 -    and poly_gcd_dvd2 [iff]: "gcd x y dvd y"
    3.46 -  apply (induct x y rule: gcd_poly.induct)
    3.47 -  apply (simp_all add: gcd_poly.simps)
    3.48 -  apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
    3.49 -  apply (blast dest: dvd_mod_imp_dvd)
    3.50 -  done
    3.51 -
    3.52 -lemma poly_gcd_greatest:
    3.53 -  fixes k x y :: "_ poly"
    3.54 -  shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y"
    3.55 -  by (induct x y rule: gcd_poly.induct)
    3.56 -     (simp_all add: gcd_poly.simps dvd_mod dvd_smult)
    3.57 -
    3.58 -lemma dvd_poly_gcd_iff [iff]:
    3.59 -  fixes k x y :: "_ poly"
    3.60 -  shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
    3.61 -  by (auto intro!: poly_gcd_greatest intro: dvd_trans [of _ "gcd x y"])
    3.62 -
    3.63 -lemma poly_gcd_monic:
    3.64 -  fixes x y :: "_ poly"
    3.65 -  shows "coeff (gcd x y) (degree (gcd x y)) =
    3.66 -    (if x = 0 \<and> y = 0 then 0 else 1)"
    3.67 -  by (induct x y rule: gcd_poly.induct)
    3.68 -     (simp_all add: gcd_poly.simps nonzero_imp_inverse_nonzero)
    3.69 -
    3.70 -lemma poly_gcd_zero_iff [simp]:
    3.71 -  fixes x y :: "_ poly"
    3.72 -  shows "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    3.73 -  by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
    3.74 -
    3.75 -lemma poly_gcd_0_0 [simp]:
    3.76 -  "gcd (0::_ poly) 0 = 0"
    3.77 -  by simp
    3.78 -
    3.79 -lemma poly_dvd_antisym:
    3.80 -  fixes p q :: "'a::idom poly"
    3.81 -  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
    3.82 -  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
    3.83 -proof (cases "p = 0")
    3.84 -  case True with coeff show "p = q" by simp
    3.85 -next
    3.86 -  case False with coeff have "q \<noteq> 0" by auto
    3.87 -  have degree: "degree p = degree q"
    3.88 -    using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
    3.89 -    by (intro order_antisym dvd_imp_degree_le)
    3.90 -
    3.91 -  from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
    3.92 -  with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
    3.93 -  with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"
    3.94 -    by (simp add: degree_mult_eq)
    3.95 -  with coeff a show "p = q"
    3.96 -    by (cases a, auto split: if_splits)
    3.97 -qed
    3.98 -
    3.99 -lemma poly_gcd_unique:
   3.100 -  fixes d x y :: "_ poly"
   3.101 -  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
   3.102 -    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
   3.103 -    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
   3.104 -  shows "gcd x y = d"
   3.105 -proof -
   3.106 -  have "coeff (gcd x y) (degree (gcd x y)) = coeff d (degree d)"
   3.107 -    by (simp_all add: poly_gcd_monic monic)
   3.108 -  moreover have "gcd x y dvd d"
   3.109 -    using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
   3.110 -  moreover have "d dvd gcd x y"
   3.111 -    using dvd1 dvd2 by (rule poly_gcd_greatest)
   3.112 -  ultimately show ?thesis
   3.113 -    by (rule poly_dvd_antisym)
   3.114 -qed
   3.115 -
   3.116 -instance poly :: (field) semiring_gcd
   3.117 -proof
   3.118 -  fix p q :: "'a::field poly"
   3.119 -  show "normalize (gcd p q) = gcd p q"
   3.120 -    by (induct p q rule: gcd_poly.induct)
   3.121 -      (simp_all add: gcd_poly.simps normalize_poly_def)
   3.122 -  show "lcm p q = normalize (p * q) div gcd p q"
   3.123 -    by (simp add: coeff_degree_mult div_smult_left div_smult_right lcm_poly_def normalize_poly_def)
   3.124 -      (metis (no_types, lifting) div_smult_right inverse_mult_distrib inverse_zero mult.commute pdivmod_rel pdivmod_rel_def smult_eq_0_iff)
   3.125 -qed simp_all
   3.126 -
   3.127 -lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
   3.128 -by (rule poly_gcd_unique) simp_all
   3.129 -
   3.130 -lemma poly_gcd_1_right [simp]: "gcd x 1 = (1 :: _ poly)"
   3.131 -by (rule poly_gcd_unique) simp_all
   3.132 -
   3.133 -lemma poly_gcd_minus_left [simp]: "gcd (- x) y = gcd x (y :: _ poly)"
   3.134 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
   3.135 -
   3.136 -lemma poly_gcd_minus_right [simp]: "gcd x (- y) = gcd x (y :: _ poly)"
   3.137 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
   3.138 -
   3.139 -lemma poly_gcd_code [code]:
   3.140 -  "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
   3.141 -  by (simp add: gcd_poly.simps)
   3.142 -
   3.143 -end
     4.1 --- a/src/HOL/Number_Theory/Polynomial_Factorial.thy	Sun Aug 14 23:35:16 2016 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,1468 +0,0 @@
     4.4 -theory Polynomial_Factorial
     4.5 -imports 
     4.6 -  Complex_Main
     4.7 -  Euclidean_Algorithm 
     4.8 -  "~~/src/HOL/Library/Polynomial"
     4.9 -  "~~/src/HOL/Library/Normalized_Fraction"
    4.10 -begin
    4.11 -
    4.12 -subsection \<open>Prelude\<close>
    4.13 -
    4.14 -lemma msetprod_mult: 
    4.15 -  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
    4.16 -  by (induction A) (simp_all add: mult_ac)
    4.17 -  
    4.18 -lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
    4.19 -  by (induction A) (simp_all add: mult_ac)
    4.20 -  
    4.21 -lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
    4.22 -proof safe
    4.23 -  assume "x \<noteq> 0"
    4.24 -  hence "y = x * (y / x)" by (simp add: field_simps)
    4.25 -  thus "x dvd y" by (rule dvdI)
    4.26 -qed auto
    4.27 -
    4.28 -lemma nat_descend_induct [case_names base descend]:
    4.29 -  assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
    4.30 -  assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
    4.31 -  shows   "P m"
    4.32 -  using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
    4.33 -
    4.34 -lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
    4.35 -  by (metis GreatestI)
    4.36 -
    4.37 -
    4.38 -context field
    4.39 -begin
    4.40 -
    4.41 -subclass idom_divide ..
    4.42 -
    4.43 -end
    4.44 -
    4.45 -context field
    4.46 -begin
    4.47 -
    4.48 -definition normalize_field :: "'a \<Rightarrow> 'a" 
    4.49 -  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
    4.50 -definition unit_factor_field :: "'a \<Rightarrow> 'a" 
    4.51 -  where [simp]: "unit_factor_field x = x"
    4.52 -definition euclidean_size_field :: "'a \<Rightarrow> nat" 
    4.53 -  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
    4.54 -definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.55 -  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
    4.56 -
    4.57 -end
    4.58 -
    4.59 -instantiation real :: euclidean_ring
    4.60 -begin
    4.61 -
    4.62 -definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    4.63 -definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    4.64 -definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    4.65 -definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
    4.66 -
    4.67 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    4.68 -end
    4.69 -
    4.70 -instantiation real :: euclidean_ring_gcd
    4.71 -begin
    4.72 -
    4.73 -definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    4.74 -  "gcd_real = gcd_eucl"
    4.75 -definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    4.76 -  "lcm_real = lcm_eucl"
    4.77 -definition Gcd_real :: "real set \<Rightarrow> real" where
    4.78 - "Gcd_real = Gcd_eucl"
    4.79 -definition Lcm_real :: "real set \<Rightarrow> real" where
    4.80 - "Lcm_real = Lcm_eucl"
    4.81 -
    4.82 -instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    4.83 -
    4.84 -end
    4.85 -
    4.86 -instantiation rat :: euclidean_ring
    4.87 -begin
    4.88 -
    4.89 -definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    4.90 -definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    4.91 -definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    4.92 -definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
    4.93 -
    4.94 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    4.95 -end
    4.96 -
    4.97 -instantiation rat :: euclidean_ring_gcd
    4.98 -begin
    4.99 -
   4.100 -definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   4.101 -  "gcd_rat = gcd_eucl"
   4.102 -definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   4.103 -  "lcm_rat = lcm_eucl"
   4.104 -definition Gcd_rat :: "rat set \<Rightarrow> rat" where
   4.105 - "Gcd_rat = Gcd_eucl"
   4.106 -definition Lcm_rat :: "rat set \<Rightarrow> rat" where
   4.107 - "Lcm_rat = Lcm_eucl"
   4.108 -
   4.109 -instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
   4.110 -
   4.111 -end
   4.112 -
   4.113 -instantiation complex :: euclidean_ring
   4.114 -begin
   4.115 -
   4.116 -definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
   4.117 -definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
   4.118 -definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
   4.119 -definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
   4.120 -
   4.121 -instance by standard (simp_all add: dvd_field_iff divide_simps)
   4.122 -end
   4.123 -
   4.124 -instantiation complex :: euclidean_ring_gcd
   4.125 -begin
   4.126 -
   4.127 -definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   4.128 -  "gcd_complex = gcd_eucl"
   4.129 -definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   4.130 -  "lcm_complex = lcm_eucl"
   4.131 -definition Gcd_complex :: "complex set \<Rightarrow> complex" where
   4.132 - "Gcd_complex = Gcd_eucl"
   4.133 -definition Lcm_complex :: "complex set \<Rightarrow> complex" where
   4.134 - "Lcm_complex = Lcm_eucl"
   4.135 -
   4.136 -instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
   4.137 -
   4.138 -end
   4.139 -
   4.140 -
   4.141 -
   4.142 -subsection \<open>Lifting elements into the field of fractions\<close>
   4.143 -
   4.144 -definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
   4.145 -
   4.146 -lemma to_fract_0 [simp]: "to_fract 0 = 0"
   4.147 -  by (simp add: to_fract_def eq_fract Zero_fract_def)
   4.148 -
   4.149 -lemma to_fract_1 [simp]: "to_fract 1 = 1"
   4.150 -  by (simp add: to_fract_def eq_fract One_fract_def)
   4.151 -
   4.152 -lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
   4.153 -  by (simp add: to_fract_def)
   4.154 -
   4.155 -lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
   4.156 -  by (simp add: to_fract_def)
   4.157 -  
   4.158 -lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
   4.159 -  by (simp add: to_fract_def)
   4.160 -  
   4.161 -lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
   4.162 -  by (simp add: to_fract_def)
   4.163 -
   4.164 -lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
   4.165 -  by (simp add: to_fract_def eq_fract)
   4.166 -  
   4.167 -lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
   4.168 -  by (simp add: to_fract_def Zero_fract_def eq_fract)
   4.169 -
   4.170 -lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
   4.171 -  by transfer simp
   4.172 -
   4.173 -lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
   4.174 -  by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
   4.175 -
   4.176 -lemma to_fract_quot_of_fract:
   4.177 -  assumes "snd (quot_of_fract x) = 1"
   4.178 -  shows   "to_fract (fst (quot_of_fract x)) = x"
   4.179 -proof -
   4.180 -  have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
   4.181 -  also note assms
   4.182 -  finally show ?thesis by (simp add: to_fract_def)
   4.183 -qed
   4.184 -
   4.185 -lemma snd_quot_of_fract_Fract_whole:
   4.186 -  assumes "y dvd x"
   4.187 -  shows   "snd (quot_of_fract (Fract x y)) = 1"
   4.188 -  using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
   4.189 -  
   4.190 -lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
   4.191 -  by (simp add: to_fract_def)
   4.192 -
   4.193 -lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
   4.194 -  unfolding to_fract_def by transfer (simp add: normalize_quot_def)
   4.195 -
   4.196 -lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
   4.197 -  by transfer simp
   4.198 - 
   4.199 -lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
   4.200 -  unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
   4.201 -
   4.202 -lemma coprime_quot_of_fract:
   4.203 -  "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
   4.204 -  by transfer (simp add: coprime_normalize_quot)
   4.205 -
   4.206 -lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
   4.207 -  using quot_of_fract_in_normalized_fracts[of x] 
   4.208 -  by (simp add: normalized_fracts_def case_prod_unfold)  
   4.209 -
   4.210 -lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
   4.211 -  by (subst (2) normalize_mult_unit_factor [symmetric, of x])
   4.212 -     (simp del: normalize_mult_unit_factor)
   4.213 -  
   4.214 -lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
   4.215 -  by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
   4.216 -
   4.217 -  
   4.218 -subsection \<open>Mapping polynomials\<close>
   4.219 -
   4.220 -definition map_poly 
   4.221 -     :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
   4.222 -  "map_poly f p = Poly (map f (coeffs p))"
   4.223 -
   4.224 -lemma map_poly_0 [simp]: "map_poly f 0 = 0"
   4.225 -  by (simp add: map_poly_def)
   4.226 -
   4.227 -lemma map_poly_1: "map_poly f 1 = [:f 1:]"
   4.228 -  by (simp add: map_poly_def)
   4.229 -
   4.230 -lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
   4.231 -  by (simp add: map_poly_def one_poly_def)
   4.232 -
   4.233 -lemma coeff_map_poly:
   4.234 -  assumes "f 0 = 0"
   4.235 -  shows   "coeff (map_poly f p) n = f (coeff p n)"
   4.236 -  by (auto simp: map_poly_def nth_default_def coeffs_def assms
   4.237 -        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
   4.238 -
   4.239 -lemma coeffs_map_poly [code abstract]: 
   4.240 -    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
   4.241 -  by (simp add: map_poly_def)
   4.242 -
   4.243 -lemma set_coeffs_map_poly:
   4.244 -  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
   4.245 -  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
   4.246 -
   4.247 -lemma coeffs_map_poly': 
   4.248 -  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
   4.249 -  shows   "coeffs (map_poly f p) = map f (coeffs p)"
   4.250 -  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
   4.251 -                           intro!: strip_while_not_last split: if_splits)
   4.252 -
   4.253 -lemma degree_map_poly:
   4.254 -  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   4.255 -  shows   "degree (map_poly f p) = degree p"
   4.256 -  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
   4.257 -
   4.258 -lemma map_poly_eq_0_iff:
   4.259 -  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   4.260 -  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
   4.261 -proof -
   4.262 -  {
   4.263 -    fix n :: nat
   4.264 -    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
   4.265 -    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
   4.266 -    proof (cases "n < length (coeffs p)")
   4.267 -      case True
   4.268 -      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
   4.269 -      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
   4.270 -    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
   4.271 -    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
   4.272 -  }
   4.273 -  thus ?thesis by (auto simp: poly_eq_iff)
   4.274 -qed
   4.275 -
   4.276 -lemma map_poly_smult:
   4.277 -  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
   4.278 -  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
   4.279 -  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
   4.280 -
   4.281 -lemma map_poly_pCons:
   4.282 -  assumes "f 0 = 0"
   4.283 -  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
   4.284 -  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
   4.285 -
   4.286 -lemma map_poly_map_poly:
   4.287 -  assumes "f 0 = 0" "g 0 = 0"
   4.288 -  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
   4.289 -  by (intro poly_eqI) (simp add: coeff_map_poly assms)
   4.290 -
   4.291 -lemma map_poly_id [simp]: "map_poly id p = p"
   4.292 -  by (simp add: map_poly_def)
   4.293 -
   4.294 -lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
   4.295 -  by (simp add: map_poly_def)
   4.296 -
   4.297 -lemma map_poly_cong: 
   4.298 -  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
   4.299 -  shows   "map_poly f p = map_poly g p"
   4.300 -proof -
   4.301 -  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
   4.302 -  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
   4.303 -qed
   4.304 -
   4.305 -lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
   4.306 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   4.307 -
   4.308 -lemma map_poly_idI:
   4.309 -  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   4.310 -  shows   "map_poly f p = p"
   4.311 -  using map_poly_cong[OF assms, of _ id] by simp
   4.312 -
   4.313 -lemma map_poly_idI':
   4.314 -  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   4.315 -  shows   "p = map_poly f p"
   4.316 -  using map_poly_cong[OF assms, of _ id] by simp
   4.317 -
   4.318 -lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
   4.319 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   4.320 -
   4.321 -lemma div_const_poly_conv_map_poly: 
   4.322 -  assumes "[:c:] dvd p"
   4.323 -  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
   4.324 -proof (cases "c = 0")
   4.325 -  case False
   4.326 -  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   4.327 -  moreover {
   4.328 -    have "smult c q = [:c:] * q" by simp
   4.329 -    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
   4.330 -    finally have "smult c q div [:c:] = q" .
   4.331 -  }
   4.332 -  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
   4.333 -qed (auto intro!: poly_eqI simp: coeff_map_poly)
   4.334 -
   4.335 -
   4.336 -
   4.337 -subsection \<open>Various facts about polynomials\<close>
   4.338 -
   4.339 -lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
   4.340 -  by (induction A) (simp_all add: one_poly_def mult_ac)
   4.341 -
   4.342 -lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
   4.343 -  using degree_mod_less[of b a] by auto
   4.344 -  
   4.345 -lemma is_unit_const_poly_iff: 
   4.346 -    "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
   4.347 -  by (auto simp: one_poly_def)
   4.348 -
   4.349 -lemma is_unit_poly_iff:
   4.350 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   4.351 -  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
   4.352 -proof safe
   4.353 -  assume "p dvd 1"
   4.354 -  then obtain q where pq: "1 = p * q" by (erule dvdE)
   4.355 -  hence "degree 1 = degree (p * q)" by simp
   4.356 -  also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
   4.357 -  finally have "degree p = 0" by simp
   4.358 -  from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
   4.359 -  with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
   4.360 -    by (auto simp: is_unit_const_poly_iff)
   4.361 -qed (auto simp: is_unit_const_poly_iff)
   4.362 -
   4.363 -lemma is_unit_polyE:
   4.364 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   4.365 -  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
   4.366 -  using assms by (subst (asm) is_unit_poly_iff) blast
   4.367 -
   4.368 -lemma smult_eq_iff:
   4.369 -  assumes "(b :: 'a :: field) \<noteq> 0"
   4.370 -  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   4.371 -proof
   4.372 -  assume "smult a p = smult b q"
   4.373 -  also from assms have "smult (inverse b) \<dots> = q" by simp
   4.374 -  finally show "smult (a / b) p = q" by (simp add: field_simps)
   4.375 -qed (insert assms, auto)
   4.376 -
   4.377 -lemma irreducible_const_poly_iff:
   4.378 -  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   4.379 -  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
   4.380 -proof
   4.381 -  assume A: "irreducible c"
   4.382 -  show "irreducible [:c:]"
   4.383 -  proof (rule irreducibleI)
   4.384 -    fix a b assume ab: "[:c:] = a * b"
   4.385 -    hence "degree [:c:] = degree (a * b)" by (simp only: )
   4.386 -    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
   4.387 -    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
   4.388 -    finally have "degree a = 0" "degree b = 0" by auto
   4.389 -    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
   4.390 -    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
   4.391 -    hence "c = a' * b'" by (simp add: ab' mult_ac)
   4.392 -    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
   4.393 -    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
   4.394 -  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
   4.395 -next
   4.396 -  assume A: "irreducible [:c:]"
   4.397 -  show "irreducible c"
   4.398 -  proof (rule irreducibleI)
   4.399 -    fix a b assume ab: "c = a * b"
   4.400 -    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
   4.401 -    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
   4.402 -    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
   4.403 -  qed (insert A, auto simp: irreducible_def one_poly_def)
   4.404 -qed
   4.405 -
   4.406 -lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   4.407 -  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
   4.408 -
   4.409 -  
   4.410 -subsection \<open>Normalisation of polynomials\<close>
   4.411 -
   4.412 -instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
   4.413 -begin
   4.414 -
   4.415 -definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   4.416 -  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
   4.417 -
   4.418 -definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
   4.419 -  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   4.420 -
   4.421 -lemma normalize_poly_altdef:
   4.422 -  "normalize p = p div [:unit_factor (lead_coeff p):]"
   4.423 -proof (cases "p = 0")
   4.424 -  case False
   4.425 -  thus ?thesis
   4.426 -    by (subst div_const_poly_conv_map_poly)
   4.427 -       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
   4.428 -qed (auto simp: normalize_poly_def)
   4.429 -
   4.430 -instance
   4.431 -proof
   4.432 -  fix p :: "'a poly"
   4.433 -  show "unit_factor p * normalize p = p"
   4.434 -    by (cases "p = 0")
   4.435 -       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
   4.436 -          smult_conv_map_poly map_poly_map_poly o_def)
   4.437 -next
   4.438 -  fix p :: "'a poly"
   4.439 -  assume "is_unit p"
   4.440 -  then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
   4.441 -  thus "normalize p = 1"
   4.442 -    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
   4.443 -next
   4.444 -  fix p :: "'a poly" assume "p \<noteq> 0"
   4.445 -  thus "is_unit (unit_factor p)"
   4.446 -    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
   4.447 -qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
   4.448 -
   4.449 -end
   4.450 -
   4.451 -lemma unit_factor_pCons:
   4.452 -  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   4.453 -  by (simp add: unit_factor_poly_def)
   4.454 -
   4.455 -lemma normalize_monom [simp]:
   4.456 -  "normalize (monom a n) = monom (normalize a) n"
   4.457 -  by (simp add: map_poly_monom normalize_poly_def)
   4.458 -
   4.459 -lemma unit_factor_monom [simp]:
   4.460 -  "unit_factor (monom a n) = monom (unit_factor a) 0"
   4.461 -  by (simp add: unit_factor_poly_def )
   4.462 -
   4.463 -lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   4.464 -  by (simp add: normalize_poly_def map_poly_pCons)
   4.465 -
   4.466 -lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   4.467 -proof -
   4.468 -  have "smult c p = [:c:] * p" by simp
   4.469 -  also have "normalize \<dots> = smult (normalize c) (normalize p)"
   4.470 -    by (subst normalize_mult) (simp add: normalize_const_poly)
   4.471 -  finally show ?thesis .
   4.472 -qed
   4.473 -
   4.474 -lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   4.475 -proof -
   4.476 -  have "smult c p = [:c:] * p" by simp
   4.477 -  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   4.478 -  proof safe
   4.479 -    assume A: "[:c:] * p dvd 1"
   4.480 -    thus "p dvd 1" by (rule dvd_mult_right)
   4.481 -    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
   4.482 -    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
   4.483 -    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
   4.484 -    also note B [symmetric]
   4.485 -    finally show "c dvd 1" by simp
   4.486 -  next
   4.487 -    assume "c dvd 1" "p dvd 1"
   4.488 -    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
   4.489 -    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
   4.490 -    hence "[:c:] dvd 1" by (rule dvdI)
   4.491 -    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
   4.492 -  qed
   4.493 -  finally show ?thesis .
   4.494 -qed
   4.495 -
   4.496 -
   4.497 -subsection \<open>Content and primitive part of a polynomial\<close>
   4.498 -
   4.499 -definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
   4.500 -  "content p = Gcd (set (coeffs p))"
   4.501 -
   4.502 -lemma content_0 [simp]: "content 0 = 0"
   4.503 -  by (simp add: content_def)
   4.504 -
   4.505 -lemma content_1 [simp]: "content 1 = 1"
   4.506 -  by (simp add: content_def)
   4.507 -
   4.508 -lemma content_const [simp]: "content [:c:] = normalize c"
   4.509 -  by (simp add: content_def cCons_def)
   4.510 -
   4.511 -lemma const_poly_dvd_iff_dvd_content:
   4.512 -  fixes c :: "'a :: semiring_Gcd"
   4.513 -  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
   4.514 -proof (cases "p = 0")
   4.515 -  case [simp]: False
   4.516 -  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
   4.517 -  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
   4.518 -  proof safe
   4.519 -    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
   4.520 -    thus "c dvd coeff p n"
   4.521 -      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
   4.522 -  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
   4.523 -  also have "\<dots> \<longleftrightarrow> c dvd content p"
   4.524 -    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
   4.525 -          dvd_mult_unit_iff lead_coeff_nonzero)
   4.526 -  finally show ?thesis .
   4.527 -qed simp_all
   4.528 -
   4.529 -lemma content_dvd [simp]: "[:content p:] dvd p"
   4.530 -  by (subst const_poly_dvd_iff_dvd_content) simp_all
   4.531 -  
   4.532 -lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
   4.533 -  by (cases "n \<le> degree p") 
   4.534 -     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
   4.535 -
   4.536 -lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
   4.537 -  by (simp add: content_def Gcd_dvd)
   4.538 -
   4.539 -lemma normalize_content [simp]: "normalize (content p) = content p"
   4.540 -  by (simp add: content_def)
   4.541 -
   4.542 -lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
   4.543 -proof
   4.544 -  assume "is_unit (content p)"
   4.545 -  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
   4.546 -  thus "content p = 1" by simp
   4.547 -qed auto
   4.548 -
   4.549 -lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
   4.550 -  by (simp add: content_def coeffs_smult Gcd_mult)
   4.551 -
   4.552 -lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   4.553 -  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
   4.554 -
   4.555 -definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
   4.556 -  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
   4.557 -  
   4.558 -lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
   4.559 -  by (simp add: primitive_part_def)
   4.560 -
   4.561 -lemma content_times_primitive_part [simp]:
   4.562 -  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
   4.563 -  shows "smult (content p) (primitive_part p) = p"
   4.564 -proof (cases "p = 0")
   4.565 -  case False
   4.566 -  thus ?thesis
   4.567 -  unfolding primitive_part_def
   4.568 -  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
   4.569 -           intro: map_poly_idI)
   4.570 -qed simp_all
   4.571 -
   4.572 -lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   4.573 -proof (cases "p = 0")
   4.574 -  case False
   4.575 -  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   4.576 -    by (simp add:  primitive_part_def)
   4.577 -  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   4.578 -    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   4.579 -  finally show ?thesis using False by simp
   4.580 -qed simp
   4.581 -
   4.582 -lemma content_primitive_part [simp]:
   4.583 -  assumes "p \<noteq> 0"
   4.584 -  shows   "content (primitive_part p) = 1"
   4.585 -proof -
   4.586 -  have "p = smult (content p) (primitive_part p)" by simp
   4.587 -  also have "content \<dots> = content p * content (primitive_part p)" 
   4.588 -    by (simp del: content_times_primitive_part)
   4.589 -  finally show ?thesis using assms by simp
   4.590 -qed
   4.591 -
   4.592 -lemma content_decompose:
   4.593 -  fixes p :: "'a :: semiring_Gcd poly"
   4.594 -  obtains p' where "p = smult (content p) p'" "content p' = 1"
   4.595 -proof (cases "p = 0")
   4.596 -  case True
   4.597 -  thus ?thesis by (intro that[of 1]) simp_all
   4.598 -next
   4.599 -  case False
   4.600 -  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
   4.601 -  have "content p * 1 = content p * content r" by (subst r) simp
   4.602 -  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
   4.603 -  with r show ?thesis by (intro that[of r]) simp_all
   4.604 -qed
   4.605 -
   4.606 -lemma smult_content_normalize_primitive_part [simp]:
   4.607 -  "smult (content p) (normalize (primitive_part p)) = normalize p"
   4.608 -proof -
   4.609 -  have "smult (content p) (normalize (primitive_part p)) = 
   4.610 -          normalize ([:content p:] * primitive_part p)" 
   4.611 -    by (subst normalize_mult) (simp_all add: normalize_const_poly)
   4.612 -  also have "[:content p:] * primitive_part p = p" by simp
   4.613 -  finally show ?thesis .
   4.614 -qed
   4.615 -
   4.616 -lemma content_dvd_contentI [intro]:
   4.617 -  "p dvd q \<Longrightarrow> content p dvd content q"
   4.618 -  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   4.619 -  
   4.620 -lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   4.621 -  by (simp add: primitive_part_def map_poly_pCons)
   4.622 - 
   4.623 -lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   4.624 -  by (auto simp: primitive_part_def)
   4.625 -  
   4.626 -lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   4.627 -proof (cases "p = 0")
   4.628 -  case False
   4.629 -  have "p = smult (content p) (primitive_part p)" by simp
   4.630 -  also from False have "degree \<dots> = degree (primitive_part p)"
   4.631 -    by (subst degree_smult_eq) simp_all
   4.632 -  finally show ?thesis ..
   4.633 -qed simp_all
   4.634 -
   4.635 -
   4.636 -subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
   4.637 -
   4.638 -abbreviation (input) fract_poly 
   4.639 -  where "fract_poly \<equiv> map_poly to_fract"
   4.640 -
   4.641 -abbreviation (input) unfract_poly 
   4.642 -  where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
   4.643 -  
   4.644 -lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
   4.645 -  by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
   4.646 -
   4.647 -lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
   4.648 -  by (simp add: poly_eqI coeff_map_poly)
   4.649 -
   4.650 -lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
   4.651 -  by (simp add: one_poly_def map_poly_pCons)
   4.652 -
   4.653 -lemma fract_poly_add [simp]:
   4.654 -  "fract_poly (p + q) = fract_poly p + fract_poly q"
   4.655 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   4.656 -
   4.657 -lemma fract_poly_diff [simp]:
   4.658 -  "fract_poly (p - q) = fract_poly p - fract_poly q"
   4.659 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   4.660 -
   4.661 -lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A"
   4.662 -  by (cases "finite A", induction A rule: finite_induct) simp_all 
   4.663 -
   4.664 -lemma fract_poly_mult [simp]:
   4.665 -  "fract_poly (p * q) = fract_poly p * fract_poly q"
   4.666 -  by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
   4.667 -
   4.668 -lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
   4.669 -  by (auto simp: poly_eq_iff coeff_map_poly)
   4.670 -
   4.671 -lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
   4.672 -  using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
   4.673 -
   4.674 -lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
   4.675 -  by (auto elim!: dvdE)
   4.676 -
   4.677 -lemma msetprod_fract_poly: 
   4.678 -  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
   4.679 -  by (induction A) (simp_all add: mult_ac)
   4.680 -  
   4.681 -lemma is_unit_fract_poly_iff:
   4.682 -  "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
   4.683 -proof safe
   4.684 -  assume A: "p dvd 1"
   4.685 -  with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
   4.686 -  from A show "content p = 1"
   4.687 -    by (auto simp: is_unit_poly_iff normalize_1_iff)
   4.688 -next
   4.689 -  assume A: "fract_poly p dvd 1" and B: "content p = 1"
   4.690 -  from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
   4.691 -  {
   4.692 -    fix n :: nat assume "n > 0"
   4.693 -    have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
   4.694 -    also note c
   4.695 -    also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
   4.696 -    finally have "coeff p n = 0" by simp
   4.697 -  }
   4.698 -  hence "degree p \<le> 0" by (intro degree_le) simp_all
   4.699 -  with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
   4.700 -qed
   4.701 -  
   4.702 -lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
   4.703 -  using fract_poly_dvd[of p 1] by simp
   4.704 -
   4.705 -lemma fract_poly_smult_eqE:
   4.706 -  fixes c :: "'a :: {idom_divide,ring_gcd} fract"
   4.707 -  assumes "fract_poly p = smult c (fract_poly q)"
   4.708 -  obtains a b 
   4.709 -    where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
   4.710 -proof -
   4.711 -  define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
   4.712 -  have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
   4.713 -    by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
   4.714 -  hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
   4.715 -  hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
   4.716 -  moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
   4.717 -    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
   4.718 -          normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
   4.719 -  ultimately show ?thesis by (intro that[of a b])
   4.720 -qed
   4.721 -
   4.722 -
   4.723 -subsection \<open>Fractional content\<close>
   4.724 -
   4.725 -abbreviation (input) Lcm_coeff_denoms 
   4.726 -    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
   4.727 -  where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
   4.728 -  
   4.729 -definition fract_content :: 
   4.730 -      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
   4.731 -  "fract_content p = 
   4.732 -     (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
   4.733 -
   4.734 -definition primitive_part_fract :: 
   4.735 -      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
   4.736 -  "primitive_part_fract p = 
   4.737 -     primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
   4.738 -
   4.739 -lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
   4.740 -  by (simp add: primitive_part_fract_def)
   4.741 -
   4.742 -lemma fract_content_eq_0_iff [simp]:
   4.743 -  "fract_content p = 0 \<longleftrightarrow> p = 0"
   4.744 -  unfolding fract_content_def Let_def Zero_fract_def
   4.745 -  by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
   4.746 -
   4.747 -lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
   4.748 -  unfolding primitive_part_fract_def
   4.749 -  by (rule content_primitive_part)
   4.750 -     (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
   4.751 -
   4.752 -lemma content_times_primitive_part_fract:
   4.753 -  "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
   4.754 -proof -
   4.755 -  define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
   4.756 -  have "fract_poly p' = 
   4.757 -          map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
   4.758 -    unfolding primitive_part_fract_def p'_def 
   4.759 -    by (subst map_poly_map_poly) (simp_all add: o_assoc)
   4.760 -  also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
   4.761 -  proof (intro map_poly_idI, unfold o_apply)
   4.762 -    fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
   4.763 -    then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
   4.764 -      by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
   4.765 -    note c(2)
   4.766 -    also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   4.767 -      by simp
   4.768 -    also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
   4.769 -                 Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
   4.770 -      unfolding to_fract_def by (subst mult_fract) simp_all
   4.771 -    also have "snd (quot_of_fract \<dots>) = 1"
   4.772 -      by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
   4.773 -    finally show "to_fract (fst (quot_of_fract c)) = c"
   4.774 -      by (rule to_fract_quot_of_fract)
   4.775 -  qed
   4.776 -  also have "p' = smult (content p') (primitive_part p')" 
   4.777 -    by (rule content_times_primitive_part [symmetric])
   4.778 -  also have "primitive_part p' = primitive_part_fract p"
   4.779 -    by (simp add: primitive_part_fract_def p'_def)
   4.780 -  also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
   4.781 -               smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
   4.782 -  finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
   4.783 -                      smult (to_fract (Lcm_coeff_denoms p)) p" .
   4.784 -  thus ?thesis
   4.785 -    by (subst (asm) smult_eq_iff)
   4.786 -       (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
   4.787 -qed
   4.788 -
   4.789 -lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
   4.790 -proof -
   4.791 -  have "Lcm_coeff_denoms (fract_poly p) = 1"
   4.792 -    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
   4.793 -  hence "fract_content (fract_poly p) = 
   4.794 -           to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
   4.795 -    by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
   4.796 -  also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
   4.797 -    by (intro map_poly_idI) simp_all
   4.798 -  finally show ?thesis .
   4.799 -qed
   4.800 -
   4.801 -lemma content_decompose_fract:
   4.802 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
   4.803 -  obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
   4.804 -proof (cases "p = 0")
   4.805 -  case True
   4.806 -  hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
   4.807 -  thus ?thesis ..
   4.808 -next
   4.809 -  case False
   4.810 -  thus ?thesis
   4.811 -    by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
   4.812 -qed
   4.813 -
   4.814 -
   4.815 -subsection \<open>More properties of content and primitive part\<close>
   4.816 -
   4.817 -lemma lift_prime_elem_poly:
   4.818 -  assumes "prime_elem (c :: 'a :: semidom)"
   4.819 -  shows   "prime_elem [:c:]"
   4.820 -proof (rule prime_elemI)
   4.821 -  fix a b assume *: "[:c:] dvd a * b"
   4.822 -  from * have dvd: "c dvd coeff (a * b) n" for n
   4.823 -    by (subst (asm) const_poly_dvd_iff) blast
   4.824 -  {
   4.825 -    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
   4.826 -    assume "\<not>[:c:] dvd b"
   4.827 -    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
   4.828 -    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
   4.829 -      by (auto intro: le_degree simp: less_Suc_eq_le)
   4.830 -    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
   4.831 -    have "i \<le> m" if "\<not>c dvd coeff b i" for i
   4.832 -      unfolding m_def by (rule Greatest_le[OF that B])
   4.833 -    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
   4.834 -
   4.835 -    have "c dvd coeff a i" for i
   4.836 -    proof (induction i rule: nat_descend_induct[of "degree a"])
   4.837 -      case (base i)
   4.838 -      thus ?case by (simp add: coeff_eq_0)
   4.839 -    next
   4.840 -      case (descend i)
   4.841 -      let ?A = "{..i+m} - {i}"
   4.842 -      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
   4.843 -      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
   4.844 -        by (simp add: coeff_mult)
   4.845 -      also have "{..i+m} = insert i ?A" by auto
   4.846 -      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
   4.847 -                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
   4.848 -        (is "_ = _ + ?S")
   4.849 -        by (subst setsum.insert) simp_all
   4.850 -      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
   4.851 -      moreover have "c dvd ?S"
   4.852 -      proof (rule dvd_setsum)
   4.853 -        fix k assume k: "k \<in> {..i+m} - {i}"
   4.854 -        show "c dvd coeff a k * coeff b (i + m - k)"
   4.855 -        proof (cases "k < i")
   4.856 -          case False
   4.857 -          with k have "c dvd coeff a k" by (intro descend.IH) simp
   4.858 -          thus ?thesis by simp
   4.859 -        next
   4.860 -          case True
   4.861 -          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
   4.862 -          thus ?thesis by simp
   4.863 -        qed
   4.864 -      qed
   4.865 -      ultimately have "c dvd coeff a i * coeff b m"
   4.866 -        by (simp add: dvd_add_left_iff)
   4.867 -      with assms coeff_m show "c dvd coeff a i"
   4.868 -        by (simp add: prime_elem_dvd_mult_iff)
   4.869 -    qed
   4.870 -    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
   4.871 -  }
   4.872 -  thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
   4.873 -qed (insert assms, simp_all add: prime_elem_def one_poly_def)
   4.874 -
   4.875 -lemma prime_elem_const_poly_iff:
   4.876 -  fixes c :: "'a :: semidom"
   4.877 -  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
   4.878 -proof
   4.879 -  assume A: "prime_elem [:c:]"
   4.880 -  show "prime_elem c"
   4.881 -  proof (rule prime_elemI)
   4.882 -    fix a b assume "c dvd a * b"
   4.883 -    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
   4.884 -    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
   4.885 -    thus "c dvd a \<or> c dvd b" by simp
   4.886 -  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
   4.887 -qed (auto intro: lift_prime_elem_poly)
   4.888 -
   4.889 -context
   4.890 -begin
   4.891 -
   4.892 -private lemma content_1_mult:
   4.893 -  fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
   4.894 -  assumes "content f = 1" "content g = 1"
   4.895 -  shows   "content (f * g) = 1"
   4.896 -proof (cases "f * g = 0")
   4.897 -  case False
   4.898 -  from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
   4.899 -
   4.900 -  hence "f * g \<noteq> 0" by auto
   4.901 -  {
   4.902 -    assume "\<not>is_unit (content (f * g))"
   4.903 -    with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
   4.904 -      by (intro prime_divisor_exists) simp_all
   4.905 -    then obtain p where "p dvd content (f * g)" "prime p" by blast
   4.906 -    from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
   4.907 -      by (simp add: const_poly_dvd_iff_dvd_content)
   4.908 -    moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
   4.909 -    ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
   4.910 -      by (simp add: prime_elem_dvd_mult_iff)
   4.911 -    with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
   4.912 -    with \<open>prime p\<close> have False by simp
   4.913 -  }
   4.914 -  hence "is_unit (content (f * g))" by blast
   4.915 -  hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
   4.916 -  thus ?thesis by simp
   4.917 -qed (insert assms, auto)
   4.918 -
   4.919 -lemma content_mult:
   4.920 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   4.921 -  shows "content (p * q) = content p * content q"
   4.922 -proof -
   4.923 -  from content_decompose[of p] guess p' . note p = this
   4.924 -  from content_decompose[of q] guess q' . note q = this
   4.925 -  have "content (p * q) = content p * content q * content (p' * q')"
   4.926 -    by (subst p, subst q) (simp add: mult_ac normalize_mult)
   4.927 -  also from p q have "content (p' * q') = 1" by (intro content_1_mult)
   4.928 -  finally show ?thesis by simp
   4.929 -qed
   4.930 -
   4.931 -lemma primitive_part_mult:
   4.932 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   4.933 -  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
   4.934 -proof -
   4.935 -  have "primitive_part (p * q) = p * q div [:content (p * q):]"
   4.936 -    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   4.937 -  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
   4.938 -    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
   4.939 -  also have "\<dots> = primitive_part p * primitive_part q"
   4.940 -    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   4.941 -  finally show ?thesis .
   4.942 -qed
   4.943 -
   4.944 -lemma primitive_part_smult:
   4.945 -  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   4.946 -  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
   4.947 -proof -
   4.948 -  have "smult a p = [:a:] * p" by simp
   4.949 -  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
   4.950 -    by (subst primitive_part_mult) simp_all
   4.951 -  finally show ?thesis .
   4.952 -qed  
   4.953 -
   4.954 -lemma primitive_part_dvd_primitive_partI [intro]:
   4.955 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   4.956 -  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
   4.957 -  by (auto elim!: dvdE simp: primitive_part_mult)
   4.958 -
   4.959 -lemma content_msetprod: 
   4.960 -  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
   4.961 -  shows "content (msetprod A) = msetprod (image_mset content A)"
   4.962 -  by (induction A) (simp_all add: content_mult mult_ac)
   4.963 -
   4.964 -lemma fract_poly_dvdD:
   4.965 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   4.966 -  assumes "fract_poly p dvd fract_poly q" "content p = 1"
   4.967 -  shows   "p dvd q"
   4.968 -proof -
   4.969 -  from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
   4.970 -  from content_decompose_fract[of r] guess c r' . note r' = this
   4.971 -  from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
   4.972 -  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
   4.973 -  have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
   4.974 -  hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
   4.975 -  have "1 = gcd a (normalize b)" by (simp add: ab)
   4.976 -  also note eq'
   4.977 -  also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
   4.978 -  finally have [simp]: "a = 1" by simp
   4.979 -  from eq ab have "q = p * ([:b:] * r')" by simp
   4.980 -  thus ?thesis by (rule dvdI)
   4.981 -qed
   4.982 -
   4.983 -lemma content_prod_eq_1_iff: 
   4.984 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   4.985 -  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
   4.986 -proof safe
   4.987 -  assume A: "content (p * q) = 1"
   4.988 -  {
   4.989 -    fix p q :: "'a poly" assume "content p * content q = 1"
   4.990 -    hence "1 = content p * content q" by simp
   4.991 -    hence "content p dvd 1" by (rule dvdI)
   4.992 -    hence "content p = 1" by simp
   4.993 -  } note B = this
   4.994 -  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
   4.995 -    by (simp_all add: content_mult mult_ac)
   4.996 -qed (auto simp: content_mult)
   4.997 -
   4.998 -end
   4.999 -
  4.1000 -
  4.1001 -subsection \<open>Polynomials over a field are a Euclidean ring\<close>
  4.1002 -
  4.1003 -context
  4.1004 -begin
  4.1005 -
  4.1006 -private definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
  4.1007 -  "unit_factor_field_poly p = [:lead_coeff p:]"
  4.1008 -
  4.1009 -private definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
  4.1010 -  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
  4.1011 -
  4.1012 -private definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
  4.1013 -  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
  4.1014 -
  4.1015 -private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
  4.1016 -    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
  4.1017 -
  4.1018 -interpretation field_poly: 
  4.1019 -  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" 
  4.1020 -    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
  4.1021 -proof (standard, unfold dvd_field_poly)
  4.1022 -  fix p :: "'a poly"
  4.1023 -  show "unit_factor_field_poly p * normalize_field_poly p = p"
  4.1024 -    by (cases "p = 0") 
  4.1025 -       (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
  4.1026 -next
  4.1027 -  fix p :: "'a poly" assume "is_unit p"
  4.1028 -  thus "normalize_field_poly p = 1"
  4.1029 -    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
  4.1030 -next
  4.1031 -  fix p :: "'a poly" assume "p \<noteq> 0"
  4.1032 -  thus "is_unit (unit_factor_field_poly p)"
  4.1033 -    by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
  4.1034 -qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
  4.1035 -       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
  4.1036 -
  4.1037 -private lemma field_poly_irreducible_imp_prime:
  4.1038 -  assumes "irreducible (p :: 'a :: field poly)"
  4.1039 -  shows   "prime_elem p"
  4.1040 -proof -
  4.1041 -  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
  4.1042 -  from field_poly.irreducible_imp_prime_elem[of p] assms
  4.1043 -    show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
  4.1044 -      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
  4.1045 -qed
  4.1046 -
  4.1047 -private lemma field_poly_msetprod_prime_factorization:
  4.1048 -  assumes "(x :: 'a :: field poly) \<noteq> 0"
  4.1049 -  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
  4.1050 -proof -
  4.1051 -  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
  4.1052 -  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
  4.1053 -    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
  4.1054 -  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
  4.1055 -qed
  4.1056 -
  4.1057 -private lemma field_poly_in_prime_factorization_imp_prime:
  4.1058 -  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
  4.1059 -  shows   "prime_elem p"
  4.1060 -proof -
  4.1061 -  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
  4.1062 -  have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
  4.1063 -             normalize_field_poly unit_factor_field_poly" ..
  4.1064 -  from field_poly.in_prime_factorization_imp_prime[of p x] assms
  4.1065 -    show ?thesis unfolding prime_elem_def dvd_field_poly
  4.1066 -      comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
  4.1067 -qed
  4.1068 -
  4.1069 -
  4.1070 -subsection \<open>Primality and irreducibility in polynomial rings\<close>
  4.1071 -
  4.1072 -lemma nonconst_poly_irreducible_iff:
  4.1073 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  4.1074 -  assumes "degree p \<noteq> 0"
  4.1075 -  shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
  4.1076 -proof safe
  4.1077 -  assume p: "irreducible p"
  4.1078 -
  4.1079 -  from content_decompose[of p] guess p' . note p' = this
  4.1080 -  hence "p = [:content p:] * p'" by simp
  4.1081 -  from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
  4.1082 -  moreover have "\<not>p' dvd 1"
  4.1083 -  proof
  4.1084 -    assume "p' dvd 1"
  4.1085 -    hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
  4.1086 -    with assms show False by contradiction
  4.1087 -  qed
  4.1088 -  ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
  4.1089 -  
  4.1090 -  show "irreducible (map_poly to_fract p)"
  4.1091 -  proof (rule irreducibleI)
  4.1092 -    have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
  4.1093 -    with assms show "map_poly to_fract p \<noteq> 0" by auto
  4.1094 -  next
  4.1095 -    show "\<not>is_unit (fract_poly p)"
  4.1096 -    proof
  4.1097 -      assume "is_unit (map_poly to_fract p)"
  4.1098 -      hence "degree (map_poly to_fract p) = 0"
  4.1099 -        by (auto simp: is_unit_poly_iff)
  4.1100 -      hence "degree p = 0" by (simp add: degree_map_poly)
  4.1101 -      with assms show False by contradiction
  4.1102 -   qed
  4.1103 - next
  4.1104 -   fix q r assume qr: "fract_poly p = q * r"
  4.1105 -   from content_decompose_fract[of q] guess cg q' . note q = this
  4.1106 -   from content_decompose_fract[of r] guess cr r' . note r = this
  4.1107 -   from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
  4.1108 -   from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
  4.1109 -     by (simp add: q r)
  4.1110 -   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
  4.1111 -   hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
  4.1112 -   with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
  4.1113 -   hence "normalize b = gcd a b" by simp
  4.1114 -   also from ab(3) have "\<dots> = 1" .
  4.1115 -   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
  4.1116 -   
  4.1117 -   note eq
  4.1118 -   also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
  4.1119 -   also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
  4.1120 -   finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
  4.1121 -   from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
  4.1122 -   hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
  4.1123 -   hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
  4.1124 -   with q r show "is_unit q \<or> is_unit r"
  4.1125 -     by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
  4.1126 - qed
  4.1127 -
  4.1128 -next
  4.1129 -
  4.1130 -  assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
  4.1131 -  show "irreducible p"
  4.1132 -  proof (rule irreducibleI)
  4.1133 -    from irred show "p \<noteq> 0" by auto
  4.1134 -  next
  4.1135 -    from irred show "\<not>p dvd 1"
  4.1136 -      by (auto simp: irreducible_def dest: fract_poly_is_unit)
  4.1137 -  next
  4.1138 -    fix q r assume qr: "p = q * r"
  4.1139 -    hence "fract_poly p = fract_poly q * fract_poly r" by simp
  4.1140 -    from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
  4.1141 -      by (rule irreducibleD)
  4.1142 -    with primitive qr show "q dvd 1 \<or> r dvd 1"
  4.1143 -      by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
  4.1144 -  qed
  4.1145 -qed
  4.1146 -
  4.1147 -private lemma irreducible_imp_prime_poly:
  4.1148 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  4.1149 -  assumes "irreducible p"
  4.1150 -  shows   "prime_elem p"
  4.1151 -proof (cases "degree p = 0")
  4.1152 -  case True
  4.1153 -  with assms show ?thesis
  4.1154 -    by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
  4.1155 -             intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
  4.1156 -next
  4.1157 -  case False
  4.1158 -  from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
  4.1159 -    by (simp_all add: nonconst_poly_irreducible_iff)
  4.1160 -  from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
  4.1161 -  show ?thesis
  4.1162 -  proof (rule prime_elemI)
  4.1163 -    fix q r assume "p dvd q * r"
  4.1164 -    hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
  4.1165 -    hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
  4.1166 -    from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
  4.1167 -      by (rule prime_elem_dvd_multD)
  4.1168 -    with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
  4.1169 -  qed (insert assms, auto simp: irreducible_def)
  4.1170 -qed
  4.1171 -
  4.1172 -
  4.1173 -lemma degree_primitive_part_fract [simp]:
  4.1174 -  "degree (primitive_part_fract p) = degree p"
  4.1175 -proof -
  4.1176 -  have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
  4.1177 -    by (simp add: content_times_primitive_part_fract)
  4.1178 -  also have "degree \<dots> = degree (primitive_part_fract p)"
  4.1179 -    by (auto simp: degree_map_poly)
  4.1180 -  finally show ?thesis ..
  4.1181 -qed
  4.1182 -
  4.1183 -lemma irreducible_primitive_part_fract:
  4.1184 -  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
  4.1185 -  assumes "irreducible p"
  4.1186 -  shows   "irreducible (primitive_part_fract p)"
  4.1187 -proof -
  4.1188 -  from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
  4.1189 -    by (intro notI) 
  4.1190 -       (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
  4.1191 -  hence [simp]: "p \<noteq> 0" by auto
  4.1192 -
  4.1193 -  note \<open>irreducible p\<close>
  4.1194 -  also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
  4.1195 -    by (simp add: content_times_primitive_part_fract)
  4.1196 -  also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
  4.1197 -    by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
  4.1198 -  finally show ?thesis using deg
  4.1199 -    by (simp add: nonconst_poly_irreducible_iff)
  4.1200 -qed
  4.1201 -
  4.1202 -lemma prime_elem_primitive_part_fract:
  4.1203 -  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
  4.1204 -  shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
  4.1205 -  by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
  4.1206 -
  4.1207 -lemma irreducible_linear_field_poly:
  4.1208 -  fixes a b :: "'a::field"
  4.1209 -  assumes "b \<noteq> 0"
  4.1210 -  shows "irreducible [:a,b:]"
  4.1211 -proof (rule irreducibleI)
  4.1212 -  fix p q assume pq: "[:a,b:] = p * q"
  4.1213 -  also from pq assms have "degree \<dots> = degree p + degree q" 
  4.1214 -    by (intro degree_mult_eq) auto
  4.1215 -  finally have "degree p = 0 \<or> degree q = 0" using assms by auto
  4.1216 -  with assms pq show "is_unit p \<or> is_unit q"
  4.1217 -    by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
  4.1218 -qed (insert assms, auto simp: is_unit_poly_iff)
  4.1219 -
  4.1220 -lemma prime_elem_linear_field_poly:
  4.1221 -  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
  4.1222 -  by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
  4.1223 -
  4.1224 -lemma irreducible_linear_poly:
  4.1225 -  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
  4.1226 -  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
  4.1227 -  by (auto intro!: irreducible_linear_field_poly 
  4.1228 -           simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
  4.1229 -
  4.1230 -lemma prime_elem_linear_poly:
  4.1231 -  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
  4.1232 -  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
  4.1233 -  by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
  4.1234 -
  4.1235 -  
  4.1236 -subsection \<open>Prime factorisation of polynomials\<close>   
  4.1237 -
  4.1238 -private lemma poly_prime_factorization_exists_content_1:
  4.1239 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  4.1240 -  assumes "p \<noteq> 0" "content p = 1"
  4.1241 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  4.1242 -proof -
  4.1243 -  let ?P = "field_poly.prime_factorization (fract_poly p)"
  4.1244 -  define c where "c = msetprod (image_mset fract_content ?P)"
  4.1245 -  define c' where "c' = c * to_fract (lead_coeff p)"
  4.1246 -  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
  4.1247 -  define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
  4.1248 -  have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
  4.1249 -                      content (primitive_part_fract x))"
  4.1250 -    by (simp add: e_def content_msetprod multiset.map_comp o_def)
  4.1251 -  also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
  4.1252 -    by (intro image_mset_cong content_primitive_part_fract) auto
  4.1253 -  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
  4.1254 -  
  4.1255 -  have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
  4.1256 -          normalize_field_poly (fract_poly p)" by simp
  4.1257 -  also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
  4.1258 -    by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
  4.1259 -  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
  4.1260 -    by (subst field_poly_msetprod_prime_factorization) simp_all
  4.1261 -  also have "\<dots> = msetprod (image_mset id ?P)" by simp
  4.1262 -  also have "image_mset id ?P = 
  4.1263 -               image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
  4.1264 -    by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
  4.1265 -  also have "msetprod \<dots> = smult c (fract_poly e)"
  4.1266 -    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
  4.1267 -  also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
  4.1268 -    by (simp add: c'_def)
  4.1269 -  finally have eq: "fract_poly p = smult c' (fract_poly e)" .
  4.1270 -  also obtain b where b: "c' = to_fract b" "is_unit b"
  4.1271 -  proof -
  4.1272 -    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
  4.1273 -    from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
  4.1274 -    with assms content_e have "a = normalize b" by (simp add: ab(4))
  4.1275 -    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
  4.1276 -    with ab ab' have "c' = to_fract b" by auto
  4.1277 -    from this and \<open>is_unit b\<close> show ?thesis by (rule that)
  4.1278 -  qed
  4.1279 -  hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
  4.1280 -  finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
  4.1281 -  hence "p = [:b:] * e" by simp
  4.1282 -  with b have "normalize p = normalize e" 
  4.1283 -    by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
  4.1284 -  also have "normalize e = msetprod A"
  4.1285 -    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
  4.1286 -  finally have "msetprod A = normalize p" ..
  4.1287 -  
  4.1288 -  have "prime_elem p" if "p \<in># A" for p
  4.1289 -    using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
  4.1290 -                        dest!: field_poly_in_prime_factorization_imp_prime )
  4.1291 -  from this and \<open>msetprod A = normalize p\<close> show ?thesis
  4.1292 -    by (intro exI[of _ A]) blast
  4.1293 -qed
  4.1294 -
  4.1295 -lemma poly_prime_factorization_exists:
  4.1296 -  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  4.1297 -  assumes "p \<noteq> 0"
  4.1298 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  4.1299 -proof -
  4.1300 -  define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
  4.1301 -  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
  4.1302 -    by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
  4.1303 -  then guess A by (elim exE conjE) note A = this
  4.1304 -  moreover from assms have "msetprod B = [:content p:]"
  4.1305 -    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
  4.1306 -  moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
  4.1307 -    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
  4.1308 -  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
  4.1309 -qed
  4.1310 -
  4.1311 -end
  4.1312 -
  4.1313 -
  4.1314 -subsection \<open>Typeclass instances\<close>
  4.1315 -
  4.1316 -instance poly :: (factorial_ring_gcd) factorial_semiring
  4.1317 -  by standard (rule poly_prime_factorization_exists)  
  4.1318 -
  4.1319 -instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
  4.1320 -begin
  4.1321 -
  4.1322 -definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  4.1323 -  [code del]: "gcd_poly = gcd_factorial"
  4.1324 -
  4.1325 -definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  4.1326 -  [code del]: "lcm_poly = lcm_factorial"
  4.1327 -  
  4.1328 -definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
  4.1329 - [code del]: "Gcd_poly = Gcd_factorial"
  4.1330 -
  4.1331 -definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
  4.1332 - [code del]: "Lcm_poly = Lcm_factorial"
  4.1333 - 
  4.1334 -instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
  4.1335 -
  4.1336 -end
  4.1337 -
  4.1338 -instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
  4.1339 -begin
  4.1340 -
  4.1341 -definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
  4.1342 -  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
  4.1343 -
  4.1344 -instance 
  4.1345 -  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
  4.1346 -end
  4.1347 -
  4.1348 -
  4.1349 -instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
  4.1350 -  by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
  4.1351 -
  4.1352 -  
  4.1353 -subsection \<open>Polynomial GCD\<close>
  4.1354 -
  4.1355 -lemma gcd_poly_decompose:
  4.1356 -  fixes p q :: "'a :: factorial_ring_gcd poly"
  4.1357 -  shows "gcd p q = 
  4.1358 -           smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  4.1359 -proof (rule sym, rule gcdI)
  4.1360 -  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  4.1361 -          [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
  4.1362 -  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
  4.1363 -    by simp
  4.1364 -next
  4.1365 -  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
  4.1366 -          [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
  4.1367 -  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
  4.1368 -    by simp
  4.1369 -next
  4.1370 -  fix d assume "d dvd p" "d dvd q"
  4.1371 -  hence "[:content d:] * primitive_part d dvd 
  4.1372 -           [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
  4.1373 -    by (intro mult_dvd_mono) auto
  4.1374 -  thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
  4.1375 -    by simp
  4.1376 -qed (auto simp: normalize_smult)
  4.1377 -  
  4.1378 -
  4.1379 -lemma gcd_poly_pseudo_mod:
  4.1380 -  fixes p q :: "'a :: factorial_ring_gcd poly"
  4.1381 -  assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
  4.1382 -  shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
  4.1383 -proof -
  4.1384 -  define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
  4.1385 -  define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
  4.1386 -  have [simp]: "primitive_part a = unit_factor a"
  4.1387 -    by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
  4.1388 -  from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
  4.1389 -  
  4.1390 -  have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
  4.1391 -  have "gcd (q * r + s) q = gcd q s"
  4.1392 -    using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
  4.1393 -  with pseudo_divmod(1)[OF nz rs]
  4.1394 -    have "gcd (p * a) q = gcd q s" by (simp add: a_def)
  4.1395 -  also from prim have "gcd (p * a) q = gcd p q"
  4.1396 -    by (subst gcd_poly_decompose)
  4.1397 -       (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
  4.1398 -             simp del: mult_pCons_right )
  4.1399 -  also from prim have "gcd q s = gcd q (primitive_part s)"
  4.1400 -    by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
  4.1401 -  also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
  4.1402 -  finally show ?thesis .
  4.1403 -qed
  4.1404 -
  4.1405 -lemma degree_pseudo_mod_less:
  4.1406 -  assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
  4.1407 -  shows   "degree (pseudo_mod p q) < degree q"
  4.1408 -  using pseudo_mod(2)[of q p] assms by auto
  4.1409 -
  4.1410 -function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  4.1411 -  "gcd_poly_code_aux p q = 
  4.1412 -     (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
  4.1413 -by auto
  4.1414 -termination
  4.1415 -  by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
  4.1416 -     (auto simp: degree_primitive_part degree_pseudo_mod_less)
  4.1417 -
  4.1418 -declare gcd_poly_code_aux.simps [simp del]
  4.1419 -
  4.1420 -lemma gcd_poly_code_aux_correct:
  4.1421 -  assumes "content p = 1" "q = 0 \<or> content q = 1"
  4.1422 -  shows   "gcd_poly_code_aux p q = gcd p q"
  4.1423 -  using assms
  4.1424 -proof (induction p q rule: gcd_poly_code_aux.induct)
  4.1425 -  case (1 p q)
  4.1426 -  show ?case
  4.1427 -  proof (cases "q = 0")
  4.1428 -    case True
  4.1429 -    thus ?thesis by (subst gcd_poly_code_aux.simps) auto
  4.1430 -  next
  4.1431 -    case False
  4.1432 -    hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
  4.1433 -      by (subst gcd_poly_code_aux.simps) simp_all
  4.1434 -    also from "1.prems" False 
  4.1435 -      have "primitive_part (pseudo_mod p q) = 0 \<or> 
  4.1436 -              content (primitive_part (pseudo_mod p q)) = 1"
  4.1437 -      by (cases "pseudo_mod p q = 0") auto
  4.1438 -    with "1.prems" False 
  4.1439 -      have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
  4.1440 -              gcd q (primitive_part (pseudo_mod p q))"
  4.1441 -      by (intro 1) simp_all
  4.1442 -    also from "1.prems" False 
  4.1443 -      have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
  4.1444 -    finally show ?thesis .
  4.1445 -  qed
  4.1446 -qed
  4.1447 -
  4.1448 -definition gcd_poly_code 
  4.1449 -    :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
  4.1450 -  where "gcd_poly_code p q = 
  4.1451 -           (if p = 0 then normalize q else if q = 0 then normalize p else
  4.1452 -              smult (gcd (content p) (content q)) 
  4.1453 -                (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
  4.1454 -
  4.1455 -lemma lcm_poly_code [code]: 
  4.1456 -  fixes p q :: "'a :: factorial_ring_gcd poly"
  4.1457 -  shows "lcm p q = normalize (p * q) div gcd p q"
  4.1458 -  by (rule lcm_gcd)
  4.1459 -
  4.1460 -lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
  4.1461 -  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
  4.1462 -
  4.1463 -declare Gcd_set
  4.1464 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
  4.1465 -
  4.1466 -declare Lcm_set
  4.1467 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
  4.1468 -  
  4.1469 -value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
  4.1470 -
  4.1471 -end