tuned structure
authorhaftmann
Thu Jan 05 17:11:21 2017 +0100 (2017-01-05)
changeset 647958e7db8df16a0
parent 64794 6f7391f28197
child 64809 a0e1f64be67c
tuned structure
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_Factorial.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Thu Jan 05 14:49:21 2017 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Jan 05 17:11:21 2017 +0100
     1.3 @@ -12,6 +12,21 @@
     1.4    "~~/src/HOL/Library/Infinite_Set"
     1.5  begin
     1.6  
     1.7 +subsection \<open>Misc\<close>
     1.8 +
     1.9 +lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
    1.10 +  using quotient_of_denom_pos [OF surjective_pairing] .
    1.11 +  
    1.12 +lemma of_int_divide_in_Ints: 
    1.13 +  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: idom_divide set)"
    1.14 +proof (cases "of_int b = (0 :: 'a)")
    1.15 +  case False
    1.16 +  assume "b dvd a"
    1.17 +  then obtain c where "a = b * c" ..
    1.18 +  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
    1.19 +qed auto
    1.20 +
    1.21 +  
    1.22  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    1.23  
    1.24  definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
    1.25 @@ -143,6 +158,33 @@
    1.26    "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
    1.27    by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
    1.28  
    1.29 +lemma eq_zero_or_degree_less:
    1.30 +  assumes "degree p \<le> n" and "coeff p n = 0"
    1.31 +  shows "p = 0 \<or> degree p < n"
    1.32 +proof (cases n)
    1.33 +  case 0
    1.34 +  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close>
    1.35 +  have "coeff p (degree p) = 0" by simp
    1.36 +  then have "p = 0" by simp
    1.37 +  then show ?thesis ..
    1.38 +next
    1.39 +  case (Suc m)
    1.40 +  have "\<forall>i>n. coeff p i = 0"
    1.41 +    using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0)
    1.42 +  then have "\<forall>i\<ge>n. coeff p i = 0"
    1.43 +    using \<open>coeff p n = 0\<close> by (simp add: le_less)
    1.44 +  then have "\<forall>i>m. coeff p i = 0"
    1.45 +    using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le)
    1.46 +  then have "degree p \<le> m"
    1.47 +    by (rule degree_le)
    1.48 +  then have "degree p < n"
    1.49 +    using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le)
    1.50 +  then show ?thesis ..
    1.51 +qed
    1.52 +
    1.53 +lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr - 1"
    1.54 +  using eq_zero_or_degree_less by fastforce
    1.55 +
    1.56  
    1.57  subsection \<open>List-style constructor for polynomials\<close>
    1.58  
    1.59 @@ -481,6 +523,7 @@
    1.60    "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
    1.61    by (simp add: fold_coeffs_def)
    1.62  
    1.63 +
    1.64  subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
    1.65  
    1.66  definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
    1.67 @@ -572,8 +615,22 @@
    1.68    
    1.69  lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
    1.70    using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
    1.71 -  
    1.72 -    
    1.73 +
    1.74 +
    1.75 +subsection \<open>Leading coefficient\<close>
    1.76 +
    1.77 +abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a"
    1.78 +  where "lead_coeff p \<equiv> coeff p (degree p)"
    1.79 +
    1.80 +lemma lead_coeff_pCons[simp]:
    1.81 +  "p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p"
    1.82 +  "p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a"
    1.83 +  by auto
    1.84 +
    1.85 +lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
    1.86 +  by (cases "c = 0") (simp_all add: degree_monom_eq)
    1.87 +
    1.88 +
    1.89  subsection \<open>Addition and subtraction\<close>
    1.90  
    1.91  instantiation poly :: (comm_monoid_add) comm_monoid_add
    1.92 @@ -694,6 +751,16 @@
    1.93    "degree (- p) = degree p"
    1.94    unfolding degree_def by simp
    1.95  
    1.96 +lemma lead_coeff_add_le:
    1.97 +  assumes "degree p < degree q"
    1.98 +  shows "lead_coeff (p + q) = lead_coeff q" 
    1.99 +  using assms
   1.100 +  by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   1.101 +
   1.102 +lemma lead_coeff_minus:
   1.103 +  "lead_coeff (- p) = - lead_coeff p"
   1.104 +  by (metis coeff_minus degree_minus)
   1.105 +
   1.106  lemma degree_diff_le_max:
   1.107    fixes p q :: "'a :: ab_group_add poly"
   1.108    shows "degree (p - q) \<le> max (degree p) (degree q)"
   1.109 @@ -894,7 +961,16 @@
   1.110    shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
   1.111    by (rule coeffs_eqI)
   1.112      (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
   1.113 -   
   1.114 +
   1.115 +lemma smult_eq_iff:
   1.116 +  assumes "(b :: 'a :: field) \<noteq> 0"
   1.117 +  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   1.118 +proof
   1.119 +  assume "smult a p = smult b q"
   1.120 +  also from assms have "smult (inverse b) \<dots> = q" by simp
   1.121 +  finally show "smult (a / b) p = q" by (simp add: field_simps)
   1.122 +qed (insert assms, auto)
   1.123 +
   1.124  instantiation poly :: (comm_semiring_0) comm_semiring_0
   1.125  begin
   1.126  
   1.127 @@ -1037,6 +1113,10 @@
   1.128    "degree (p ^ n) \<le> degree p * n"
   1.129    by (induct n) (auto intro: order_trans degree_mult_le)
   1.130  
   1.131 +lemma coeff_0_power:
   1.132 +  "coeff (p ^ n) 0 = coeff p 0 ^ n"
   1.133 +  by (induction n) (simp_all add: coeff_mult)
   1.134 +
   1.135  lemma poly_smult [simp]:
   1.136    "poly (smult a p) x = a * poly p x"
   1.137    by (induct p, simp, simp add: algebra_simps)
   1.138 @@ -1064,6 +1144,40 @@
   1.139      by (rule le_trans[OF degree_mult_le], insert insert, auto)
   1.140  qed simp
   1.141  
   1.142 +lemma coeff_0_prod_list:
   1.143 +  "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
   1.144 +  by (induction xs) (simp_all add: coeff_mult)
   1.145 +
   1.146 +lemma coeff_monom_mult: 
   1.147 +  "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
   1.148 +proof -
   1.149 +  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
   1.150 +    by (simp add: coeff_mult)
   1.151 +  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
   1.152 +    by (intro sum.cong) simp_all
   1.153 +  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))" by (simp add: sum.delta')
   1.154 +  finally show ?thesis .
   1.155 +qed
   1.156 +
   1.157 +lemma monom_1_dvd_iff':
   1.158 +  "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
   1.159 +proof
   1.160 +  assume "monom 1 n dvd p"
   1.161 +  then obtain r where r: "p = monom 1 n * r" by (elim dvdE)
   1.162 +  thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult)
   1.163 +next
   1.164 +  assume zero: "(\<forall>k<n. coeff p k = 0)"
   1.165 +  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
   1.166 +  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
   1.167 +    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 
   1.168 +        subst cofinite_eq_sequentially [symmetric]) transfer
   1.169 +  hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def
   1.170 +    by (subst poly.Abs_poly_inverse) simp_all
   1.171 +  have "p = monom 1 n * r"
   1.172 +    by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all)
   1.173 +  thus "monom 1 n dvd p" by simp
   1.174 +qed
   1.175 +
   1.176  
   1.177  subsection \<open>Mapping polynomials\<close>
   1.178  
   1.179 @@ -1185,10 +1299,18 @@
   1.180  lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
   1.181    by (simp add: of_nat_poly)
   1.182  
   1.183 -lemma of_int_poly: "of_int n = [:of_int n :: 'a :: comm_ring_1:]"
   1.184 +lemma lead_coeff_of_nat [simp]:
   1.185 +  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
   1.186 +  by (simp add: of_nat_poly)
   1.187 +
   1.188 +lemma of_int_poly: "of_int k = [:of_int k :: 'a :: comm_ring_1:]"
   1.189    by (simp only: of_int_of_nat of_nat_poly) simp
   1.190  
   1.191 -lemma degree_of_int [simp]: "degree (of_int n) = 0"
   1.192 +lemma degree_of_int [simp]: "degree (of_int k) = 0"
   1.193 +  by (simp add: of_int_poly)
   1.194 +
   1.195 +lemma lead_coeff_of_int [simp]:
   1.196 +  "lead_coeff (of_int k) = (of_int k :: 'a :: {comm_ring_1,ring_char_0})"
   1.197    by (simp add: of_int_poly)
   1.198  
   1.199  lemma numeral_poly: "numeral n = [:numeral n:]"
   1.200 @@ -1197,6 +1319,10 @@
   1.201  lemma degree_numeral [simp]: "degree (numeral n) = 0"
   1.202    by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   1.203  
   1.204 +lemma lead_coeff_numeral [simp]: 
   1.205 +  "lead_coeff (numeral n) = numeral n"
   1.206 +  by (simp add: numeral_poly)
   1.207 +
   1.208  
   1.209  subsection \<open>Lemmas about divisibility\<close>
   1.210  
   1.211 @@ -1237,6 +1363,28 @@
   1.212    shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
   1.213    by (auto elim: smult_dvd smult_dvd_cancel)
   1.214  
   1.215 +lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   1.216 +proof -
   1.217 +  have "smult c p = [:c:] * p" by simp
   1.218 +  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   1.219 +  proof safe
   1.220 +    assume A: "[:c:] * p dvd 1"
   1.221 +    thus "p dvd 1" by (rule dvd_mult_right)
   1.222 +    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
   1.223 +    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
   1.224 +    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
   1.225 +    also note B [symmetric]
   1.226 +    finally show "c dvd 1" by simp
   1.227 +  next
   1.228 +    assume "c dvd 1" "p dvd 1"
   1.229 +    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
   1.230 +    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
   1.231 +    hence "[:c:] dvd 1" by (rule dvdI)
   1.232 +    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
   1.233 +  qed
   1.234 +  finally show ?thesis .
   1.235 +qed
   1.236 +
   1.237  
   1.238  subsection \<open>Polynomials form an integral domain\<close>
   1.239  
   1.240 @@ -1302,6 +1450,27 @@
   1.241    "[:a::'a::{comm_semiring_1,semiring_no_zero_divisors}:] dvd [:b:] \<longleftrightarrow> a dvd b"
   1.242    by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)
   1.243  
   1.244 +lemma lead_coeff_mult:
   1.245 +  fixes p q :: "'a :: {comm_semiring_0, semiring_no_zero_divisors} poly"
   1.246 +  shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
   1.247 +  by (cases "p=0 \<or> q=0", auto simp add:coeff_mult_degree_sum degree_mult_eq)
   1.248 +
   1.249 +lemma lead_coeff_smult:
   1.250 +  "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
   1.251 +proof -
   1.252 +  have "smult c p = [:c:] * p" by simp
   1.253 +  also have "lead_coeff \<dots> = c * lead_coeff p"
   1.254 +    by (subst lead_coeff_mult) simp_all
   1.255 +  finally show ?thesis .
   1.256 +qed
   1.257 +
   1.258 +lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   1.259 +  by simp
   1.260 +
   1.261 +lemma lead_coeff_power: 
   1.262 +  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
   1.263 +  by (induction n) (simp_all add: lead_coeff_mult)
   1.264 +
   1.265  
   1.266  subsection \<open>Polynomials form an ordered integral domain\<close>
   1.267  
   1.268 @@ -1407,69 +1576,10 @@
   1.269  text \<open>TODO: Simplification rules for comparisons\<close>
   1.270  
   1.271  
   1.272 -subsection \<open>Leading coefficient\<close>
   1.273 -
   1.274 -abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a"
   1.275 -  where "lead_coeff p \<equiv> coeff p (degree p)"
   1.276 -
   1.277 -lemma lead_coeff_pCons[simp]:
   1.278 -  "p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p"
   1.279 -  "p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a"
   1.280 -  by auto
   1.281 -
   1.282 -lemma coeff_0_prod_list:
   1.283 -  "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
   1.284 -  by (induction xs) (simp_all add: coeff_mult)
   1.285 -
   1.286 -lemma coeff_0_power:
   1.287 -  "coeff (p ^ n) 0 = coeff p 0 ^ n"
   1.288 -  by (induction n) (simp_all add: coeff_mult)
   1.289 -
   1.290 -lemma lead_coeff_mult:
   1.291 -  fixes p q :: "'a :: {comm_semiring_0, semiring_no_zero_divisors} poly"
   1.292 -  shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
   1.293 -  by (cases "p=0 \<or> q=0", auto simp add:coeff_mult_degree_sum degree_mult_eq)
   1.294 -
   1.295 -lemma lead_coeff_add_le:
   1.296 -  assumes "degree p < degree q"
   1.297 -  shows "lead_coeff (p + q) = lead_coeff q" 
   1.298 -  using assms
   1.299 -  by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   1.300 -
   1.301 -lemma lead_coeff_minus:
   1.302 -  "lead_coeff (- p) = - lead_coeff p"
   1.303 -  by (metis coeff_minus degree_minus)
   1.304 -
   1.305 -lemma lead_coeff_smult:
   1.306 -  "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
   1.307 -proof -
   1.308 -  have "smult c p = [:c:] * p" by simp
   1.309 -  also have "lead_coeff \<dots> = c * lead_coeff p"
   1.310 -    by (subst lead_coeff_mult) simp_all
   1.311 -  finally show ?thesis .
   1.312 -qed
   1.313 -
   1.314 -lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   1.315 -  by simp
   1.316 -
   1.317 -lemma lead_coeff_of_nat [simp]:
   1.318 -  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
   1.319 -  by (simp add: of_nat_poly)
   1.320 -
   1.321 -lemma lead_coeff_numeral [simp]: 
   1.322 -  "lead_coeff (numeral n) = numeral n"
   1.323 -  by (simp add: numeral_poly)
   1.324 -
   1.325 -lemma lead_coeff_power: 
   1.326 -  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
   1.327 -  by (induction n) (simp_all add: lead_coeff_mult)
   1.328 -
   1.329 -lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   1.330 -  by (cases "c = 0") (simp_all add: degree_monom_eq)
   1.331 -
   1.332 -
   1.333  subsection \<open>Synthetic division and polynomial roots\<close>
   1.334  
   1.335 +subsubsection \<open>Synthetic division\<close>  
   1.336 +  
   1.337  text \<open>
   1.338    Synthetic division is simply division by the linear polynomial @{term "x - c"}.
   1.339  \<close>
   1.340 @@ -1537,9 +1647,12 @@
   1.341    using synthetic_div_correct [of p c]
   1.342    by (simp add: algebra_simps)
   1.343  
   1.344 +    
   1.345 +subsubsection \<open>Polynomial roots\<close>
   1.346 +  
   1.347  lemma poly_eq_0_iff_dvd:
   1.348    fixes c :: "'a::{comm_ring_1}"
   1.349 -  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
   1.350 +  shows "poly p c = 0 \<longleftrightarrow> [:- c, 1:] dvd p"
   1.351  proof
   1.352    assume "poly p c = 0"
   1.353    with synthetic_div_correct' [of c p]
   1.354 @@ -1553,7 +1666,7 @@
   1.355  
   1.356  lemma dvd_iff_poly_eq_0:
   1.357    fixes c :: "'a::{comm_ring_1}"
   1.358 -  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
   1.359 +  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (- c) = 0"
   1.360    by (simp add: poly_eq_0_iff_dvd)
   1.361  
   1.362  lemma poly_roots_finite:
   1.363 @@ -1608,1318 +1721,8 @@
   1.364    shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
   1.365    by (auto simp add: poly_eq_poly_eq_iff [symmetric])
   1.366  
   1.367 -
   1.368 -subsection \<open>Long division of polynomials\<close>
   1.369 -
   1.370 -inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
   1.371 -  where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
   1.372 -  | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
   1.373 -  | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
   1.374 -      \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
   1.375 -  
   1.376 -lemma eucl_rel_poly_iff:
   1.377 -  "eucl_rel_poly x y (q, r) \<longleftrightarrow>
   1.378 -    x = q * y + r \<and>
   1.379 -      (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
   1.380 -  by (auto elim: eucl_rel_poly.cases
   1.381 -    intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
   1.382 -  
   1.383 -lemma eucl_rel_poly_0:
   1.384 -  "eucl_rel_poly 0 y (0, 0)"
   1.385 -  unfolding eucl_rel_poly_iff by simp
   1.386 -
   1.387 -lemma eucl_rel_poly_by_0:
   1.388 -  "eucl_rel_poly x 0 (0, x)"
   1.389 -  unfolding eucl_rel_poly_iff by simp
   1.390 -
   1.391 -lemma eq_zero_or_degree_less:
   1.392 -  assumes "degree p \<le> n" and "coeff p n = 0"
   1.393 -  shows "p = 0 \<or> degree p < n"
   1.394 -proof (cases n)
   1.395 -  case 0
   1.396 -  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close>
   1.397 -  have "coeff p (degree p) = 0" by simp
   1.398 -  then have "p = 0" by simp
   1.399 -  then show ?thesis ..
   1.400 -next
   1.401 -  case (Suc m)
   1.402 -  have "\<forall>i>n. coeff p i = 0"
   1.403 -    using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0)
   1.404 -  then have "\<forall>i\<ge>n. coeff p i = 0"
   1.405 -    using \<open>coeff p n = 0\<close> by (simp add: le_less)
   1.406 -  then have "\<forall>i>m. coeff p i = 0"
   1.407 -    using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le)
   1.408 -  then have "degree p \<le> m"
   1.409 -    by (rule degree_le)
   1.410 -  then have "degree p < n"
   1.411 -    using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le)
   1.412 -  then show ?thesis ..
   1.413 -qed
   1.414 -
   1.415 -lemma eucl_rel_poly_pCons:
   1.416 -  assumes rel: "eucl_rel_poly x y (q, r)"
   1.417 -  assumes y: "y \<noteq> 0"
   1.418 -  assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
   1.419 -  shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
   1.420 -    (is "eucl_rel_poly ?x y (?q, ?r)")
   1.421 -proof -
   1.422 -  have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
   1.423 -    using assms unfolding eucl_rel_poly_iff by simp_all
   1.424 -
   1.425 -  have 1: "?x = ?q * y + ?r"
   1.426 -    using b x by simp
   1.427 -
   1.428 -  have 2: "?r = 0 \<or> degree ?r < degree y"
   1.429 -  proof (rule eq_zero_or_degree_less)
   1.430 -    show "degree ?r \<le> degree y"
   1.431 -    proof (rule degree_diff_le)
   1.432 -      show "degree (pCons a r) \<le> degree y"
   1.433 -        using r by auto
   1.434 -      show "degree (smult b y) \<le> degree y"
   1.435 -        by (rule degree_smult_le)
   1.436 -    qed
   1.437 -  next
   1.438 -    show "coeff ?r (degree y) = 0"
   1.439 -      using \<open>y \<noteq> 0\<close> unfolding b by simp
   1.440 -  qed
   1.441 -
   1.442 -  from 1 2 show ?thesis
   1.443 -    unfolding eucl_rel_poly_iff
   1.444 -    using \<open>y \<noteq> 0\<close> by simp
   1.445 -qed
   1.446 -
   1.447 -lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
   1.448 -apply (cases "y = 0")
   1.449 -apply (fast intro!: eucl_rel_poly_by_0)
   1.450 -apply (induct x)
   1.451 -apply (fast intro!: eucl_rel_poly_0)
   1.452 -apply (fast intro!: eucl_rel_poly_pCons)
   1.453 -done
   1.454 -
   1.455 -lemma eucl_rel_poly_unique:
   1.456 -  assumes 1: "eucl_rel_poly x y (q1, r1)"
   1.457 -  assumes 2: "eucl_rel_poly x y (q2, r2)"
   1.458 -  shows "q1 = q2 \<and> r1 = r2"
   1.459 -proof (cases "y = 0")
   1.460 -  assume "y = 0" with assms show ?thesis
   1.461 -    by (simp add: eucl_rel_poly_iff)
   1.462 -next
   1.463 -  assume [simp]: "y \<noteq> 0"
   1.464 -  from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
   1.465 -    unfolding eucl_rel_poly_iff by simp_all
   1.466 -  from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
   1.467 -    unfolding eucl_rel_poly_iff by simp_all
   1.468 -  from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
   1.469 -    by (simp add: algebra_simps)
   1.470 -  from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
   1.471 -    by (auto intro: degree_diff_less)
   1.472 -
   1.473 -  show "q1 = q2 \<and> r1 = r2"
   1.474 -  proof (rule ccontr)
   1.475 -    assume "\<not> (q1 = q2 \<and> r1 = r2)"
   1.476 -    with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
   1.477 -    with r3 have "degree (r2 - r1) < degree y" by simp
   1.478 -    also have "degree y \<le> degree (q1 - q2) + degree y" by simp
   1.479 -    also have "\<dots> = degree ((q1 - q2) * y)"
   1.480 -      using \<open>q1 \<noteq> q2\<close> by (simp add: degree_mult_eq)
   1.481 -    also have "\<dots> = degree (r2 - r1)"
   1.482 -      using q3 by simp
   1.483 -    finally have "degree (r2 - r1) < degree (r2 - r1)" .
   1.484 -    then show "False" by simp
   1.485 -  qed
   1.486 -qed
   1.487 -
   1.488 -lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
   1.489 -by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
   1.490 -
   1.491 -lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
   1.492 -by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
   1.493 -
   1.494 -lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
   1.495 -
   1.496 -lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
   1.497 -
   1.498 -
   1.499 -
   1.500 -subsection \<open>Pseudo-Division and Division of Polynomials\<close>
   1.501 -
   1.502 -text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
   1.503 -
   1.504 -fun pseudo_divmod_main :: "'a :: comm_ring_1  \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly 
   1.505 -  \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly \<times> 'a poly" where
   1.506 -  "pseudo_divmod_main lc q r d dr (Suc n) = (let
   1.507 -     rr = smult lc r;
   1.508 -     qq = coeff r dr;
   1.509 -     rrr = rr - monom qq n * d;
   1.510 -     qqq = smult lc q + monom qq n
   1.511 -     in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
   1.512 -| "pseudo_divmod_main lc q r d dr 0 = (q,r)"
   1.513 -
   1.514 -definition pseudo_divmod :: "'a :: comm_ring_1 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" where
   1.515 -  "pseudo_divmod p q \<equiv> if q = 0 then (0,p) else
   1.516 -     pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p) (1 + length (coeffs p) - length (coeffs q))"
   1.517 -
   1.518 -lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr - 1"
   1.519 -  using eq_zero_or_degree_less by fastforce
   1.520 -  
   1.521 -lemma pseudo_divmod_main: assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
   1.522 -  and *: "degree r \<le> dr" "pseudo_divmod_main lc q r d dr n = (q',r')" 
   1.523 -    "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> r = 0" 
   1.524 -  shows "(r' = 0 \<or> degree r' < degree d) \<and> smult (lc^n) (d * q + r) = d * q' + r'"
   1.525 -  using *
   1.526 -proof (induct n arbitrary: q r dr)
   1.527 -  case (Suc n q r dr)
   1.528 -  let ?rr = "smult lc r"
   1.529 -  let ?qq = "coeff r dr"
   1.530 -  define b where [simp]: "b = monom ?qq n"
   1.531 -  let ?rrr = "?rr - b * d"
   1.532 -  let ?qqq = "smult lc q + b"
   1.533 -  note res = Suc(3)
   1.534 -  from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def] 
   1.535 -  have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')" 
   1.536 -    by (simp del: pseudo_divmod_main.simps)
   1.537 -  have dr: "dr = n + degree d" using Suc(4) by auto
   1.538 -  have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
   1.539 -  proof (cases "?qq = 0")
   1.540 -    case False
   1.541 -    hence n: "n = degree b" by (simp add: degree_monom_eq)
   1.542 -    show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
   1.543 -  qed auto
   1.544 -  also have "\<dots> = lc * coeff b n" unfolding d by simp
   1.545 -  finally have "coeff (b * d) dr = lc * coeff b n" .
   1.546 -  moreover have "coeff ?rr dr = lc * coeff r dr" by simp
   1.547 -  ultimately have c0: "coeff ?rrr dr = 0" by auto
   1.548 -  have dr: "dr = n + degree d" using Suc(4) by auto
   1.549 -  have deg_rr: "degree ?rr \<le> dr" using Suc(2) 
   1.550 -    using degree_smult_le dual_order.trans by blast 
   1.551 -  have deg_bd: "degree (b * d) \<le> dr"
   1.552 -    unfolding dr
   1.553 -    by(rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
   1.554 -  have "degree ?rrr \<le> dr"
   1.555 -    using degree_diff_le[OF deg_rr deg_bd] by auto
   1.556 -  with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)" by (rule coeff_0_degree_minus_1)
   1.557 -  have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
   1.558 -  proof (cases dr)
   1.559 -    case 0
   1.560 -    with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
   1.561 -    with deg_rrr have "degree ?rrr = 0" by simp
   1.562 -    hence "\<exists> a. ?rrr = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
   1.563 -    from this obtain a where rrr: "?rrr = [:a:]" by auto
   1.564 -    show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
   1.565 -  qed (insert Suc(4), auto)
   1.566 -  note IH = Suc(1)[OF deg_rrr res this]
   1.567 -  show ?case
   1.568 -  proof (intro conjI)
   1.569 -    show "r' = 0 \<or> degree r' < degree d" using IH by blast
   1.570 -    show "smult (lc ^ Suc n) (d * q + r) = d * q' + r'"
   1.571 -      unfolding IH[THEN conjunct2,symmetric]
   1.572 -      by (simp add: field_simps smult_add_right)
   1.573 -  qed
   1.574 -qed auto
   1.575 -
   1.576 -lemma pseudo_divmod:
   1.577 -  assumes g: "g \<noteq> 0" and *: "pseudo_divmod f g = (q,r)" 
   1.578 -  shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is ?A)
   1.579 -    and "r = 0 \<or> degree r < degree g" (is ?B)
   1.580 -proof -
   1.581 -  from *[unfolded pseudo_divmod_def Let_def]
   1.582 -  have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (auto simp: g)
   1.583 -  note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl]
   1.584 -  have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \<or>
   1.585 -    degree f = 0 \<and> 1 + length (coeffs f) - length (coeffs g) = 0 \<and> f = 0" using g 
   1.586 -    by (cases "f = 0"; cases "coeffs g", auto simp: degree_eq_length_coeffs)
   1.587 -  note main = main[OF this]
   1.588 -  from main show "r = 0 \<or> degree r < degree g" by auto
   1.589 -  show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" 
   1.590 -    by (subst main[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
   1.591 -    insert g, cases "f = 0"; cases "coeffs g", auto)
   1.592 -qed
   1.593 -  
   1.594 -definition "pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)"
   1.595 -
   1.596 -lemma snd_pseudo_divmod_main:
   1.597 -  "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)"
   1.598 -by (induct n arbitrary: q q' lc r d dr; simp add: Let_def)
   1.599 -
   1.600 -definition pseudo_mod 
   1.601 -    :: "'a :: {comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   1.602 -  "pseudo_mod f g = snd (pseudo_divmod f g)"
   1.603 -  
   1.604 -lemma pseudo_mod:
   1.605 -  fixes f g
   1.606 -  defines "r \<equiv> pseudo_mod f g"
   1.607 -  assumes g: "g \<noteq> 0"
   1.608 -  shows "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" "r = 0 \<or> degree r < degree g"
   1.609 -proof - 
   1.610 -  let ?cg = "coeff g (degree g)"
   1.611 -  let ?cge = "?cg ^ (Suc (degree f) - degree g)"
   1.612 -  define a where "a = ?cge"
   1.613 -  obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def]
   1.614 -    by (cases "pseudo_divmod f g", auto)
   1.615 -  from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g" 
   1.616 -    unfolding a_def by auto
   1.617 -  show "r = 0 \<or> degree r < degree g" by fact
   1.618 -  from g have "a \<noteq> 0" unfolding a_def by auto
   1.619 -  thus "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" using id by auto
   1.620 -qed
   1.621 -
   1.622 -instantiation poly :: (idom_divide) idom_divide
   1.623 -begin
   1.624 -
   1.625 -fun divide_poly_main :: "'a \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly 
   1.626 -  \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly" where
   1.627 -  "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in 
   1.628 -     if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
   1.629 -     divide_poly_main 
   1.630 -       lc 
   1.631 -       (q + mon) 
   1.632 -       (r - mon * d) 
   1.633 -       d (dr - 1) n else 0)"
   1.634 -| "divide_poly_main lc q r d dr 0 = q"
   1.635 -
   1.636 -definition divide_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   1.637 -  "divide_poly f g = (if g = 0 then 0 else
   1.638 -     divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))" 
   1.639 -
   1.640 -lemma divide_poly_main:
   1.641 -  assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
   1.642 -    and *: "degree (d * r) \<le> dr" "divide_poly_main lc q (d * r) d dr n = q'" 
   1.643 -    "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> d * r = 0" 
   1.644 -  shows "q' = q + r"
   1.645 -  using *
   1.646 -proof (induct n arbitrary: q r dr)
   1.647 -  case (Suc n q r dr)
   1.648 -  let ?rr = "d * r"
   1.649 -  let ?a = "coeff ?rr dr"
   1.650 -  let ?qq = "?a div lc"
   1.651 -  define b where [simp]: "b = monom ?qq n"
   1.652 -  let ?rrr =  "d * (r - b)"
   1.653 -  let ?qqq = "q + b"
   1.654 -  note res = Suc(3)
   1.655 -  have dr: "dr = n + degree d" using Suc(4) by auto
   1.656 -  have lc: "lc \<noteq> 0" using d by auto
   1.657 -  have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
   1.658 -  proof (cases "?qq = 0")
   1.659 -    case False
   1.660 -    hence n: "n = degree b" by (simp add: degree_monom_eq)
   1.661 -    show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
   1.662 -  qed simp
   1.663 -  also have "\<dots> = lc * coeff b n" unfolding d by simp
   1.664 -  finally have c2: "coeff (b * d) dr = lc * coeff b n" .
   1.665 -  have rrr: "?rrr = ?rr - b * d" by (simp add: field_simps)
   1.666 -  have c1: "coeff (d * r) dr = lc * coeff r n"
   1.667 -  proof (cases "degree r = n")
   1.668 -    case True
   1.669 -    thus ?thesis using Suc(2) unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps)
   1.670 -  next
   1.671 -    case False
   1.672 -    have "degree r \<le> n" using dr Suc(2) by auto
   1.673 -      (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq diff_is_0_eq diff_zero le_cases)
   1.674 -    with False have r_n: "degree r < n" by auto
   1.675 -    hence right: "lc * coeff r n = 0" by (simp add: coeff_eq_0)
   1.676 -    have "coeff (d * r) dr = coeff (d * r) (degree d + n)" unfolding dr by (simp add: ac_simps)
   1.677 -    also have "\<dots> = 0" using r_n
   1.678 -      by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0 
   1.679 -        coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq)
   1.680 -    finally show ?thesis unfolding right .
   1.681 -  qed
   1.682 -  have c0: "coeff ?rrr dr = 0" 
   1.683 -    and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr" unfolding rrr coeff_diff c2
   1.684 -    unfolding b_def coeff_monom coeff_smult c1 using lc by auto
   1.685 -  from res[unfolded divide_poly_main.simps[of lc q] Let_def] id
   1.686 -  have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'" 
   1.687 -    by (simp del: divide_poly_main.simps add: field_simps)
   1.688 -  note IH = Suc(1)[OF _ res] 
   1.689 -  have dr: "dr = n + degree d" using Suc(4) by auto
   1.690 -  have deg_rr: "degree ?rr \<le> dr" using Suc(2) by auto
   1.691 -  have deg_bd: "degree (b * d) \<le> dr"
   1.692 -    unfolding dr b_def by (rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
   1.693 -  have "degree ?rrr \<le> dr" unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd])
   1.694 -  with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)" by (rule coeff_0_degree_minus_1)
   1.695 -  have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"  
   1.696 -  proof (cases dr)
   1.697 -    case 0
   1.698 -    with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
   1.699 -    with deg_rrr have "degree ?rrr = 0" by simp
   1.700 -    from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]" by metis
   1.701 -    show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
   1.702 -  qed (insert Suc(4), auto)
   1.703 -  note IH = IH[OF deg_rrr this]
   1.704 -  show ?case using IH by simp
   1.705 -next
   1.706 -  case (0 q r dr)
   1.707 -  show ?case 
   1.708 -  proof (cases "r = 0")
   1.709 -    case True
   1.710 -    thus ?thesis using 0 by auto
   1.711 -  next
   1.712 -    case False
   1.713 -    have "degree (d * r) = degree d + degree r" using d False 
   1.714 -      by (subst degree_mult_eq, auto)
   1.715 -    thus ?thesis using 0 d by auto
   1.716 -  qed
   1.717 -qed 
   1.718 -
   1.719 -lemma fst_pseudo_divmod_main_as_divide_poly_main:
   1.720 -  assumes d: "d \<noteq> 0"
   1.721 -  defines lc: "lc \<equiv> coeff d (degree d)"
   1.722 -  shows "fst (pseudo_divmod_main lc q r d dr n) = divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n"
   1.723 -proof(induct n arbitrary: q r dr)
   1.724 -  case 0 then show ?case by simp
   1.725 -next
   1.726 -  case (Suc n)
   1.727 -    note lc0 = leading_coeff_neq_0[OF d, folded lc]
   1.728 -    then have "pseudo_divmod_main lc q r d dr (Suc n) =
   1.729 -    pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n)
   1.730 -      (smult lc r - monom (coeff r dr) n * d) d (dr - 1) n"
   1.731 -    by (simp add: Let_def ac_simps)
   1.732 -    also have "fst ... = divide_poly_main lc
   1.733 -     (smult (lc^n) (smult lc q + monom (coeff r dr) n))
   1.734 -     (smult (lc^n) (smult lc r - monom (coeff r dr) n * d))
   1.735 -     d (dr - 1) n"
   1.736 -      unfolding Suc[unfolded divide_poly_main.simps Let_def]..
   1.737 -    also have "... = divide_poly_main lc (smult (lc ^ Suc n) q)
   1.738 -        (smult (lc ^ Suc n) r) d dr (Suc n)"
   1.739 -      unfolding smult_monom smult_distribs mult_smult_left[symmetric]
   1.740 -      using lc0 by (simp add: Let_def ac_simps)
   1.741 -    finally show ?case.
   1.742 -qed
   1.743 -
   1.744 -
   1.745 -lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0"
   1.746 -proof (induct n arbitrary: r d dr)
   1.747 -  case (Suc n r d dr)
   1.748 -  show ?case unfolding divide_poly_main.simps[of _ _ r] Let_def
   1.749 -    by (simp add: Suc del: divide_poly_main.simps)
   1.750 -qed simp
   1.751 -
   1.752 -lemma divide_poly:
   1.753 -  assumes g: "g \<noteq> 0"
   1.754 -  shows "(f * g) div g = (f :: 'a poly)" 
   1.755 -proof - 
   1.756 -  have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs  g)) 
   1.757 -    = (f * g) div g" unfolding divide_poly_def Let_def by (simp add: ac_simps)
   1.758 -  note main = divide_poly_main[OF g refl le_refl this]
   1.759 -  {
   1.760 -    fix f :: "'a poly"
   1.761 -    assume "f \<noteq> 0"
   1.762 -    hence "length (coeffs f) = Suc (degree f)" unfolding degree_eq_length_coeffs by auto
   1.763 -  } note len = this
   1.764 -  have "(f * g) div g = 0 + f"
   1.765 -  proof (rule main, goal_cases)
   1.766 -    case 1
   1.767 -    show ?case
   1.768 -    proof (cases "f = 0")
   1.769 -      case True
   1.770 -      with g show ?thesis by (auto simp: degree_eq_length_coeffs)
   1.771 -    next
   1.772 -      case False
   1.773 -      with g have fg: "g * f \<noteq> 0" by auto
   1.774 -      show ?thesis unfolding len[OF fg] len[OF g] by auto
   1.775 -    qed
   1.776 -  qed
   1.777 -  thus ?thesis by simp
   1.778 -qed
   1.779 -
   1.780 -lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
   1.781 -  by (simp add: divide_poly_def Let_def divide_poly_main_0)
   1.782 -
   1.783 -instance
   1.784 -  by standard (auto simp: divide_poly divide_poly_0)
   1.785 -
   1.786 -end
   1.787 -
   1.788 -instance poly :: (idom_divide) algebraic_semidom ..
   1.789 -
   1.790 -lemma div_const_poly_conv_map_poly: 
   1.791 -  assumes "[:c:] dvd p"
   1.792 -  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
   1.793 -proof (cases "c = 0")
   1.794 -  case False
   1.795 -  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   1.796 -  moreover {
   1.797 -    have "smult c q = [:c:] * q" by simp
   1.798 -    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
   1.799 -    finally have "smult c q div [:c:] = q" .
   1.800 -  }
   1.801 -  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
   1.802 -qed (auto intro!: poly_eqI simp: coeff_map_poly)
   1.803 -
   1.804 -lemma is_unit_monom_0:
   1.805 -  fixes a :: "'a::field"
   1.806 -  assumes "a \<noteq> 0"
   1.807 -  shows "is_unit (monom a 0)"
   1.808 -proof
   1.809 -  from assms show "1 = monom a 0 * monom (inverse a) 0"
   1.810 -    by (simp add: mult_monom)
   1.811 -qed
   1.812 -
   1.813 -lemma is_unit_triv:
   1.814 -  fixes a :: "'a::field"
   1.815 -  assumes "a \<noteq> 0"
   1.816 -  shows "is_unit [:a:]"
   1.817 -  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
   1.818 -
   1.819 -lemma is_unit_iff_degree:
   1.820 -  assumes "p \<noteq> (0 :: _ :: field poly)"
   1.821 -  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
   1.822 -proof
   1.823 -  assume ?Q
   1.824 -  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
   1.825 -  with assms show ?P by (simp add: is_unit_triv)
   1.826 -next
   1.827 -  assume ?P
   1.828 -  then obtain q where "q \<noteq> 0" "p * q = 1" ..
   1.829 -  then have "degree (p * q) = degree 1"
   1.830 -    by simp
   1.831 -  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
   1.832 -    by (simp add: degree_mult_eq)
   1.833 -  then show ?Q by simp
   1.834 -qed
   1.835 -
   1.836 -lemma is_unit_pCons_iff:
   1.837 -  "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
   1.838 -  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
   1.839 -
   1.840 -lemma is_unit_monom_trival:
   1.841 -  fixes p :: "'a::field poly"
   1.842 -  assumes "is_unit p"
   1.843 -  shows "monom (coeff p (degree p)) 0 = p"
   1.844 -  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
   1.845 -
   1.846 -lemma is_unit_const_poly_iff: 
   1.847 -  "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
   1.848 -  by (auto simp: one_poly_def)
   1.849 -
   1.850 -lemma is_unit_polyE:
   1.851 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   1.852 -  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
   1.853 -proof -
   1.854 -  from assms obtain q where "1 = p * q"
   1.855 -    by (rule dvdE)
   1.856 -  then have "p \<noteq> 0" and "q \<noteq> 0"
   1.857 -    by auto
   1.858 -  from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
   1.859 -    by simp
   1.860 -  also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
   1.861 -    by (simp add: degree_mult_eq)
   1.862 -  finally have "degree p = 0" by simp
   1.863 -  with degree_eq_zeroE obtain c where c: "p = [:c:]" .
   1.864 -  moreover with \<open>p dvd 1\<close> have "c dvd 1"
   1.865 -    by (simp add: is_unit_const_poly_iff)
   1.866 -  ultimately show thesis
   1.867 -    by (rule that)
   1.868 -qed
   1.869 -
   1.870 -lemma is_unit_polyE':
   1.871 -  assumes "is_unit (p::_::field poly)"
   1.872 -  obtains a where "p = monom a 0" and "a \<noteq> 0"
   1.873 -proof -
   1.874 -  obtain a q where "p = pCons a q" by (cases p)
   1.875 -  with assms have "p = [:a:]" and "a \<noteq> 0"
   1.876 -    by (simp_all add: is_unit_pCons_iff)
   1.877 -  with that show thesis by (simp add: monom_0)
   1.878 -qed
   1.879 -
   1.880 -lemma is_unit_poly_iff:
   1.881 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   1.882 -  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
   1.883 -  by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
   1.884 -
   1.885 -instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
   1.886 -begin
   1.887 -
   1.888 -definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   1.889 -  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
   1.890 -
   1.891 -definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
   1.892 -  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   1.893 -
   1.894 -instance proof
   1.895 -  fix p :: "'a poly"
   1.896 -  show "unit_factor p * normalize p = p"
   1.897 -    by (cases "p = 0")
   1.898 -       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
   1.899 -          smult_conv_map_poly map_poly_map_poly o_def)
   1.900 -next
   1.901 -  fix p :: "'a poly"
   1.902 -  assume "is_unit p"
   1.903 -  then obtain c where p: "p = [:c:]" "is_unit c"
   1.904 -    by (auto simp: is_unit_poly_iff)
   1.905 -  thus "normalize p = 1"
   1.906 -    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
   1.907 -next
   1.908 -  fix p :: "'a poly" assume "p \<noteq> 0"
   1.909 -  thus "is_unit (unit_factor p)"
   1.910 -    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
   1.911 -qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
   1.912 -
   1.913 -end
   1.914 -
   1.915 -lemma normalize_poly_eq_div:
   1.916 -  "normalize p = p div [:unit_factor (lead_coeff p):]"
   1.917 -proof (cases "p = 0")
   1.918 -  case False
   1.919 -  thus ?thesis
   1.920 -    by (subst div_const_poly_conv_map_poly)
   1.921 -       (auto simp: normalize_poly_def const_poly_dvd_iff)
   1.922 -qed (auto simp: normalize_poly_def)
   1.923 -
   1.924 -lemma unit_factor_pCons:
   1.925 -  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   1.926 -  by (simp add: unit_factor_poly_def)
   1.927 -
   1.928 -lemma normalize_monom [simp]:
   1.929 -  "normalize (monom a n) = monom (normalize a) n"
   1.930 -  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
   1.931 -
   1.932 -lemma unit_factor_monom [simp]:
   1.933 -  "unit_factor (monom a n) = monom (unit_factor a) 0"
   1.934 -  by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
   1.935 -
   1.936 -lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   1.937 -  by (simp add: normalize_poly_def map_poly_pCons)
   1.938 -
   1.939 -lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   1.940 -proof -
   1.941 -  have "smult c p = [:c:] * p" by simp
   1.942 -  also have "normalize \<dots> = smult (normalize c) (normalize p)"
   1.943 -    by (subst normalize_mult) (simp add: normalize_const_poly)
   1.944 -  finally show ?thesis .
   1.945 -qed
   1.946 -
   1.947 -
   1.948 -subsubsection \<open>Division in Field Polynomials\<close>
   1.949 -
   1.950 -text\<open>
   1.951 - This part connects the above result to the division of field polynomials.
   1.952 - Mainly imported from Isabelle 2016.
   1.953 -\<close>
   1.954 -
   1.955 -lemma pseudo_divmod_field:
   1.956 -  assumes g: "(g::'a::field poly) \<noteq> 0" and *: "pseudo_divmod f g = (q,r)"
   1.957 -  defines "c \<equiv> coeff g (degree g) ^ (Suc (degree f) - degree g)"
   1.958 -  shows "f = g * smult (1/c) q + smult (1/c) r"
   1.959 -proof -
   1.960 -  from leading_coeff_neq_0[OF g] have c0: "c \<noteq> 0" unfolding c_def by auto
   1.961 -  from pseudo_divmod(1)[OF g *, folded c_def]
   1.962 -  have "smult c f = g * q + r" by auto
   1.963 -  also have "smult (1/c) ... = g * smult (1/c) q + smult (1/c) r" by (simp add: smult_add_right)
   1.964 -  finally show ?thesis using c0 by auto
   1.965 -qed
   1.966 -
   1.967 -lemma divide_poly_main_field:
   1.968 -  assumes d: "(d::'a::field poly) \<noteq> 0"
   1.969 -  defines lc: "lc \<equiv> coeff d (degree d)"
   1.970 -  shows "divide_poly_main lc q r d dr n = fst (pseudo_divmod_main lc (smult ((1/lc)^n) q) (smult ((1/lc)^n) r) d dr n)"
   1.971 -  unfolding lc
   1.972 -  by(subst fst_pseudo_divmod_main_as_divide_poly_main, auto simp: d power_one_over)
   1.973 -
   1.974 -lemma divide_poly_field:
   1.975 -  fixes f g :: "'a :: field poly"
   1.976 -  defines "f' \<equiv> smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f"
   1.977 -  shows "(f::'a::field poly) div g = fst (pseudo_divmod f' g)"
   1.978 -proof (cases "g = 0")
   1.979 -  case True show ?thesis 
   1.980 -    unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True by (simp add: divide_poly_main_0)
   1.981 -next
   1.982 -  case False
   1.983 -    from leading_coeff_neq_0[OF False] have "degree f' = degree f" unfolding f'_def by auto
   1.984 -    then show ?thesis
   1.985 -      using length_coeffs_degree[of f'] length_coeffs_degree[of f]
   1.986 -      unfolding divide_poly_def pseudo_divmod_def Let_def
   1.987 -                divide_poly_main_field[OF False]
   1.988 -                length_coeffs_degree[OF False] 
   1.989 -                f'_def
   1.990 -      by force
   1.991 -qed
   1.992 -
   1.993 -instantiation poly :: (field) ring_div
   1.994 -begin
   1.995 -
   1.996 -definition modulo_poly where
   1.997 -  mod_poly_def: "f mod g \<equiv>
   1.998 -    if g = 0 then f
   1.999 -    else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
  1.1000 -
  1.1001 -lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
  1.1002 -  unfolding eucl_rel_poly_iff
  1.1003 -proof (intro conjI)
  1.1004 -  show "x = x div y * y + x mod y"
  1.1005 -  proof(cases "y = 0")
  1.1006 -    case True show ?thesis by(simp add: True divide_poly_def divide_poly_0 mod_poly_def)
  1.1007 -  next
  1.1008 -    case False
  1.1009 -    then have "pseudo_divmod (smult ((1 / coeff y (degree y)) ^ (Suc (degree x) - degree y)) x) y =
  1.1010 -          (x div y, x mod y)"
  1.1011 -      unfolding divide_poly_field mod_poly_def pseudo_mod_def by simp
  1.1012 -    from pseudo_divmod[OF False this]
  1.1013 -    show ?thesis using False
  1.1014 -      by (simp add: power_mult_distrib[symmetric] mult.commute)
  1.1015 -  qed
  1.1016 -  show "if y = 0 then x div y = 0 else x mod y = 0 \<or> degree (x mod y) < degree y"
  1.1017 -  proof (cases "y = 0")
  1.1018 -    case True then show ?thesis by auto
  1.1019 -  next
  1.1020 -    case False
  1.1021 -      with pseudo_mod[OF this] show ?thesis unfolding mod_poly_def by simp
  1.1022 -  qed
  1.1023 -qed
  1.1024 -
  1.1025 -lemma div_poly_eq:
  1.1026 -  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
  1.1027 -  by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
  1.1028 -
  1.1029 -lemma mod_poly_eq:
  1.1030 -  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
  1.1031 -  by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
  1.1032 -
  1.1033 -instance
  1.1034 -proof
  1.1035 -  fix x y :: "'a poly"
  1.1036 -  from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
  1.1037 -  show "x div y * y + x mod y = x" by auto
  1.1038 -next
  1.1039 -  fix x y z :: "'a poly"
  1.1040 -  assume "y \<noteq> 0"
  1.1041 -  hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
  1.1042 -    using eucl_rel_poly [of x y]
  1.1043 -    by (simp add: eucl_rel_poly_iff distrib_right)
  1.1044 -  thus "(x + z * y) div y = z + x div y"
  1.1045 -    by (rule div_poly_eq)
  1.1046 -next
  1.1047 -  fix x y z :: "'a poly"
  1.1048 -  assume "x \<noteq> 0"
  1.1049 -  show "(x * y) div (x * z) = y div z"
  1.1050 -  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
  1.1051 -    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
  1.1052 -      by (rule eucl_rel_poly_by_0)
  1.1053 -    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
  1.1054 -      by (rule div_poly_eq)
  1.1055 -    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
  1.1056 -      by (rule eucl_rel_poly_0)
  1.1057 -    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
  1.1058 -      by (rule div_poly_eq)
  1.1059 -    case False then show ?thesis by auto
  1.1060 -  next
  1.1061 -    case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
  1.1062 -    with \<open>x \<noteq> 0\<close>
  1.1063 -    have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
  1.1064 -      by (auto simp add: eucl_rel_poly_iff algebra_simps)
  1.1065 -        (rule classical, simp add: degree_mult_eq)
  1.1066 -    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
  1.1067 -    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
  1.1068 -    then show ?thesis by (simp add: div_poly_eq)
  1.1069 -  qed
  1.1070 -qed
  1.1071 -
  1.1072 -end
  1.1073 -
  1.1074 -lemma degree_mod_less:
  1.1075 -  "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
  1.1076 -  using eucl_rel_poly [of x y]
  1.1077 -  unfolding eucl_rel_poly_iff by simp
  1.1078 -
  1.1079 -lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
  1.1080 -proof -
  1.1081 -  assume "degree x < degree y"
  1.1082 -  hence "eucl_rel_poly x y (0, x)"
  1.1083 -    by (simp add: eucl_rel_poly_iff)
  1.1084 -  thus "x div y = 0" by (rule div_poly_eq)
  1.1085 -qed
  1.1086 -
  1.1087 -lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
  1.1088 -proof -
  1.1089 -  assume "degree x < degree y"
  1.1090 -  hence "eucl_rel_poly x y (0, x)"
  1.1091 -    by (simp add: eucl_rel_poly_iff)
  1.1092 -  thus "x mod y = x" by (rule mod_poly_eq)
  1.1093 -qed
  1.1094 -
  1.1095 -lemma eucl_rel_poly_smult_left:
  1.1096 -  "eucl_rel_poly x y (q, r)
  1.1097 -    \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
  1.1098 -  unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
  1.1099 -
  1.1100 -lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
  1.1101 -  by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  1.1102 -
  1.1103 -lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  1.1104 -  by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  1.1105 -
  1.1106 -lemma poly_div_minus_left [simp]:
  1.1107 -  fixes x y :: "'a::field poly"
  1.1108 -  shows "(- x) div y = - (x div y)"
  1.1109 -  using div_smult_left [of "- 1::'a"] by simp
  1.1110 -
  1.1111 -lemma poly_mod_minus_left [simp]:
  1.1112 -  fixes x y :: "'a::field poly"
  1.1113 -  shows "(- x) mod y = - (x mod y)"
  1.1114 -  using mod_smult_left [of "- 1::'a"] by simp
  1.1115 -
  1.1116 -lemma eucl_rel_poly_add_left:
  1.1117 -  assumes "eucl_rel_poly x y (q, r)"
  1.1118 -  assumes "eucl_rel_poly x' y (q', r')"
  1.1119 -  shows "eucl_rel_poly (x + x') y (q + q', r + r')"
  1.1120 -  using assms unfolding eucl_rel_poly_iff
  1.1121 -  by (auto simp add: algebra_simps degree_add_less)
  1.1122 -
  1.1123 -lemma poly_div_add_left:
  1.1124 -  fixes x y z :: "'a::field poly"
  1.1125 -  shows "(x + y) div z = x div z + y div z"
  1.1126 -  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  1.1127 -  by (rule div_poly_eq)
  1.1128 -
  1.1129 -lemma poly_mod_add_left:
  1.1130 -  fixes x y z :: "'a::field poly"
  1.1131 -  shows "(x + y) mod z = x mod z + y mod z"
  1.1132 -  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  1.1133 -  by (rule mod_poly_eq)
  1.1134 -
  1.1135 -lemma poly_div_diff_left:
  1.1136 -  fixes x y z :: "'a::field poly"
  1.1137 -  shows "(x - y) div z = x div z - y div z"
  1.1138 -  by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
  1.1139 -
  1.1140 -lemma poly_mod_diff_left:
  1.1141 -  fixes x y z :: "'a::field poly"
  1.1142 -  shows "(x - y) mod z = x mod z - y mod z"
  1.1143 -  by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
  1.1144 -
  1.1145 -lemma eucl_rel_poly_smult_right:
  1.1146 -  "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
  1.1147 -    \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
  1.1148 -  unfolding eucl_rel_poly_iff by simp
  1.1149 -
  1.1150 -lemma div_smult_right:
  1.1151 -  "(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  1.1152 -  by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  1.1153 -
  1.1154 -lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  1.1155 -  by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  1.1156 -
  1.1157 -lemma poly_div_minus_right [simp]:
  1.1158 -  fixes x y :: "'a::field poly"
  1.1159 -  shows "x div (- y) = - (x div y)"
  1.1160 -  using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
  1.1161 -
  1.1162 -lemma poly_mod_minus_right [simp]:
  1.1163 -  fixes x y :: "'a::field poly"
  1.1164 -  shows "x mod (- y) = x mod y"
  1.1165 -  using mod_smult_right [of "- 1::'a"] by simp
  1.1166 -
  1.1167 -lemma eucl_rel_poly_mult:
  1.1168 -  "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
  1.1169 -    \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
  1.1170 -apply (cases "z = 0", simp add: eucl_rel_poly_iff)
  1.1171 -apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
  1.1172 -apply (cases "r = 0")
  1.1173 -apply (cases "r' = 0")
  1.1174 -apply (simp add: eucl_rel_poly_iff)
  1.1175 -apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
  1.1176 -apply (cases "r' = 0")
  1.1177 -apply (simp add: eucl_rel_poly_iff degree_mult_eq)
  1.1178 -apply (simp add: eucl_rel_poly_iff field_simps)
  1.1179 -apply (simp add: degree_mult_eq degree_add_less)
  1.1180 -done
  1.1181 -
  1.1182 -lemma poly_div_mult_right:
  1.1183 -  fixes x y z :: "'a::field poly"
  1.1184 -  shows "x div (y * z) = (x div y) div z"
  1.1185 -  by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  1.1186 -
  1.1187 -lemma poly_mod_mult_right:
  1.1188 -  fixes x y z :: "'a::field poly"
  1.1189 -  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
  1.1190 -  by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  1.1191 -
  1.1192 -lemma mod_pCons:
  1.1193 -  fixes a and x
  1.1194 -  assumes y: "y \<noteq> 0"
  1.1195 -  defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  1.1196 -  shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
  1.1197 -unfolding b
  1.1198 -apply (rule mod_poly_eq)
  1.1199 -apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
  1.1200 -done
  1.1201 -
  1.1202 -definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  1.1203 -where
  1.1204 -  "pdivmod p q = (p div q, p mod q)"
  1.1205 -
  1.1206 -lemma pdivmod_0:
  1.1207 -  "pdivmod 0 q = (0, 0)"
  1.1208 -  by (simp add: pdivmod_def)
  1.1209 -
  1.1210 -lemma pdivmod_pCons:
  1.1211 -  "pdivmod (pCons a p) q =
  1.1212 -    (if q = 0 then (0, pCons a p) else
  1.1213 -      (let (s, r) = pdivmod p q;
  1.1214 -           b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1.1215 -        in (pCons b s, pCons a r - smult b q)))"
  1.1216 -  apply (simp add: pdivmod_def Let_def, safe)
  1.1217 -  apply (rule div_poly_eq)
  1.1218 -  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
  1.1219 -  apply (rule mod_poly_eq)
  1.1220 -  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
  1.1221 -  done
  1.1222 -
  1.1223 -lemma pdivmod_fold_coeffs:
  1.1224 -  "pdivmod p q = (if q = 0 then (0, p)
  1.1225 -    else fold_coeffs (\<lambda>a (s, r).
  1.1226 -      let b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1.1227 -      in (pCons b s, pCons a r - smult b q)
  1.1228 -   ) p (0, 0))"
  1.1229 -  apply (cases "q = 0")
  1.1230 -  apply (simp add: pdivmod_def)
  1.1231 -  apply (rule sym)
  1.1232 -  apply (induct p)
  1.1233 -  apply (simp_all add: pdivmod_0 pdivmod_pCons)
  1.1234 -  apply (case_tac "a = 0 \<and> p = 0")
  1.1235 -  apply (auto simp add: pdivmod_def)
  1.1236 -  done
  1.1237 -
  1.1238 -subsection \<open>List-based versions for fast implementation\<close>
  1.1239 -(* Subsection by:
  1.1240 -      Sebastiaan Joosten
  1.1241 -      René Thiemann
  1.1242 -      Akihisa Yamada
  1.1243 -    *)
  1.1244 -fun minus_poly_rev_list :: "'a :: group_add list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  1.1245 -  "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
  1.1246 -| "minus_poly_rev_list xs [] = xs"
  1.1247 -| "minus_poly_rev_list [] (y # ys) = []"
  1.1248 -
  1.1249 -fun pseudo_divmod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.1250 -  \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
  1.1251 -  "pseudo_divmod_main_list lc q r d (Suc n) = (let
  1.1252 -     rr = map (op * lc) r;
  1.1253 -     a = hd r;
  1.1254 -     qqq = cCons a (map (op * lc) q);
  1.1255 -     rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  1.1256 -     in pseudo_divmod_main_list lc qqq rrr d n)"
  1.1257 -| "pseudo_divmod_main_list lc q r d 0 = (q,r)"
  1.1258 -
  1.1259 -fun pseudo_mod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.1260 -  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.1261 -  "pseudo_mod_main_list lc r d (Suc n) = (let
  1.1262 -     rr = map (op * lc) r;
  1.1263 -     a = hd r;
  1.1264 -     rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  1.1265 -     in pseudo_mod_main_list lc rrr d n)"
  1.1266 -| "pseudo_mod_main_list lc r d 0 = r"
  1.1267 -
  1.1268 -
  1.1269 -fun divmod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.1270 -  \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
  1.1271 -  "divmod_poly_one_main_list q r d (Suc n) = (let
  1.1272 -     a = hd r;
  1.1273 -     qqq = cCons a q;
  1.1274 -     rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  1.1275 -     in divmod_poly_one_main_list qqq rr d n)"
  1.1276 -| "divmod_poly_one_main_list q r d 0 = (q,r)"
  1.1277 -
  1.1278 -fun mod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list 
  1.1279 -  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.1280 -  "mod_poly_one_main_list r d (Suc n) = (let
  1.1281 -     a = hd r;
  1.1282 -     rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  1.1283 -     in mod_poly_one_main_list rr d n)"
  1.1284 -| "mod_poly_one_main_list r d 0 = r"
  1.1285 -
  1.1286 -definition pseudo_divmod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list" where
  1.1287 -  "pseudo_divmod_list p q =
  1.1288 -  (if q = [] then ([],p) else
  1.1289 - (let rq = rev q;
  1.1290 -     (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in 
  1.1291 -   (qu,rev re)))"
  1.1292 -
  1.1293 -definition pseudo_mod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  1.1294 -  "pseudo_mod_list p q =
  1.1295 -  (if q = [] then p else
  1.1296 - (let rq = rev q;
  1.1297 -     re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in 
  1.1298 -   (rev re)))"
  1.1299 -
  1.1300 -lemma minus_zero_does_nothing:
  1.1301 -"(minus_poly_rev_list x (map (op * 0) y)) = (x :: 'a :: ring list)"
  1.1302 -  by(induct x y rule: minus_poly_rev_list.induct, auto)
  1.1303 -
  1.1304 -lemma length_minus_poly_rev_list[simp]:
  1.1305 - "length (minus_poly_rev_list xs ys) = length xs"
  1.1306 -  by(induct xs ys rule: minus_poly_rev_list.induct, auto)
  1.1307 -
  1.1308 -lemma if_0_minus_poly_rev_list:
  1.1309 -  "(if a = 0 then x else minus_poly_rev_list x (map (op * a) y))
  1.1310 -      = minus_poly_rev_list x (map (op * (a :: 'a :: ring)) y)"
  1.1311 -  by(cases "a=0",simp_all add:minus_zero_does_nothing)
  1.1312 -
  1.1313 -lemma Poly_append:
  1.1314 -  "Poly ((a::'a::comm_semiring_1 list) @ b) = Poly a + monom 1 (length a) * Poly b"
  1.1315 -  by (induct a,auto simp: monom_0 monom_Suc)
  1.1316 -
  1.1317 -lemma minus_poly_rev_list: "length p \<ge> length (q :: 'a :: comm_ring_1 list) \<Longrightarrow>
  1.1318 -  Poly (rev (minus_poly_rev_list (rev p) (rev q)))
  1.1319 -  = Poly p - monom 1 (length p - length q) * Poly q"
  1.1320 -proof (induct "rev p" "rev q" arbitrary: p q rule: minus_poly_rev_list.induct)
  1.1321 -  case (1 x xs y ys) 
  1.1322 -  have "length (rev q) \<le> length (rev p)" using 1 by simp
  1.1323 -  from this[folded 1(2,3)] have ys_xs:"length ys \<le> length xs" by simp
  1.1324 -  hence a:"Poly (rev (minus_poly_rev_list xs ys)) =
  1.1325 -           Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)"
  1.1326 -    by(subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev],auto)
  1.1327 -  have "Poly p - monom 1 (length p - length q) * Poly q
  1.1328 -      = Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))"
  1.1329 -    by simp
  1.1330 -  also have "\<dots> = Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))"
  1.1331 -    unfolding 1(2,3) by simp
  1.1332 -  also have "\<dots> = Poly (rev xs) + monom x (length xs) -
  1.1333 -  (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))" using ys_xs
  1.1334 -    by (simp add:Poly_append distrib_left mult_monom smult_monom)
  1.1335 -  also have "\<dots> = Poly (rev (minus_poly_rev_list xs ys)) + monom (x - y) (length xs)"
  1.1336 -    unfolding a diff_monom[symmetric] by(simp)
  1.1337 -  finally show ?case
  1.1338 -    unfolding 1(2,3)[symmetric] by (simp add: smult_monom Poly_append)
  1.1339 -qed auto
  1.1340 -
  1.1341 -lemma smult_monom_mult: "smult a (monom b n * f) = monom (a * b) n * f"
  1.1342 -  using smult_monom [of a _ n] by (metis mult_smult_left)
  1.1343 -
  1.1344 -lemma head_minus_poly_rev_list:
  1.1345 -  "length d \<le> length r \<Longrightarrow> d\<noteq>[] \<Longrightarrow>
  1.1346 -  hd (minus_poly_rev_list (map (op * (last d :: 'a :: comm_ring)) r) (map (op * (hd r)) (rev d))) = 0"
  1.1347 -proof(induct r)
  1.1348 -  case (Cons a rs)
  1.1349 -  thus ?case by(cases "rev d", simp_all add:ac_simps)
  1.1350 -qed simp
  1.1351 -
  1.1352 -lemma Poly_map: "Poly (map (op * a) p) = smult a (Poly p)"
  1.1353 -proof (induct p)
  1.1354 -  case(Cons x xs) thus ?case by (cases "Poly xs = 0",auto)
  1.1355 -qed simp
  1.1356 -
  1.1357 -lemma last_coeff_is_hd: "xs \<noteq> [] \<Longrightarrow> coeff (Poly xs) (length xs - 1) = hd (rev xs)"
  1.1358 -  by (simp_all add: hd_conv_nth rev_nth nth_default_nth nth_append)
  1.1359 -
  1.1360 -lemma pseudo_divmod_main_list_invar :
  1.1361 -  assumes leading_nonzero:"last d \<noteq> 0"
  1.1362 -  and lc:"last d = lc"
  1.1363 -  and dNonempty:"d \<noteq> []"
  1.1364 -  and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q',rev r')"
  1.1365 -  and "n = (1 + length r - length d)"
  1.1366 -  shows 
  1.1367 -  "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n = 
  1.1368 -  (Poly q', Poly r')"
  1.1369 -using assms(4-)
  1.1370 -proof(induct "n" arbitrary: r q)
  1.1371 -case (Suc n r q)
  1.1372 -  have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
  1.1373 -  have rNonempty:"r \<noteq> []"
  1.1374 -    using ifCond dNonempty using Suc_leI length_greater_0_conv list.size(3) by fastforce
  1.1375 -  let ?a = "(hd (rev r))"
  1.1376 -  let ?rr = "map (op * lc) (rev r)"
  1.1377 -  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (op * ?a) (rev d))))"
  1.1378 -  let ?qq = "cCons ?a (map (op * lc) q)"
  1.1379 -  have n: "n = (1 + length r - length d - 1)"
  1.1380 -    using ifCond Suc(3) by simp
  1.1381 -  have rr_val:"(length ?rrr) = (length r - 1)" using ifCond by auto
  1.1382 -  hence rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)"
  1.1383 -    using rNonempty ifCond unfolding One_nat_def by auto
  1.1384 -  from ifCond have id: "Suc (length r) - length d = Suc (length r - length d)" by auto
  1.1385 -  have "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')"
  1.1386 -    using Suc.prems ifCond by (simp add:Let_def if_0_minus_poly_rev_list id)
  1.1387 -  hence v:"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')"
  1.1388 -    using n by auto
  1.1389 -  have sucrr:"Suc (length r) - length d = Suc (length r - length d)"
  1.1390 -    using Suc_diff_le ifCond not_less_eq_eq by blast
  1.1391 -  have n_ok : "n = 1 + (length ?rrr) - length d" using Suc(3) rNonempty by simp
  1.1392 -  have cong: "\<And> x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  1.1393 -    pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n" by simp
  1.1394 -  have hd_rev:"coeff (Poly r) (length r - Suc 0) = hd (rev r)"
  1.1395 -    using last_coeff_is_hd[OF rNonempty] by simp
  1.1396 -  show ?case unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def
  1.1397 -  proof (rule cong[OF _ _ refl], goal_cases)
  1.1398 -    case 1 
  1.1399 -    show ?case unfolding monom_Suc hd_rev[symmetric]
  1.1400 -      by (simp add: smult_monom Poly_map)
  1.1401 -  next
  1.1402 -    case 2 
  1.1403 -    show ?case 
  1.1404 -    proof (subst Poly_on_rev_starting_with_0, goal_cases)
  1.1405 -      show "hd (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))) = 0"
  1.1406 -        by (fold lc, subst head_minus_poly_rev_list, insert ifCond dNonempty,auto)
  1.1407 -      from ifCond have "length d \<le> length r" by simp
  1.1408 -      then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
  1.1409 -        Poly (rev (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))))"
  1.1410 -        by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
  1.1411 -          minus_poly_rev_list)
  1.1412 -    qed
  1.1413 -  qed simp
  1.1414 -qed simp
  1.1415 -
  1.1416 -lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g =
  1.1417 -  map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
  1.1418 -proof (cases "g=0")
  1.1419 -case False
  1.1420 -  hence coeffs_g_nonempty:"(coeffs g) \<noteq> []" by simp
  1.1421 -  hence lastcoeffs:"last (coeffs g) = coeff g (degree g)"
  1.1422 -    by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil)
  1.1423 -  obtain q r where qr: "pseudo_divmod_main_list
  1.1424 -            (last (coeffs g)) (rev [])
  1.1425 -            (rev (coeffs f)) (rev (coeffs g))
  1.1426 -            (1 + length (coeffs f) -
  1.1427 -             length (coeffs g)) = (q,rev (rev r))"  by force
  1.1428 -  then have qr': "pseudo_divmod_main_list
  1.1429 -            (hd (rev (coeffs g))) []
  1.1430 -            (rev (coeffs f)) (rev (coeffs g))
  1.1431 -            (1 + length (coeffs f) -
  1.1432 -             length (coeffs g)) = (q,r)" using hd_rev[OF coeffs_g_nonempty] by(auto)
  1.1433 -  from False have cg: "(coeffs g = []) = False" by auto
  1.1434 -  have last_non0:"last (coeffs g) \<noteq> 0" using False by (simp add:last_coeffs_not_0)
  1.1435 -  show ?thesis
  1.1436 -    unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False
  1.1437 -    pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False]
  1.1438 -    poly_of_list_def
  1.1439 -    using False by (auto simp: degree_eq_length_coeffs)
  1.1440 -next
  1.1441 -  case True
  1.1442 -  show ?thesis unfolding True unfolding pseudo_divmod_def pseudo_divmod_list_def
  1.1443 -  by auto
  1.1444 -qed
  1.1445 -
  1.1446 -lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q 
  1.1447 -  xs ys n) = pseudo_mod_main_list l xs ys n"
  1.1448 -  by (induct n arbitrary: l q xs ys, auto simp: Let_def)
  1.1449 -
  1.1450 -lemma pseudo_mod_impl[code]: "pseudo_mod f g =
  1.1451 -  poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))"
  1.1452 -proof -
  1.1453 -  have snd_case: "\<And> f g p. snd ((\<lambda> (x,y). (f x, g y)) p) = g (snd p)" 
  1.1454 -    by auto
  1.1455 -  show ?thesis
  1.1456 -  unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
  1.1457 -    pseudo_mod_list_def Let_def
  1.1458 -  by (simp add: snd_case pseudo_mod_main_list)
  1.1459 -qed
  1.1460 -
  1.1461 -
  1.1462 -(* *************** *)
  1.1463 -subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
  1.1464 -
  1.1465 -lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)"
  1.1466 -  by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique)
  1.1467 -
  1.1468 -lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f) 
  1.1469 -     else let 
  1.1470 -       ilc = inverse (coeff g (degree g));       
  1.1471 -       h = smult ilc g;
  1.1472 -       (q,r) = pseudo_divmod f h
  1.1473 -     in (smult ilc q, r))" (is "?l = ?r")
  1.1474 -proof (cases "g = 0")
  1.1475 -  case False
  1.1476 -  define lc where "lc = inverse (coeff g (degree g))"
  1.1477 -  define h where "h = smult lc g"
  1.1478 -  from False have h1: "coeff h (degree h) = 1" and lc: "lc \<noteq> 0" unfolding h_def lc_def by auto
  1.1479 -  hence h0: "h \<noteq> 0" by auto
  1.1480 -  obtain q r where p: "pseudo_divmod f h = (q,r)" by force
  1.1481 -  from False have id: "?r = (smult lc q, r)" 
  1.1482 -    unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
  1.1483 -  from pseudo_divmod[OF h0 p, unfolded h1] 
  1.1484 -  have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
  1.1485 -  have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
  1.1486 -  hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel)
  1.1487 -  hence "pdivmod f g = (smult lc q, r)" 
  1.1488 -    unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc]
  1.1489 -    using lc by auto
  1.1490 -  with id show ?thesis by auto
  1.1491 -qed (auto simp: pdivmod_def)
  1.1492 -
  1.1493 -lemma pdivmod_via_pseudo_divmod_list: "pdivmod f g = (let 
  1.1494 -  cg = coeffs g
  1.1495 -  in if cg = [] then (0,f)
  1.1496 -     else let 
  1.1497 -       cf = coeffs f;
  1.1498 -       ilc = inverse (last cg);       
  1.1499 -       ch = map (op * ilc) cg;
  1.1500 -       (q,r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
  1.1501 -     in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))"
  1.1502 -proof -
  1.1503 -  note d = pdivmod_via_pseudo_divmod
  1.1504 -      pseudo_divmod_impl pseudo_divmod_list_def
  1.1505 -  show ?thesis
  1.1506 -  proof (cases "g = 0")
  1.1507 -    case True thus ?thesis unfolding d by auto
  1.1508 -  next
  1.1509 -    case False
  1.1510 -    define ilc where "ilc = inverse (coeff g (degree g))"
  1.1511 -    from False have ilc: "ilc \<noteq> 0" unfolding ilc_def by auto
  1.1512 -    with False have id: "(g = 0) = False" "(coeffs g = []) = False" 
  1.1513 -      "last (coeffs g) = coeff g (degree g)" 
  1.1514 -      "(coeffs (smult ilc g) = []) = False"
  1.1515 -      by (auto simp: last_coeffs_eq_coeff_degree) 
  1.1516 -    have id2: "hd (rev (coeffs (smult ilc g))) = 1"      
  1.1517 -      by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
  1.1518 -    have id3: "length (coeffs (smult ilc g)) = length (coeffs g)" 
  1.1519 -      "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))" unfolding coeffs_smult using ilc by auto
  1.1520 -    obtain q r where pair: "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g)))
  1.1521 -           (1 + length (coeffs f) - length (coeffs g)) = (q,r)" by force
  1.1522 -    show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2 
  1.1523 -      unfolding id3 pair map_prod_def split by (auto simp: Poly_map)
  1.1524 -  qed
  1.1525 -qed
  1.1526 -
  1.1527 -lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
  1.1528 -proof (intro ext, goal_cases)
  1.1529 -  case (1 q r d n)
  1.1530 -  {
  1.1531 -    fix xs :: "'a list"
  1.1532 -    have "map (op * 1) xs = xs" by (induct xs, auto)
  1.1533 -  } note [simp] = this
  1.1534 -  show ?case by (induct n arbitrary: q r d, auto simp: Let_def)
  1.1535 -qed
  1.1536 -
  1.1537 -fun divide_poly_main_list :: "'a::idom_divide \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.1538 -  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.1539 -  "divide_poly_main_list lc q r d (Suc n) = (let
  1.1540 -     cr = hd r
  1.1541 -     in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let 
  1.1542 -     a = cr div lc;
  1.1543 -     qq = cCons a q;
  1.1544 -     rr = minus_poly_rev_list r (map (op * a) d)
  1.1545 -     in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  1.1546 -| "divide_poly_main_list lc q r d 0 = q"
  1.1547 -
  1.1548 -
  1.1549 -lemma divide_poly_main_list_simp[simp]: "divide_poly_main_list lc q r d (Suc n) = (let
  1.1550 -     cr = hd r;
  1.1551 -     a = cr div lc;
  1.1552 -     qq = cCons a q;
  1.1553 -     rr = minus_poly_rev_list r (map (op * a) d)
  1.1554 -     in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  1.1555 -  by (simp add: Let_def minus_zero_does_nothing)
  1.1556 -
  1.1557 -declare divide_poly_main_list.simps(1)[simp del]
  1.1558 -
  1.1559 -definition divide_poly_list :: "'a::idom_divide poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1.1560 -  "divide_poly_list f g =
  1.1561 -    (let cg = coeffs g
  1.1562 -     in if cg = [] then g
  1.1563 -        else let cf = coeffs f; cgr = rev cg
  1.1564 -          in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
  1.1565 -
  1.1566 -lemmas pdivmod_via_divmod_list[code] = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1]
  1.1567 -
  1.1568 -lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n"
  1.1569 -  by  (induct n arbitrary: q r d, auto simp: Let_def)
  1.1570 -
  1.1571 -lemma mod_poly_code[code]: "f mod g =
  1.1572 -    (let cg = coeffs g
  1.1573 -     in if cg = [] then f
  1.1574 -        else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
  1.1575 -                 r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
  1.1576 -             in poly_of_list (rev r))" (is "?l = ?r")
  1.1577 -proof -
  1.1578 -  have "?l = snd (pdivmod f g)" unfolding pdivmod_def by simp
  1.1579 -  also have "\<dots> = ?r" unfolding pdivmod_via_divmod_list Let_def
  1.1580 -     mod_poly_one_main_list[symmetric, of _ _ _ Nil] by (auto split: prod.splits)
  1.1581 -  finally show ?thesis .
  1.1582 -qed
  1.1583 -
  1.1584 -definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 
  1.1585 -  "div_field_poly_impl f g = (
  1.1586 -    let cg = coeffs g
  1.1587 -      in if cg = [] then 0
  1.1588 -        else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
  1.1589 -                 q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
  1.1590 -             in poly_of_list ((map (op * ilc) q)))"
  1.1591 -
  1.1592 -text \<open>We do not declare the following lemma as code equation, since then polynomial division 
  1.1593 -  on non-fields will no longer be executable. However, a code-unfold is possible, since 
  1.1594 -  \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close>
  1.1595 -lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl"
  1.1596 -proof (intro ext)
  1.1597 -  fix f g :: "'a poly"
  1.1598 -  have "f div g = fst (pdivmod f g)" unfolding pdivmod_def by simp
  1.1599 -  also have "\<dots> = div_field_poly_impl f g" unfolding 
  1.1600 -    div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits)
  1.1601 -  finally show "f div g =  div_field_poly_impl f g" .
  1.1602 -qed
  1.1603 -
  1.1604 -
  1.1605 -lemma divide_poly_main_list:
  1.1606 -  assumes lc0: "lc \<noteq> 0"
  1.1607 -  and lc:"last d = lc"
  1.1608 -  and d:"d \<noteq> []"
  1.1609 -  and "n = (1 + length r - length d)"
  1.1610 -  shows 
  1.1611 -  "Poly (divide_poly_main_list lc q (rev r) (rev d) n) =
  1.1612 -  divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n"
  1.1613 -using assms(4-)
  1.1614 -proof(induct "n" arbitrary: r q)
  1.1615 -case (Suc n r q)
  1.1616 -  have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
  1.1617 -  have r: "r \<noteq> []"
  1.1618 -    using ifCond d using Suc_leI length_greater_0_conv list.size(3) by fastforce
  1.1619 -  then obtain rr lcr where r: "r = rr @ [lcr]" by (cases r rule: rev_cases, auto)
  1.1620 -  from d lc obtain dd where d: "d = dd @ [lc]" 
  1.1621 -    by (cases d rule: rev_cases, auto)
  1.1622 -  from Suc(2) ifCond have n: "n = 1 + length rr - length d" by (auto simp: r)
  1.1623 -  from ifCond have len: "length dd \<le> length rr" by (simp add: r d)
  1.1624 -  show ?case
  1.1625 -  proof (cases "lcr div lc * lc = lcr")
  1.1626 -    case False
  1.1627 -    thus ?thesis unfolding Suc(2)[symmetric] using r d
  1.1628 -      by (auto simp add: Let_def nth_default_append)
  1.1629 -  next
  1.1630 -    case True
  1.1631 -    hence id:
  1.1632 -    "?thesis = (Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
  1.1633 -         (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) = 
  1.1634 -      divide_poly_main lc
  1.1635 -           (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
  1.1636 -           (Poly r - monom (lcr div lc) n * Poly d)
  1.1637 -           (Poly d) (length rr - 1) n)"
  1.1638 -           using r d 
  1.1639 -      by (cases r rule: rev_cases; cases "d" rule: rev_cases; 
  1.1640 -        auto simp add: Let_def rev_map nth_default_append)      
  1.1641 -    have cong: "\<And> x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  1.1642 -      divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n" by simp
  1.1643 -    show ?thesis unfolding id 
  1.1644 -    proof (subst Suc(1), simp add: n,
  1.1645 -      subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases)
  1.1646 -      case 2 
  1.1647 -      have "monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)"
  1.1648 -        by (simp add: mult_monom len True)
  1.1649 -      thus ?case unfolding r d Poly_append n ring_distribs
  1.1650 -        by (auto simp: Poly_map smult_monom smult_monom_mult)
  1.1651 -    qed (auto simp: len monom_Suc smult_monom)
  1.1652 -  qed
  1.1653 -qed simp
  1.1654 -
  1.1655 -
  1.1656 -lemma divide_poly_list[code]: "f div g = divide_poly_list f g" 
  1.1657 -proof -
  1.1658 -  note d = divide_poly_def divide_poly_list_def
  1.1659 -  show ?thesis
  1.1660 -  proof (cases "g = 0")
  1.1661 -    case True
  1.1662 -    show ?thesis unfolding d True by auto
  1.1663 -  next
  1.1664 -    case False
  1.1665 -    then obtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases, auto)    
  1.1666 -    with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False" by auto
  1.1667 -    from cg False have lcg: "coeff g (degree g) = lcg" 
  1.1668 -      using last_coeffs_eq_coeff_degree last_snoc by force
  1.1669 -    with False have lcg0: "lcg \<noteq> 0" by auto
  1.1670 -    from cg have ltp: "Poly (cg @ [lcg]) = g"
  1.1671 -     using Poly_coeffs [of g] by auto
  1.1672 -    show ?thesis unfolding d cg Let_def id if_False poly_of_list_def
  1.1673 -      by (subst divide_poly_main_list, insert False cg lcg0, auto simp: lcg ltp,
  1.1674 -      simp add: degree_eq_length_coeffs)
  1.1675 -  qed
  1.1676 -qed
  1.1677 -
  1.1678 -subsection \<open>Order of polynomial roots\<close>
  1.1679 +    
  1.1680 +subsubsection \<open>Order of polynomial roots\<close>
  1.1681  
  1.1682  definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  1.1683  where
  1.1684 @@ -2984,6 +1787,124 @@
  1.1685  lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
  1.1686    by (subst (asm) order_root) auto
  1.1687  
  1.1688 +lemma order_unique_lemma:
  1.1689 +  fixes p :: "'a::idom poly"
  1.1690 +  assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
  1.1691 +  shows "n = order a p"
  1.1692 +unfolding Polynomial.order_def
  1.1693 +apply (rule Least_equality [symmetric])
  1.1694 +apply (fact assms)
  1.1695 +apply (rule classical)
  1.1696 +apply (erule notE)
  1.1697 +unfolding not_less_eq_eq
  1.1698 +using assms(1) apply (rule power_le_dvd)
  1.1699 +apply assumption
  1.1700 +  done
  1.1701 +    
  1.1702 +lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
  1.1703 +proof -
  1.1704 +  define i where "i = order a p"
  1.1705 +  define j where "j = order a q"
  1.1706 +  define t where "t = [:-a, 1:]"
  1.1707 +  have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
  1.1708 +    unfolding t_def by (simp add: dvd_iff_poly_eq_0)
  1.1709 +  assume "p * q \<noteq> 0"
  1.1710 +  then show "order a (p * q) = i + j"
  1.1711 +    apply clarsimp
  1.1712 +    apply (drule order [where a=a and p=p, folded i_def t_def])
  1.1713 +    apply (drule order [where a=a and p=q, folded j_def t_def])
  1.1714 +    apply clarify
  1.1715 +    apply (erule dvdE)+
  1.1716 +    apply (rule order_unique_lemma [symmetric], fold t_def)
  1.1717 +    apply (simp_all add: power_add t_dvd_iff)
  1.1718 +    done
  1.1719 +qed
  1.1720 +
  1.1721 +lemma order_smult:
  1.1722 +  assumes "c \<noteq> 0" 
  1.1723 +  shows "order x (smult c p) = order x p"
  1.1724 +proof (cases "p = 0")
  1.1725 +  case False
  1.1726 +  have "smult c p = [:c:] * p" by simp
  1.1727 +  also from assms False have "order x \<dots> = order x [:c:] + order x p" 
  1.1728 +    by (subst order_mult) simp_all
  1.1729 +  also from assms have "order x [:c:] = 0" by (intro order_0I) auto
  1.1730 +  finally show ?thesis by simp
  1.1731 +qed simp
  1.1732 +
  1.1733 +(* Next two lemmas contributed by Wenda Li *)
  1.1734 +lemma order_1_eq_0 [simp]:"order x 1 = 0" 
  1.1735 +  by (metis order_root poly_1 zero_neq_one)
  1.1736 +
  1.1737 +lemma order_power_n_n: "order a ([:-a,1:]^n)=n" 
  1.1738 +proof (induct n) (*might be proved more concisely using nat_less_induct*)
  1.1739 +  case 0
  1.1740 +  thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
  1.1741 +next 
  1.1742 +  case (Suc n)
  1.1743 +  have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" 
  1.1744 +    by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral 
  1.1745 +      one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
  1.1746 +  moreover have "order a [:-a,1:]=1" unfolding order_def
  1.1747 +    proof (rule Least_equality,rule ccontr)
  1.1748 +      assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
  1.1749 +      hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
  1.1750 +      hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )" 
  1.1751 +        by (rule dvd_imp_degree_le,auto) 
  1.1752 +      thus False by auto
  1.1753 +    next
  1.1754 +      fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
  1.1755 +      show "1 \<le> y" 
  1.1756 +        proof (rule ccontr)
  1.1757 +          assume "\<not> 1 \<le> y"
  1.1758 +          hence "y=0" by auto
  1.1759 +          hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
  1.1760 +          thus False using asm by auto
  1.1761 +        qed
  1.1762 +    qed
  1.1763 +  ultimately show ?case using Suc by auto
  1.1764 +qed
  1.1765 +
  1.1766 +lemma order_0_monom [simp]:
  1.1767 +  assumes "c \<noteq> 0"
  1.1768 +  shows   "order 0 (monom c n) = n"
  1.1769 +  using assms order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
  1.1770 +
  1.1771 +lemma dvd_imp_order_le:
  1.1772 +  "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
  1.1773 +  by (auto simp: order_mult elim: dvdE)
  1.1774 +
  1.1775 +text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
  1.1776 +
  1.1777 +lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
  1.1778 +apply (cases "p = 0", auto)
  1.1779 +apply (drule order_2 [where a=a and p=p])
  1.1780 +apply (metis not_less_eq_eq power_le_dvd)
  1.1781 +apply (erule power_le_dvd [OF order_1])
  1.1782 +done
  1.1783 +
  1.1784 +lemma order_decomp:
  1.1785 +  assumes "p \<noteq> 0"
  1.1786 +  shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
  1.1787 +proof -
  1.1788 +  from assms have A: "[:- a, 1:] ^ order a p dvd p"
  1.1789 +    and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
  1.1790 +  from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
  1.1791 +  with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
  1.1792 +    by simp
  1.1793 +  then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
  1.1794 +    by simp
  1.1795 +  then have D: "\<not> [:- a, 1:] dvd q"
  1.1796 +    using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
  1.1797 +    by auto
  1.1798 +  from C D show ?thesis by blast
  1.1799 +qed
  1.1800 +
  1.1801 +lemma monom_1_dvd_iff:
  1.1802 +  assumes "p \<noteq> 0"
  1.1803 +  shows   "monom 1 n dvd p \<longleftrightarrow> n \<le> order 0 p"
  1.1804 +  using assms order_divides[of 0 n p] by (simp add: monom_altdef)
  1.1805 +
  1.1806  
  1.1807  subsection \<open>Additional induction rules on polynomials\<close>
  1.1808  
  1.1809 @@ -3053,7 +1974,7 @@
  1.1810    finally show ?thesis .
  1.1811  qed
  1.1812  
  1.1813 -
  1.1814 +  
  1.1815  subsection \<open>Composition of polynomials\<close>
  1.1816  
  1.1817  (* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
  1.1818 @@ -3256,7 +2177,6 @@
  1.1819  lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)"
  1.1820    by (auto simp add: nth_default_def add_ac)
  1.1821    
  1.1822 -  
  1.1823  lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)"
  1.1824  proof -
  1.1825    from MOST_coeff_eq_0[of p] obtain m where "\<forall>k>m. coeff p k = 0" by (auto simp: MOST_nat)
  1.1826 @@ -3444,7 +2364,7 @@
  1.1827    reflect_poly_power reflect_poly_prod reflect_poly_prod_list
  1.1828  
  1.1829  
  1.1830 -subsection \<open>Derivatives of univariate polynomials\<close>
  1.1831 +subsection \<open>Derivatives\<close>
  1.1832  
  1.1833  function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly \<Rightarrow> 'a poly"
  1.1834  where
  1.1835 @@ -3737,6 +2657,136 @@
  1.1836    qed
  1.1837  qed
  1.1838  
  1.1839 +lemma lemma_order_pderiv1:
  1.1840 +  "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
  1.1841 +    smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
  1.1842 +apply (simp only: pderiv_mult pderiv_power_Suc)
  1.1843 +apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
  1.1844 +done
  1.1845 +
  1.1846 +lemma lemma_order_pderiv:
  1.1847 +  fixes p :: "'a :: field_char_0 poly"
  1.1848 +  assumes n: "0 < n" 
  1.1849 +      and pd: "pderiv p \<noteq> 0" 
  1.1850 +      and pe: "p = [:- a, 1:] ^ n * q" 
  1.1851 +      and nd: "~ [:- a, 1:] dvd q"
  1.1852 +    shows "n = Suc (order a (pderiv p))"
  1.1853 +using n 
  1.1854 +proof -
  1.1855 +  have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
  1.1856 +    using assms by auto
  1.1857 +  obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
  1.1858 +    using assms by (cases n) auto
  1.1859 +  have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
  1.1860 +    by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
  1.1861 +  have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
  1.1862 +  proof (rule order_unique_lemma)
  1.1863 +    show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  1.1864 +      apply (subst lemma_order_pderiv1)
  1.1865 +      apply (rule dvd_add)
  1.1866 +      apply (metis dvdI dvd_mult2 power_Suc2)
  1.1867 +      apply (metis dvd_smult dvd_triv_right)
  1.1868 +      done
  1.1869 +  next
  1.1870 +    show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  1.1871 +     apply (subst lemma_order_pderiv1)
  1.1872 +     by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
  1.1873 +  qed
  1.1874 +  then show ?thesis
  1.1875 +    by (metis \<open>n = Suc n'\<close> pe)
  1.1876 +qed
  1.1877 +
  1.1878 +lemma order_pderiv:
  1.1879 +  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
  1.1880 +     (order a p = Suc (order a (pderiv p)))"
  1.1881 +apply (case_tac "p = 0", simp)
  1.1882 +apply (drule_tac a = a and p = p in order_decomp)
  1.1883 +using neq0_conv
  1.1884 +apply (blast intro: lemma_order_pderiv)
  1.1885 +done
  1.1886 +
  1.1887 +lemma poly_squarefree_decomp_order:
  1.1888 +  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  1.1889 +  and p: "p = q * d"
  1.1890 +  and p': "pderiv p = e * d"
  1.1891 +  and d: "d = r * p + s * pderiv p"
  1.1892 +  shows "order a q = (if order a p = 0 then 0 else 1)"
  1.1893 +proof (rule classical)
  1.1894 +  assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)"
  1.1895 +  from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  1.1896 +  with p have "order a p = order a q + order a d"
  1.1897 +    by (simp add: order_mult)
  1.1898 +  with 1 have "order a p \<noteq> 0" by (auto split: if_splits)
  1.1899 +  have "order a (pderiv p) = order a e + order a d"
  1.1900 +    using \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> by (simp add: order_mult)
  1.1901 +  have "order a p = Suc (order a (pderiv p))"
  1.1902 +    using \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> by (rule order_pderiv)
  1.1903 +  have "d \<noteq> 0" using \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> by simp
  1.1904 +  have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
  1.1905 +    apply (simp add: d)
  1.1906 +    apply (rule dvd_add)
  1.1907 +    apply (rule dvd_mult)
  1.1908 +    apply (simp add: order_divides \<open>p \<noteq> 0\<close>
  1.1909 +           \<open>order a p = Suc (order a (pderiv p))\<close>)
  1.1910 +    apply (rule dvd_mult)
  1.1911 +    apply (simp add: order_divides)
  1.1912 +    done
  1.1913 +  then have "order a (pderiv p) \<le> order a d"
  1.1914 +    using \<open>d \<noteq> 0\<close> by (simp add: order_divides)
  1.1915 +  show ?thesis
  1.1916 +    using \<open>order a p = order a q + order a d\<close>
  1.1917 +    using \<open>order a (pderiv p) = order a e + order a d\<close>
  1.1918 +    using \<open>order a p = Suc (order a (pderiv p))\<close>
  1.1919 +    using \<open>order a (pderiv p) \<le> order a d\<close>
  1.1920 +    by auto
  1.1921 +qed
  1.1922 +
  1.1923 +lemma poly_squarefree_decomp_order2: 
  1.1924 +     "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
  1.1925 +       p = q * d;
  1.1926 +       pderiv p = e * d;
  1.1927 +       d = r * p + s * pderiv p
  1.1928 +      \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  1.1929 +by (blast intro: poly_squarefree_decomp_order)
  1.1930 +
  1.1931 +lemma order_pderiv2: 
  1.1932 +  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
  1.1933 +      \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
  1.1934 +by (auto dest: order_pderiv)
  1.1935 +
  1.1936 +definition rsquarefree :: "'a::idom poly \<Rightarrow> bool"
  1.1937 +  where "rsquarefree p \<longleftrightarrow> p \<noteq> 0 \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
  1.1938 +
  1.1939 +lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
  1.1940 +  by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
  1.1941 +
  1.1942 +lemma rsquarefree_roots:
  1.1943 +  fixes p :: "'a :: field_char_0 poly"
  1.1944 +  shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
  1.1945 +apply (simp add: rsquarefree_def)
  1.1946 +apply (case_tac "p = 0", simp, simp)
  1.1947 +apply (case_tac "pderiv p = 0")
  1.1948 +apply simp
  1.1949 +apply (drule pderiv_iszero, clarsimp)
  1.1950 +apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
  1.1951 +apply (force simp add: order_root order_pderiv2)
  1.1952 +  done
  1.1953 +
  1.1954 +lemma poly_squarefree_decomp:
  1.1955 +  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  1.1956 +    and "p = q * d"
  1.1957 +    and "pderiv p = e * d"
  1.1958 +    and "d = r * p + s * pderiv p"
  1.1959 +  shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
  1.1960 +proof -
  1.1961 +  from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  1.1962 +  with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
  1.1963 +  have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  1.1964 +    using assms by (rule poly_squarefree_decomp_order2)
  1.1965 +  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
  1.1966 +    by (simp add: rsquarefree_def order_root)
  1.1967 +qed
  1.1968 +
  1.1969  
  1.1970  subsection \<open>Algebraic numbers\<close>
  1.1971  
  1.1972 @@ -3762,25 +2812,6 @@
  1.1973    obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
  1.1974    using assms unfolding algebraic_def by blast
  1.1975  
  1.1976 -lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
  1.1977 -  using quotient_of_denom_pos[OF surjective_pairing] .
  1.1978 -  
  1.1979 -lemma of_int_div_in_Ints: 
  1.1980 -  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: ring_div set)"
  1.1981 -proof (cases "of_int b = (0 :: 'a)")
  1.1982 -  assume "b dvd a" "of_int b \<noteq> (0::'a)"
  1.1983 -  then obtain c where "a = b * c" by (elim dvdE)
  1.1984 -  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
  1.1985 -qed auto
  1.1986 -
  1.1987 -lemma of_int_divide_in_Ints: 
  1.1988 -  "b dvd a \<Longrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: field set)"
  1.1989 -proof (cases "of_int b = (0 :: 'a)")
  1.1990 -  assume "b dvd a" "of_int b \<noteq> (0::'a)"
  1.1991 -  then obtain c where "a = b * c" by (elim dvdE)
  1.1992 -  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
  1.1993 -qed auto
  1.1994 -
  1.1995  lemma algebraic_altdef:
  1.1996    fixes p :: "'a :: field_char_0 poly"
  1.1997    shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
  1.1998 @@ -3835,285 +2866,1426 @@
  1.1999  qed
  1.2000  
  1.2001  
  1.2002 -text\<open>Lemmas for Derivatives\<close>
  1.2003 -
  1.2004 -lemma order_unique_lemma:
  1.2005 -  fixes p :: "'a::idom poly"
  1.2006 -  assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
  1.2007 -  shows "n = order a p"
  1.2008 -unfolding Polynomial.order_def
  1.2009 -apply (rule Least_equality [symmetric])
  1.2010 -apply (fact assms)
  1.2011 -apply (rule classical)
  1.2012 -apply (erule notE)
  1.2013 -unfolding not_less_eq_eq
  1.2014 -using assms(1) apply (rule power_le_dvd)
  1.2015 -apply assumption
  1.2016 -done
  1.2017 -
  1.2018 -lemma lemma_order_pderiv1:
  1.2019 -  "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
  1.2020 -    smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
  1.2021 -apply (simp only: pderiv_mult pderiv_power_Suc)
  1.2022 -apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
  1.2023 -done
  1.2024 -
  1.2025 -lemma lemma_order_pderiv:
  1.2026 -  fixes p :: "'a :: field_char_0 poly"
  1.2027 -  assumes n: "0 < n" 
  1.2028 -      and pd: "pderiv p \<noteq> 0" 
  1.2029 -      and pe: "p = [:- a, 1:] ^ n * q" 
  1.2030 -      and nd: "~ [:- a, 1:] dvd q"
  1.2031 -    shows "n = Suc (order a (pderiv p))"
  1.2032 -using n 
  1.2033 +subsection \<open>Content and primitive part of a polynomial\<close>
  1.2034 +
  1.2035 +definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
  1.2036 +  "content p = Gcd (set (coeffs p))"
  1.2037 +
  1.2038 +lemma content_0 [simp]: "content 0 = 0"
  1.2039 +  by (simp add: content_def)
  1.2040 +
  1.2041 +lemma content_1 [simp]: "content 1 = 1"
  1.2042 +  by (simp add: content_def)
  1.2043 +
  1.2044 +lemma content_const [simp]: "content [:c:] = normalize c"
  1.2045 +  by (simp add: content_def cCons_def)
  1.2046 +
  1.2047 +lemma const_poly_dvd_iff_dvd_content:
  1.2048 +  fixes c :: "'a :: semiring_Gcd"
  1.2049 +  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
  1.2050 +proof (cases "p = 0")
  1.2051 +  case [simp]: False
  1.2052 +  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
  1.2053 +  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
  1.2054 +  proof safe
  1.2055 +    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
  1.2056 +    thus "c dvd coeff p n"
  1.2057 +      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
  1.2058 +  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
  1.2059 +  also have "\<dots> \<longleftrightarrow> c dvd content p"
  1.2060 +    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
  1.2061 +          dvd_mult_unit_iff)
  1.2062 +  finally show ?thesis .
  1.2063 +qed simp_all
  1.2064 +
  1.2065 +lemma content_dvd [simp]: "[:content p:] dvd p"
  1.2066 +  by (subst const_poly_dvd_iff_dvd_content) simp_all
  1.2067 +  
  1.2068 +lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
  1.2069 +  by (cases "n \<le> degree p") 
  1.2070 +     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
  1.2071 +
  1.2072 +lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
  1.2073 +  by (simp add: content_def Gcd_dvd)
  1.2074 +
  1.2075 +lemma normalize_content [simp]: "normalize (content p) = content p"
  1.2076 +  by (simp add: content_def)
  1.2077 +
  1.2078 +lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
  1.2079 +proof
  1.2080 +  assume "is_unit (content p)"
  1.2081 +  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
  1.2082 +  thus "content p = 1" by simp
  1.2083 +qed auto
  1.2084 +
  1.2085 +lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
  1.2086 +  by (simp add: content_def coeffs_smult Gcd_mult)
  1.2087 +
  1.2088 +lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
  1.2089 +  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
  1.2090 +
  1.2091 +definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
  1.2092 +  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
  1.2093 +  
  1.2094 +lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
  1.2095 +  by (simp add: primitive_part_def)
  1.2096 +
  1.2097 +lemma content_times_primitive_part [simp]:
  1.2098 +  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
  1.2099 +  shows "smult (content p) (primitive_part p) = p"
  1.2100 +proof (cases "p = 0")
  1.2101 +  case False
  1.2102 +  thus ?thesis
  1.2103 +  unfolding primitive_part_def
  1.2104 +  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
  1.2105 +           intro: map_poly_idI)
  1.2106 +qed simp_all
  1.2107 +
  1.2108 +lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
  1.2109 +proof (cases "p = 0")
  1.2110 +  case False
  1.2111 +  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
  1.2112 +    by (simp add:  primitive_part_def)
  1.2113 +  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
  1.2114 +    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
  1.2115 +  finally show ?thesis using False by simp
  1.2116 +qed simp
  1.2117 +
  1.2118 +lemma content_primitive_part [simp]:
  1.2119 +  assumes "p \<noteq> 0"
  1.2120 +  shows   "content (primitive_part p) = 1"
  1.2121  proof -
  1.2122 -  have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
  1.2123 -    using assms by auto
  1.2124 -  obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
  1.2125 -    using assms by (cases n) auto
  1.2126 -  have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
  1.2127 -    by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
  1.2128 -  have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
  1.2129 -  proof (rule order_unique_lemma)
  1.2130 -    show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  1.2131 -      apply (subst lemma_order_pderiv1)
  1.2132 -      apply (rule dvd_add)
  1.2133 -      apply (metis dvdI dvd_mult2 power_Suc2)
  1.2134 -      apply (metis dvd_smult dvd_triv_right)
  1.2135 -      done
  1.2136 +  have "p = smult (content p) (primitive_part p)" by simp
  1.2137 +  also have "content \<dots> = content p * content (primitive_part p)" 
  1.2138 +    by (simp del: content_times_primitive_part)
  1.2139 +  finally show ?thesis using assms by simp
  1.2140 +qed
  1.2141 +
  1.2142 +lemma content_decompose:
  1.2143 +  fixes p :: "'a :: semiring_Gcd poly"
  1.2144 +  obtains p' where "p = smult (content p) p'" "content p' = 1"
  1.2145 +proof (cases "p = 0")
  1.2146 +  case True
  1.2147 +  thus ?thesis by (intro that[of 1]) simp_all
  1.2148 +next
  1.2149 +  case False
  1.2150 +  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
  1.2151 +  have "content p * 1 = content p * content r" by (subst r) simp
  1.2152 +  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
  1.2153 +  with r show ?thesis by (intro that[of r]) simp_all
  1.2154 +qed
  1.2155 +
  1.2156 +lemma content_dvd_contentI [intro]:
  1.2157 +  "p dvd q \<Longrightarrow> content p dvd content q"
  1.2158 +  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
  1.2159 +  
  1.2160 +lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
  1.2161 +  by (simp add: primitive_part_def map_poly_pCons)
  1.2162 + 
  1.2163 +lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
  1.2164 +  by (auto simp: primitive_part_def)
  1.2165 +  
  1.2166 +lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
  1.2167 +proof (cases "p = 0")
  1.2168 +  case False
  1.2169 +  have "p = smult (content p) (primitive_part p)" by simp
  1.2170 +  also from False have "degree \<dots> = degree (primitive_part p)"
  1.2171 +    by (subst degree_smult_eq) simp_all
  1.2172 +  finally show ?thesis ..
  1.2173 +qed simp_all
  1.2174 +
  1.2175 +
  1.2176 +subsection \<open>Division of polynomials\<close>
  1.2177 +
  1.2178 +subsubsection \<open>Division in general\<close>
  1.2179 +  
  1.2180 +instantiation poly :: (idom_divide) idom_divide
  1.2181 +begin
  1.2182 +
  1.2183 +fun divide_poly_main :: "'a \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly 
  1.2184 +  \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly" where
  1.2185 +  "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in 
  1.2186 +     if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
  1.2187 +     divide_poly_main 
  1.2188 +       lc 
  1.2189 +       (q + mon) 
  1.2190 +       (r - mon * d) 
  1.2191 +       d (dr - 1) n else 0)"
  1.2192 +| "divide_poly_main lc q r d dr 0 = q"
  1.2193 +
  1.2194 +definition divide_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1.2195 +  "divide_poly f g = (if g = 0 then 0 else
  1.2196 +     divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))" 
  1.2197 +
  1.2198 +lemma divide_poly_main:
  1.2199 +  assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
  1.2200 +    and *: "degree (d * r) \<le> dr" "divide_poly_main lc q (d * r) d dr n = q'" 
  1.2201 +    "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> d * r = 0" 
  1.2202 +  shows "q' = q + r"
  1.2203 +  using *
  1.2204 +proof (induct n arbitrary: q r dr)
  1.2205 +  case (Suc n q r dr)
  1.2206 +  let ?rr = "d * r"
  1.2207 +  let ?a = "coeff ?rr dr"
  1.2208 +  let ?qq = "?a div lc"
  1.2209 +  define b where [simp]: "b = monom ?qq n"
  1.2210 +  let ?rrr =  "d * (r - b)"
  1.2211 +  let ?qqq = "q + b"
  1.2212 +  note res = Suc(3)
  1.2213 +  have dr: "dr = n + degree d" using Suc(4) by auto
  1.2214 +  have lc: "lc \<noteq> 0" using d by auto
  1.2215 +  have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
  1.2216 +  proof (cases "?qq = 0")
  1.2217 +    case False
  1.2218 +    hence n: "n = degree b" by (simp add: degree_monom_eq)
  1.2219 +    show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
  1.2220 +  qed simp
  1.2221 +  also have "\<dots> = lc * coeff b n" unfolding d by simp
  1.2222 +  finally have c2: "coeff (b * d) dr = lc * coeff b n" .
  1.2223 +  have rrr: "?rrr = ?rr - b * d" by (simp add: field_simps)
  1.2224 +  have c1: "coeff (d * r) dr = lc * coeff r n"
  1.2225 +  proof (cases "degree r = n")
  1.2226 +    case True
  1.2227 +    thus ?thesis using Suc(2) unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps)
  1.2228    next
  1.2229 -    show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  1.2230 -     apply (subst lemma_order_pderiv1)
  1.2231 -     by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
  1.2232 +    case False
  1.2233 +    have "degree r \<le> n" using dr Suc(2) by auto
  1.2234 +      (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq diff_is_0_eq diff_zero le_cases)
  1.2235 +    with False have r_n: "degree r < n" by auto
  1.2236 +    hence right: "lc * coeff r n = 0" by (simp add: coeff_eq_0)
  1.2237 +    have "coeff (d * r) dr = coeff (d * r) (degree d + n)" unfolding dr by (simp add: ac_simps)
  1.2238 +    also have "\<dots> = 0" using r_n
  1.2239 +      by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0 
  1.2240 +        coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq)
  1.2241 +    finally show ?thesis unfolding right .
  1.2242 +  qed
  1.2243 +  have c0: "coeff ?rrr dr = 0" 
  1.2244 +    and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr" unfolding rrr coeff_diff c2
  1.2245 +    unfolding b_def coeff_monom coeff_smult c1 using lc by auto
  1.2246 +  from res[unfolded divide_poly_main.simps[of lc q] Let_def] id
  1.2247 +  have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'" 
  1.2248 +    by (simp del: divide_poly_main.simps add: field_simps)
  1.2249 +  note IH = Suc(1)[OF _ res] 
  1.2250 +  have dr: "dr = n + degree d" using Suc(4) by auto
  1.2251 +  have deg_rr: "degree ?rr \<le> dr" using Suc(2) by auto
  1.2252 +  have deg_bd: "degree (b * d) \<le> dr"
  1.2253 +    unfolding dr b_def by (rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
  1.2254 +  have "degree ?rrr \<le> dr" unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd])
  1.2255 +  with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)"
  1.2256 +    by (rule coeff_0_degree_minus_1)
  1.2257 +  have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"  
  1.2258 +  proof (cases dr)
  1.2259 +    case 0
  1.2260 +    with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
  1.2261 +    with deg_rrr have "degree ?rrr = 0" by simp
  1.2262 +    from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]" by metis
  1.2263 +    show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
  1.2264 +  qed (insert Suc(4), auto)
  1.2265 +  note IH = IH[OF deg_rrr this]
  1.2266 +  show ?case using IH by simp
  1.2267 +next
  1.2268 +  case (0 q r dr)
  1.2269 +  show ?case 
  1.2270 +  proof (cases "r = 0")
  1.2271 +    case True
  1.2272 +    thus ?thesis using 0 by auto
  1.2273 +  next
  1.2274 +    case False
  1.2275 +    have "degree (d * r) = degree d + degree r" using d False 
  1.2276 +      by (subst degree_mult_eq, auto)
  1.2277 +    thus ?thesis using 0 d by auto
  1.2278 +  qed
  1.2279 +qed 
  1.2280 +
  1.2281 +lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0"
  1.2282 +proof (induct n arbitrary: r d dr)
  1.2283 +  case (Suc n r d dr)
  1.2284 +  show ?case unfolding divide_poly_main.simps[of _ _ r] Let_def
  1.2285 +    by (simp add: Suc del: divide_poly_main.simps)
  1.2286 +qed simp
  1.2287 +
  1.2288 +lemma divide_poly:
  1.2289 +  assumes g: "g \<noteq> 0"
  1.2290 +  shows "(f * g) div g = (f :: 'a poly)" 
  1.2291 +proof - 
  1.2292 +  have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs  g)) 
  1.2293 +    = (f * g) div g" unfolding divide_poly_def Let_def by (simp add: ac_simps)
  1.2294 +  note main = divide_poly_main[OF g refl le_refl this]
  1.2295 +  {
  1.2296 +    fix f :: "'a poly"
  1.2297 +    assume "f \<noteq> 0"
  1.2298 +    hence "length (coeffs f) = Suc (degree f)" unfolding degree_eq_length_coeffs by auto
  1.2299 +  } note len = this
  1.2300 +  have "(f * g) div g = 0 + f"
  1.2301 +  proof (rule main, goal_cases)
  1.2302 +    case 1
  1.2303 +    show ?case
  1.2304 +    proof (cases "f = 0")
  1.2305 +      case True
  1.2306 +      with g show ?thesis by (auto simp: degree_eq_length_coeffs)
  1.2307 +    next
  1.2308 +      case False
  1.2309 +      with g have fg: "g * f \<noteq> 0" by auto
  1.2310 +      show ?thesis unfolding len[OF fg] len[OF g] by auto
  1.2311 +    qed
  1.2312    qed
  1.2313 -  then show ?thesis
  1.2314 -    by (metis \<open>n = Suc n'\<close> pe)
  1.2315 +  thus ?thesis by simp
  1.2316 +qed
  1.2317 +
  1.2318 +lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
  1.2319 +  by (simp add: divide_poly_def Let_def divide_poly_main_0)
  1.2320 +
  1.2321 +instance
  1.2322 +  by standard (auto simp: divide_poly divide_poly_0)
  1.2323 +
  1.2324 +end
  1.2325 +
  1.2326 +instance poly :: (idom_divide) algebraic_semidom ..
  1.2327 +
  1.2328 +lemma div_const_poly_conv_map_poly: 
  1.2329 +  assumes "[:c:] dvd p"
  1.2330 +  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
  1.2331 +proof (cases "c = 0")
  1.2332 +  case False
  1.2333 +  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
  1.2334 +  moreover {
  1.2335 +    have "smult c q = [:c:] * q" by simp
  1.2336 +    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
  1.2337 +    finally have "smult c q div [:c:] = q" .
  1.2338 +  }
  1.2339 +  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
  1.2340 +qed (auto intro!: poly_eqI simp: coeff_map_poly)
  1.2341 +
  1.2342 +lemma is_unit_monom_0:
  1.2343 +  fixes a :: "'a::field"
  1.2344 +  assumes "a \<noteq> 0"
  1.2345 +  shows "is_unit (monom a 0)"
  1.2346 +proof
  1.2347 +  from assms show "1 = monom a 0 * monom (inverse a) 0"
  1.2348 +    by (simp add: mult_monom)
  1.2349  qed
  1.2350  
  1.2351 -lemma order_decomp:
  1.2352 -  assumes "p \<noteq> 0"
  1.2353 -  shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
  1.2354 +lemma is_unit_triv:
  1.2355 +  fixes a :: "'a::field"
  1.2356 +  assumes "a \<noteq> 0"
  1.2357 +  shows "is_unit [:a:]"
  1.2358 +  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
  1.2359 +
  1.2360 +lemma is_unit_iff_degree:
  1.2361 +  assumes "p \<noteq> (0 :: _ :: field poly)"
  1.2362 +  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
  1.2363 +proof
  1.2364 +  assume ?Q
  1.2365 +  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
  1.2366 +  with assms show ?P by (simp add: is_unit_triv)
  1.2367 +next
  1.2368 +  assume ?P
  1.2369 +  then obtain q where "q \<noteq> 0" "p * q = 1" ..
  1.2370 +  then have "degree (p * q) = degree 1"
  1.2371 +    by simp
  1.2372 +  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
  1.2373 +    by (simp add: degree_mult_eq)
  1.2374 +  then show ?Q by simp
  1.2375 +qed
  1.2376 +
  1.2377 +lemma is_unit_pCons_iff:
  1.2378 +  "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
  1.2379 +  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
  1.2380 +
  1.2381 +lemma is_unit_monom_trival:
  1.2382 +  fixes p :: "'a::field poly"
  1.2383 +  assumes "is_unit p"
  1.2384 +  shows "monom (coeff p (degree p)) 0 = p"
  1.2385 +  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
  1.2386 +
  1.2387 +lemma is_unit_const_poly_iff: 
  1.2388 +  "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
  1.2389 +  by (auto simp: one_poly_def)
  1.2390 +
  1.2391 +lemma is_unit_polyE:
  1.2392 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
  1.2393 +  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
  1.2394  proof -
  1.2395 -  from assms have A: "[:- a, 1:] ^ order a p dvd p"
  1.2396 -    and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
  1.2397 -  from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
  1.2398 -  with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
  1.2399 +  from assms obtain q where "1 = p * q"
  1.2400 +    by (rule dvdE)
  1.2401 +  then have "p \<noteq> 0" and "q \<noteq> 0"
  1.2402 +    by auto
  1.2403 +  from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
  1.2404      by simp
  1.2405 -  then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
  1.2406 -    by simp
  1.2407 -  then have D: "\<not> [:- a, 1:] dvd q"
  1.2408 -    using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
  1.2409 -    by auto
  1.2410 -  from C D show ?thesis by blast
  1.2411 +  also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
  1.2412 +    by (simp add: degree_mult_eq)
  1.2413 +  finally have "degree p = 0" by simp
  1.2414 +  with degree_eq_zeroE obtain c where c: "p = [:c:]" .
  1.2415 +  moreover with \<open>p dvd 1\<close> have "c dvd 1"
  1.2416 +    by (simp add: is_unit_const_poly_iff)
  1.2417 +  ultimately show thesis
  1.2418 +    by (rule that)
  1.2419 +qed
  1.2420 +
  1.2421 +lemma is_unit_polyE':
  1.2422 +  assumes "is_unit (p::_::field poly)"
  1.2423 +  obtains a where "p = monom a 0" and "a \<noteq> 0"
  1.2424 +proof -
  1.2425 +  obtain a q where "p = pCons a q" by (cases p)
  1.2426 +  with assms have "p = [:a:]" and "a \<noteq> 0"
  1.2427 +    by (simp_all add: is_unit_pCons_iff)
  1.2428 +  with that show thesis by (simp add: monom_0)
  1.2429  qed
  1.2430  
  1.2431 -lemma order_pderiv:
  1.2432 -  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
  1.2433 -     (order a p = Suc (order a (pderiv p)))"
  1.2434 -apply (case_tac "p = 0", simp)
  1.2435 -apply (drule_tac a = a and p = p in order_decomp)
  1.2436 -using neq0_conv
  1.2437 -apply (blast intro: lemma_order_pderiv)
  1.2438 -done
  1.2439 -
  1.2440 -lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
  1.2441 +lemma is_unit_poly_iff:
  1.2442 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
  1.2443 +  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
  1.2444 +  by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
  1.2445 +
  1.2446 +  
  1.2447 +subsubsection \<open>Pseudo-Division\<close>
  1.2448 +
  1.2449 +text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
  1.2450 +
  1.2451 +fun pseudo_divmod_main :: "'a :: comm_ring_1  \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly 
  1.2452 +  \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly \<times> 'a poly" where
  1.2453 +  "pseudo_divmod_main lc q r d dr (Suc n) = (let
  1.2454 +     rr = smult lc r;
  1.2455 +     qq = coeff r dr;
  1.2456 +     rrr = rr - monom qq n * d;
  1.2457 +     qqq = smult lc q + monom qq n
  1.2458 +     in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
  1.2459 +| "pseudo_divmod_main lc q r d dr 0 = (q,r)"
  1.2460 +
  1.2461 +definition pseudo_divmod :: "'a :: comm_ring_1 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" where
  1.2462 +  "pseudo_divmod p q \<equiv> if q = 0 then (0,p) else
  1.2463 +     pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p) (1 + length (coeffs p) - length (coeffs q))"
  1.2464 +
  1.2465 +lemma pseudo_divmod_main: assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
  1.2466 +  and *: "degree r \<le> dr" "pseudo_divmod_main lc q r d dr n = (q',r')" 
  1.2467 +    "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> r = 0" 
  1.2468 +  shows "(r' = 0 \<or> degree r' < degree d) \<and> smult (lc^n) (d * q + r) = d * q' + r'"
  1.2469 +  using *
  1.2470 +proof (induct n arbitrary: q r dr)
  1.2471 +  case (Suc n q r dr)
  1.2472 +  let ?rr = "smult lc r"
  1.2473 +  let ?qq = "coeff r dr"
  1.2474 +  define b where [simp]: "b = monom ?qq n"
  1.2475 +  let ?rrr = "?rr - b * d"
  1.2476 +  let ?qqq = "smult lc q + b"
  1.2477 +  note res = Suc(3)
  1.2478 +  from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def] 
  1.2479 +  have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')" 
  1.2480 +    by (simp del: pseudo_divmod_main.simps)
  1.2481 +  have dr: "dr = n + degree d" using Suc(4) by auto
  1.2482 +  have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
  1.2483 +  proof (cases "?qq = 0")
  1.2484 +    case False
  1.2485 +    hence n: "n = degree b" by (simp add: degree_monom_eq)
  1.2486 +    show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
  1.2487 +  qed auto
  1.2488 +  also have "\<dots> = lc * coeff b n" unfolding d by simp
  1.2489 +  finally have "coeff (b * d) dr = lc * coeff b n" .
  1.2490 +  moreover have "coeff ?rr dr = lc * coeff r dr" by simp
  1.2491 +  ultimately have c0: "coeff ?rrr dr = 0" by auto
  1.2492 +  have dr: "dr = n + degree d" using Suc(4) by auto
  1.2493 +  have deg_rr: "degree ?rr \<le> dr" using Suc(2) 
  1.2494 +    using degree_smult_le dual_order.trans by blast 
  1.2495 +  have deg_bd: "degree (b * d) \<le> dr"
  1.2496 +    unfolding dr
  1.2497 +    by(rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
  1.2498 +  have "degree ?rrr \<le> dr"
  1.2499 +    using degree_diff_le[OF deg_rr deg_bd] by auto
  1.2500 +  with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)" by (rule coeff_0_degree_minus_1)
  1.2501 +  have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
  1.2502 +  proof (cases dr)
  1.2503 +    case 0
  1.2504 +    with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
  1.2505 +    with deg_rrr have "degree ?rrr = 0" by simp
  1.2506 +    hence "\<exists> a. ?rrr = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
  1.2507 +    from this obtain a where rrr: "?rrr = [:a:]" by auto
  1.2508 +    show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
  1.2509 +  qed (insert Suc(4), auto)
  1.2510 +  note IH = Suc(1)[OF deg_rrr res this]
  1.2511 +  show ?case
  1.2512 +  proof (intro conjI)
  1.2513 +    show "r' = 0 \<or> degree r' < degree d" using IH by blast
  1.2514 +    show "smult (lc ^ Suc n) (d * q + r) = d * q' + r'"
  1.2515 +      unfolding IH[THEN conjunct2,symmetric]
  1.2516 +      by (simp add: field_simps smult_add_right)
  1.2517 +  qed
  1.2518 +qed auto
  1.2519 +
  1.2520 +lemma pseudo_divmod:
  1.2521 +  assumes g: "g \<noteq> 0" and *: "pseudo_divmod f g = (q,r)" 
  1.2522 +  shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is ?A)
  1.2523 +    and "r = 0 \<or> degree r < degree g" (is ?B)
  1.2524  proof -
  1.2525 -  define i where "i = order a p"
  1.2526 -  define j where "j = order a q"
  1.2527 -  define t where "t = [:-a, 1:]"
  1.2528 -  have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
  1.2529 -    unfolding t_def by (simp add: dvd_iff_poly_eq_0)
  1.2530 -  assume "p * q \<noteq> 0"
  1.2531 -  then show "order a (p * q) = i + j"
  1.2532 -    apply clarsimp
  1.2533 -    apply (drule order [where a=a and p=p, folded i_def t_def])
  1.2534 -    apply (drule order [where a=a and p=q, folded j_def t_def])
  1.2535 -    apply clarify
  1.2536 -    apply (erule dvdE)+
  1.2537 -    apply (rule order_unique_lemma [symmetric], fold t_def)
  1.2538 -    apply (simp_all add: power_add t_dvd_iff)
  1.2539 -    done
  1.2540 +  from *[unfolded pseudo_divmod_def Let_def]
  1.2541 +  have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (auto simp: g)
  1.2542 +  note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl]
  1.2543 +  have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \<or>
  1.2544 +    degree f = 0 \<and> 1 + length (coeffs f) - length (coeffs g) = 0 \<and> f = 0" using g 
  1.2545 +    by (cases "f = 0"; cases "coeffs g", auto simp: degree_eq_length_coeffs)
  1.2546 +  note main = main[OF this]
  1.2547 +  from main show "r = 0 \<or> degree r < degree g" by auto
  1.2548 +  show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" 
  1.2549 +    by (subst main[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
  1.2550 +    insert g, cases "f = 0"; cases "coeffs g", auto)
  1.2551 +qed
  1.2552 +  
  1.2553 +definition "pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)"
  1.2554 +
  1.2555 +lemma snd_pseudo_divmod_main:
  1.2556 +  "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)"
  1.2557 +by (induct n arbitrary: q q' lc r d dr; simp add: Let_def)
  1.2558 +
  1.2559 +definition pseudo_mod 
  1.2560 +    :: "'a :: {comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1.2561 +  "pseudo_mod f g = snd (pseudo_divmod f g)"
  1.2562 +  
  1.2563 +lemma pseudo_mod:
  1.2564 +  fixes f g
  1.2565 +  defines "r \<equiv> pseudo_mod f g"
  1.2566 +  assumes g: "g \<noteq> 0"
  1.2567 +  shows "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" "r = 0 \<or> degree r < degree g"
  1.2568 +proof - 
  1.2569 +  let ?cg = "coeff g (degree g)"
  1.2570 +  let ?cge = "?cg ^ (Suc (degree f) - degree g)"
  1.2571 +  define a where "a = ?cge"
  1.2572 +  obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def]
  1.2573 +    by (cases "pseudo_divmod f g", auto)
  1.2574 +  from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g" 
  1.2575 +    unfolding a_def by auto
  1.2576 +  show "r = 0 \<or> degree r < degree g" by fact
  1.2577 +  from g have "a \<noteq> 0" unfolding a_def by auto
  1.2578 +  thus "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" using id by auto
  1.2579 +qed
  1.2580 +  
  1.2581 +lemma fst_pseudo_divmod_main_as_divide_poly_main:
  1.2582 +  assumes d: "d \<noteq> 0"
  1.2583 +  defines lc: "lc \<equiv> coeff d (degree d)"
  1.2584 +  shows "fst (pseudo_divmod_main lc q r d dr n) = divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n"
  1.2585 +proof(induct n arbitrary: q r dr)
  1.2586 +  case 0 then show ?case by simp
  1.2587 +next
  1.2588 +  case (Suc n)
  1.2589 +    note lc0 = leading_coeff_neq_0[OF d, folded lc]
  1.2590 +    then have "pseudo_divmod_main lc q r d dr (Suc n) =
  1.2591 +    pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n)
  1.2592 +      (smult lc r - monom (coeff r dr) n * d) d (dr - 1) n"
  1.2593 +    by (simp add: Let_def ac_simps)
  1.2594 +    also have "fst ... = divide_poly_main lc
  1.2595 +     (smult (lc^n) (smult lc q + monom (coeff r dr) n))
  1.2596 +     (smult (lc^n) (smult lc r - monom (coeff r dr) n * d))
  1.2597 +     d (dr - 1) n"
  1.2598 +      unfolding Suc[unfolded divide_poly_main.simps Let_def]..
  1.2599 +    also have "... = divide_poly_main lc (smult (lc ^ Suc n) q)
  1.2600 +        (smult (lc ^ Suc n) r) d dr (Suc n)"
  1.2601 +      unfolding smult_monom smult_distribs mult_smult_left[symmetric]
  1.2602 +      using lc0 by (simp add: Let_def ac_simps)
  1.2603 +    finally show ?case.
  1.2604  qed
  1.2605  
  1.2606 -lemma order_smult:
  1.2607 -  assumes "c \<noteq> 0" 
  1.2608 -  shows "order x (smult c p) = order x p"
  1.2609 +
  1.2610 +subsubsection \<open>Division in polynomials over fields\<close>
  1.2611 +
  1.2612 +lemma pseudo_divmod_field:
  1.2613 +  assumes g: "(g::'a::field poly) \<noteq> 0" and *: "pseudo_divmod f g = (q,r)"
  1.2614 +  defines "c \<equiv> coeff g (degree g) ^ (Suc (degree f) - degree g)"
  1.2615 +  shows "f = g * smult (1/c) q + smult (1/c) r"
  1.2616 +proof -
  1.2617 +  from leading_coeff_neq_0[OF g] have c0: "c \<noteq> 0" unfolding c_def by auto
  1.2618 +  from pseudo_divmod(1)[OF g *, folded c_def]
  1.2619 +  have "smult c f = g * q + r" by auto
  1.2620 +  also have "smult (1/c) ... = g * smult (1/c) q + smult (1/c) r" by (simp add: smult_add_right)
  1.2621 +  finally show ?thesis using c0 by auto
  1.2622 +qed
  1.2623 +
  1.2624 +lemma divide_poly_main_field:
  1.2625 +  assumes d: "(d::'a::field poly) \<noteq> 0"
  1.2626 +  defines lc: "lc \<equiv> coeff d (degree d)"
  1.2627 +  shows "divide_poly_main lc q r d dr n = fst (pseudo_divmod_main lc (smult ((1/lc)^n) q) (smult ((1/lc)^n) r) d dr n)"
  1.2628 +  unfolding lc
  1.2629 +  by(subst fst_pseudo_divmod_main_as_divide_poly_main, auto simp: d power_one_over)
  1.2630 +
  1.2631 +lemma divide_poly_field:
  1.2632 +  fixes f g :: "'a :: field poly"
  1.2633 +  defines "f' \<equiv> smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f"
  1.2634 +  shows "(f::'a::field poly) div g = fst (pseudo_divmod f' g)"
  1.2635 +proof (cases "g = 0")
  1.2636 +  case True show ?thesis 
  1.2637 +    unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True by (simp add: divide_poly_main_0)
  1.2638 +next
  1.2639 +  case False
  1.2640 +    from leading_coeff_neq_0[OF False] have "degree f' = degree f" unfolding f'_def by auto
  1.2641 +    then show ?thesis
  1.2642 +      using length_coeffs_degree[of f'] length_coeffs_degree[of f]
  1.2643 +      unfolding divide_poly_def pseudo_divmod_def Let_def
  1.2644 +                divide_poly_main_field[OF False]
  1.2645 +                length_coeffs_degree[OF False] 
  1.2646 +                f'_def
  1.2647 +      by force
  1.2648 +qed
  1.2649 +
  1.2650 +instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
  1.2651 +begin
  1.2652 +
  1.2653 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
  1.2654 +  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
  1.2655 +
  1.2656 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
  1.2657 +  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
  1.2658 +
  1.2659 +instance proof
  1.2660 +  fix p :: "'a poly"
  1.2661 +  show "unit_factor p * normalize p = p"
  1.2662 +    by (cases "p = 0")
  1.2663 +       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
  1.2664 +          smult_conv_map_poly map_poly_map_poly o_def)
  1.2665 +next
  1.2666 +  fix p :: "'a poly"
  1.2667 +  assume "is_unit p"
  1.2668 +  then obtain c where p: "p = [:c:]" "is_unit c"
  1.2669 +    by (auto simp: is_unit_poly_iff)
  1.2670 +  thus "normalize p = 1"
  1.2671 +    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
  1.2672 +next
  1.2673 +  fix p :: "'a poly" assume "p \<noteq> 0"
  1.2674 +  thus "is_unit (unit_factor p)"
  1.2675 +    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
  1.2676 +qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
  1.2677 +
  1.2678 +end
  1.2679 +
  1.2680 +lemma normalize_poly_eq_div:
  1.2681 +  "normalize p = p div [:unit_factor (lead_coeff p):]"
  1.2682  proof (cases "p = 0")
  1.2683    case False
  1.2684 +  thus ?thesis
  1.2685 +    by (subst div_const_poly_conv_map_poly)
  1.2686 +       (auto simp: normalize_poly_def const_poly_dvd_iff)
  1.2687 +qed (auto simp: normalize_poly_def)
  1.2688 +
  1.2689 +lemma unit_factor_pCons:
  1.2690 +  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
  1.2691 +  by (simp add: unit_factor_poly_def)
  1.2692 +
  1.2693 +lemma normalize_monom [simp]:
  1.2694 +  "normalize (monom a n) = monom (normalize a) n"
  1.2695 +  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
  1.2696 +
  1.2697 +lemma unit_factor_monom [simp]:
  1.2698 +  "unit_factor (monom a n) = monom (unit_factor a) 0"
  1.2699 +  by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
  1.2700 +
  1.2701 +lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
  1.2702 +  by (simp add: normalize_poly_def map_poly_pCons)
  1.2703 +
  1.2704 +lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
  1.2705 +proof -
  1.2706    have "smult c p = [:c:] * p" by simp
  1.2707 -  also from assms False have "order x \<dots> = order x [:c:] + order x p" 
  1.2708 -    by (subst order_mult) simp_all
  1.2709 -  also from assms have "order x [:c:] = 0" by (intro order_0I) auto
  1.2710 -  finally show ?thesis by simp
  1.2711 -qed simp
  1.2712 -
  1.2713 -(* Next two lemmas contributed by Wenda Li *)
  1.2714 -lemma order_1_eq_0 [simp]:"order x 1 = 0" 
  1.2715 -  by (metis order_root poly_1 zero_neq_one)
  1.2716 -
  1.2717 -lemma order_power_n_n: "order a ([:-a,1:]^n)=n" 
  1.2718 -proof (induct n) (*might be proved more concisely using nat_less_induct*)
  1.2719 -  case 0
  1.2720 -  thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
  1.2721 -next 
  1.2722 -  case (Suc n)
  1.2723 -  have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" 
  1.2724 -    by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral 
  1.2725 -      one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
  1.2726 -  moreover have "order a [:-a,1:]=1" unfolding order_def
  1.2727 -    proof (rule Least_equality,rule ccontr)
  1.2728 -      assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
  1.2729 -      hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
  1.2730 -      hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )" 
  1.2731 -        by (rule dvd_imp_degree_le,auto) 
  1.2732 -      thus False by auto
  1.2733 -    next
  1.2734 -      fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
  1.2735 -      show "1 \<le> y" 
  1.2736 -        proof (rule ccontr)
  1.2737 -          assume "\<not> 1 \<le> y"
  1.2738 -          hence "y=0" by auto
  1.2739 -          hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
  1.2740 -          thus False using asm by auto
  1.2741 -        qed
  1.2742 -    qed
  1.2743 -  ultimately show ?case using Suc by auto
  1.2744 +  also have "normalize \<dots> = smult (normalize c) (normalize p)"
  1.2745 +    by (subst normalize_mult) (simp add: normalize_const_poly)
  1.2746 +  finally show ?thesis .
  1.2747  qed
  1.2748  
  1.2749 -lemma order_0_monom [simp]:
  1.2750 -  assumes "c \<noteq> 0"
  1.2751 -  shows   "order 0 (monom c n) = n"
  1.2752 -  using assms order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
  1.2753 -
  1.2754 -lemma dvd_imp_order_le:
  1.2755 -  "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
  1.2756 -  by (auto simp: order_mult elim: dvdE)
  1.2757 -
  1.2758 -text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
  1.2759 -
  1.2760 -lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
  1.2761 -apply (cases "p = 0", auto)
  1.2762 -apply (drule order_2 [where a=a and p=p])
  1.2763 -apply (metis not_less_eq_eq power_le_dvd)
  1.2764 -apply (erule power_le_dvd [OF order_1])
  1.2765 -done
  1.2766 -
  1.2767 -lemma monom_1_dvd_iff:
  1.2768 -  assumes "p \<noteq> 0"
  1.2769 -  shows   "monom 1 n dvd p \<longleftrightarrow> n \<le> Polynomial.order 0 p"
  1.2770 -  using assms order_divides[of 0 n p] by (simp add: monom_altdef)
  1.2771 -
  1.2772 -lemma poly_squarefree_decomp_order:
  1.2773 -  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  1.2774 -  and p: "p = q * d"
  1.2775 -  and p': "pderiv p = e * d"
  1.2776 -  and d: "d = r * p + s * pderiv p"
  1.2777 -  shows "order a q = (if order a p = 0 then 0 else 1)"
  1.2778 -proof (rule classical)
  1.2779 -  assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)"
  1.2780 -  from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  1.2781 -  with p have "order a p = order a q + order a d"
  1.2782 -    by (simp add: order_mult)
  1.2783 -  with 1 have "order a p \<noteq> 0" by (auto split: if_splits)
  1.2784 -  have "order a (pderiv p) = order a e + order a d"
  1.2785 -    using \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> by (simp add: order_mult)
  1.2786 -  have "order a p = Suc (order a (pderiv p))"
  1.2787 -    using \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> by (rule order_pderiv)
  1.2788 -  have "d \<noteq> 0" using \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> by simp
  1.2789 -  have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
  1.2790 -    apply (simp add: d)
  1.2791 -    apply (rule dvd_add)
  1.2792 -    apply (rule dvd_mult)
  1.2793 -    apply (simp add: order_divides \<open>p \<noteq> 0\<close>
  1.2794 -           \<open>order a p = Suc (order a (pderiv p))\<close>)
  1.2795 -    apply (rule dvd_mult)
  1.2796 -    apply (simp add: order_divides)
  1.2797 -    done
  1.2798 -  then have "order a (pderiv p) \<le> order a d"
  1.2799 -    using \<open>d \<noteq> 0\<close> by (simp add: order_divides)
  1.2800 -  show ?thesis
  1.2801 -    using \<open>order a p = order a q + order a d\<close>
  1.2802 -    using \<open>order a (pderiv p) = order a e + order a d\<close>
  1.2803 -    using \<open>order a p = Suc (order a (pderiv p))\<close>
  1.2804 -    using \<open>order a (pderiv p) \<le> order a d\<close>
  1.2805 -    by auto
  1.2806 -qed
  1.2807 -
  1.2808 -lemma poly_squarefree_decomp_order2: 
  1.2809 -     "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
  1.2810 -       p = q * d;
  1.2811 -       pderiv p = e * d;
  1.2812 -       d = r * p + s * pderiv p
  1.2813 -      \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  1.2814 -by (blast intro: poly_squarefree_decomp_order)
  1.2815 -
  1.2816 -lemma order_pderiv2: 
  1.2817 -  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
  1.2818 -      \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
  1.2819 -by (auto dest: order_pderiv)
  1.2820 -
  1.2821 -definition
  1.2822 -  rsquarefree :: "'a::idom poly => bool" where
  1.2823 -  "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
  1.2824 -
  1.2825 -lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
  1.2826 -  by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
  1.2827 -
  1.2828 -lemma rsquarefree_roots:
  1.2829 -  fixes p :: "'a :: field_char_0 poly"
  1.2830 -  shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
  1.2831 -apply (simp add: rsquarefree_def)
  1.2832 -apply (case_tac "p = 0", simp, simp)
  1.2833 -apply (case_tac "pderiv p = 0")
  1.2834 -apply simp
  1.2835 -apply (drule pderiv_iszero, clarsimp)
  1.2836 -apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
  1.2837 -apply (force simp add: order_root order_pderiv2)
  1.2838 -done
  1.2839 -
  1.2840 -lemma poly_squarefree_decomp:
  1.2841 -  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  1.2842 -    and "p = q * d"
  1.2843 -    and "pderiv p = e * d"
  1.2844 -    and "d = r * p + s * pderiv p"
  1.2845 -  shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
  1.2846 +lemma smult_content_normalize_primitive_part [simp]:
  1.2847 +  "smult (content p) (normalize (primitive_part p)) = normalize p"
  1.2848  proof -
  1.2849 -  from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  1.2850 -  with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
  1.2851 -  have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  1.2852 -    using assms by (rule poly_squarefree_decomp_order2)
  1.2853 -  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
  1.2854 -    by (simp add: rsquarefree_def order_root)
  1.2855 -qed
  1.2856 -
  1.2857 -lemma coeff_monom_mult: 
  1.2858 -  "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
  1.2859 -proof -
  1.2860 -  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
  1.2861 -    by (simp add: coeff_mult)
  1.2862 -  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
  1.2863 -    by (intro sum.cong) simp_all
  1.2864 -  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))" by (simp add: sum.delta')
  1.2865 +  have "smult (content p) (normalize (primitive_part p)) = 
  1.2866 +          normalize ([:content p:] * primitive_part p)" 
  1.2867 +    by (subst normalize_mult) (simp_all add: normalize_const_poly)
  1.2868 +  also have "[:content p:] * primitive_part p = p" by simp
  1.2869    finally show ?thesis .
  1.2870  qed
  1.2871  
  1.2872 -lemma monom_1_dvd_iff':
  1.2873 -  "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
  1.2874 +inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
  1.2875 +  where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
  1.2876 +  | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
  1.2877 +  | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
  1.2878 +      \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
  1.2879 +  
  1.2880 +lemma eucl_rel_poly_iff:
  1.2881 +  "eucl_rel_poly x y (q, r) \<longleftrightarrow>
  1.2882 +    x = q * y + r \<and>
  1.2883 +      (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
  1.2884 +  by (auto elim: eucl_rel_poly.cases
  1.2885 +    intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
  1.2886 +  
  1.2887 +lemma eucl_rel_poly_0:
  1.2888 +  "eucl_rel_poly 0 y (0, 0)"
  1.2889 +  unfolding eucl_rel_poly_iff by simp
  1.2890 +
  1.2891 +lemma eucl_rel_poly_by_0:
  1.2892 +  "eucl_rel_poly x 0 (0, x)"
  1.2893 +  unfolding eucl_rel_poly_iff by simp
  1.2894 +
  1.2895 +lemma eucl_rel_poly_pCons:
  1.2896 +  assumes rel: "eucl_rel_poly x y (q, r)"
  1.2897 +  assumes y: "y \<noteq> 0"
  1.2898 +  assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
  1.2899 +  shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
  1.2900 +    (is "eucl_rel_poly ?x y (?q, ?r)")
  1.2901 +proof -
  1.2902 +  have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
  1.2903 +    using assms unfolding eucl_rel_poly_iff by simp_all
  1.2904 +
  1.2905 +  have 1: "?x = ?q * y + ?r"
  1.2906 +    using b x by simp
  1.2907 +
  1.2908 +  have 2: "?r = 0 \<or> degree ?r < degree y"
  1.2909 +  proof (rule eq_zero_or_degree_less)
  1.2910 +    show "degree ?r \<le> degree y"
  1.2911 +    proof (rule degree_diff_le)
  1.2912 +      show "degree (pCons a r) \<le> degree y"
  1.2913 +        using r by auto
  1.2914 +      show "degree (smult b y) \<le> degree y"
  1.2915 +        by (rule degree_smult_le)
  1.2916 +    qed
  1.2917 +  next
  1.2918 +    show "coeff ?r (degree y) = 0"
  1.2919 +      using \<open>y \<noteq> 0\<close> unfolding b by simp
  1.2920 +  qed
  1.2921 +
  1.2922 +  from 1 2 show ?thesis
  1.2923 +    unfolding eucl_rel_poly_iff
  1.2924 +    using \<open>y \<noteq> 0\<close> by simp
  1.2925 +qed
  1.2926 +
  1.2927 +lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
  1.2928 +apply (cases "y = 0")
  1.2929 +apply (fast intro!: eucl_rel_poly_by_0)
  1.2930 +apply (induct x)
  1.2931 +apply (fast intro!: eucl_rel_poly_0)
  1.2932 +apply (fast intro!: eucl_rel_poly_pCons)
  1.2933 +done
  1.2934 +
  1.2935 +lemma eucl_rel_poly_unique:
  1.2936 +  assumes 1: "eucl_rel_poly x y (q1, r1)"
  1.2937 +  assumes 2: "eucl_rel_poly x y (q2, r2)"
  1.2938 +  shows "q1 = q2 \<and> r1 = r2"
  1.2939 +proof (cases "y = 0")
  1.2940 +  assume "y = 0" with assms show ?thesis
  1.2941 +    by (simp add: eucl_rel_poly_iff)
  1.2942 +next
  1.2943 +  assume [simp]: "y \<noteq> 0"
  1.2944 +  from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
  1.2945 +    unfolding eucl_rel_poly_iff by simp_all
  1.2946 +  from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
  1.2947 +    unfolding eucl_rel_poly_iff by simp_all
  1.2948 +  from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
  1.2949 +    by (simp add: algebra_simps)
  1.2950 +  from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
  1.2951 +    by (auto intro: degree_diff_less)
  1.2952 +
  1.2953 +  show "q1 = q2 \<and> r1 = r2"
  1.2954 +  proof (rule ccontr)
  1.2955 +    assume "\<not> (q1 = q2 \<and> r1 = r2)"
  1.2956 +    with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
  1.2957 +    with r3 have "degree (r2 - r1) < degree y" by simp
  1.2958 +    also have "degree y \<le> degree (q1 - q2) + degree y" by simp
  1.2959 +    also have "\<dots> = degree ((q1 - q2) * y)"
  1.2960 +      using \<open>q1 \<noteq> q2\<close> by (simp add: degree_mult_eq)
  1.2961 +    also have "\<dots> = degree (r2 - r1)"
  1.2962 +      using q3 by simp
  1.2963 +    finally have "degree (r2 - r1) < degree (r2 - r1)" .
  1.2964 +    then show "False" by simp
  1.2965 +  qed
  1.2966 +qed
  1.2967 +
  1.2968 +lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
  1.2969 +by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
  1.2970 +
  1.2971 +lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
  1.2972 +by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
  1.2973 +
  1.2974 +lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
  1.2975 +
  1.2976 +lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
  1.2977 +
  1.2978 +instantiation poly :: (field) ring_div
  1.2979 +begin
  1.2980 +
  1.2981 +definition modulo_poly where
  1.2982 +  mod_poly_def: "f mod g \<equiv>
  1.2983 +    if g = 0 then f
  1.2984 +    else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
  1.2985 +
  1.2986 +lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
  1.2987 +  unfolding eucl_rel_poly_iff
  1.2988 +proof (intro conjI)
  1.2989 +  show "x = x div y * y + x mod y"
  1.2990 +  proof(cases "y = 0")
  1.2991 +    case True show ?thesis by(simp add: True divide_poly_def divide_poly_0 mod_poly_def)
  1.2992 +  next
  1.2993 +    case False
  1.2994 +    then have "pseudo_divmod (smult ((1 / coeff y (degree y)) ^ (Suc (degree x) - degree y)) x) y =
  1.2995 +          (x div y, x mod y)"
  1.2996 +      unfolding divide_poly_field mod_poly_def pseudo_mod_def by simp
  1.2997 +    from pseudo_divmod[OF False this]
  1.2998 +    show ?thesis using False
  1.2999 +      by (simp add: power_mult_distrib[symmetric] mult.commute)
  1.3000 +  qed
  1.3001 +  show "if y = 0 then x div y = 0 else x mod y = 0 \<or> degree (x mod y) < degree y"
  1.3002 +  proof (cases "y = 0")
  1.3003 +    case True then show ?thesis by auto
  1.3004 +  next
  1.3005 +    case False
  1.3006 +      with pseudo_mod[OF this] show ?thesis unfolding mod_poly_def by simp
  1.3007 +  qed
  1.3008 +qed
  1.3009 +
  1.3010 +lemma div_poly_eq:
  1.3011 +  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
  1.3012 +  by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
  1.3013 +
  1.3014 +lemma mod_poly_eq:
  1.3015 +  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
  1.3016 +  by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
  1.3017 +
  1.3018 +instance
  1.3019  proof
  1.3020 -  assume "monom 1 n dvd p"
  1.3021 -  then obtain r where r: "p = monom 1 n * r" by (elim dvdE)
  1.3022 -  thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult)
  1.3023 +  fix x y :: "'a poly"
  1.3024 +  from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
  1.3025 +  show "x div y * y + x mod y = x" by auto
  1.3026 +next
  1.3027 +  fix x y z :: "'a poly"
  1.3028 +  assume "y \<noteq> 0"
  1.3029 +  hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
  1.3030 +    using eucl_rel_poly [of x y]
  1.3031 +    by (simp add: eucl_rel_poly_iff distrib_right)
  1.3032 +  thus "(x + z * y) div y = z + x div y"
  1.3033 +    by (rule div_poly_eq)
  1.3034  next
  1.3035 -  assume zero: "(\<forall>k<n. coeff p k = 0)"
  1.3036 -  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
  1.3037 -  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
  1.3038 -    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 
  1.3039 -        subst cofinite_eq_sequentially [symmetric]) transfer
  1.3040 -  hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def
  1.3041 -    by (subst poly.Abs_poly_inverse) simp_all
  1.3042 -  have "p = monom 1 n * r"
  1.3043 -    by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all)
  1.3044 -  thus "monom 1 n dvd p" by simp
  1.3045 +  fix x y z :: "'a poly"
  1.3046 +  assume "x \<noteq> 0"
  1.3047 +  show "(x * y) div (x * z) = y div z"
  1.3048 +  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
  1.3049 +    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
  1.3050 +      by (rule eucl_rel_poly_by_0)
  1.3051 +    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
  1.3052 +      by (rule div_poly_eq)
  1.3053 +    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
  1.3054 +      by (rule eucl_rel_poly_0)
  1.3055 +    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
  1.3056 +      by (rule div_poly_eq)
  1.3057 +    case False then show ?thesis by auto
  1.3058 +  next
  1.3059 +    case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
  1.3060 +    with \<open>x \<noteq> 0\<close>
  1.3061 +    have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
  1.3062 +      by (auto simp add: eucl_rel_poly_iff algebra_simps)
  1.3063 +        (rule classical, simp add: degree_mult_eq)
  1.3064 +    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
  1.3065 +    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
  1.3066 +    then show ?thesis by (simp add: div_poly_eq)
  1.3067 +  qed
  1.3068 +qed
  1.3069 +
  1.3070 +end
  1.3071 +
  1.3072 +lemma degree_mod_less:
  1.3073 +  "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
  1.3074 +  using eucl_rel_poly [of x y]
  1.3075 +  unfolding eucl_rel_poly_iff by simp
  1.3076 +
  1.3077 +lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
  1.3078 +  using degree_mod_less[of b a] by auto
  1.3079 +
  1.3080 +lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
  1.3081 +proof -
  1.3082 +  assume "degree x < degree y"
  1.3083 +  hence "eucl_rel_poly x y (0, x)"
  1.3084 +    by (simp add: eucl_rel_poly_iff)
  1.3085 +  thus "x div y = 0" by (rule div_poly_eq)
  1.3086 +qed
  1.3087 +
  1.3088 +lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
  1.3089 +proof -
  1.3090 +  assume "degree x < degree y"
  1.3091 +  hence "eucl_rel_poly x y (0, x)"
  1.3092 +    by (simp add: eucl_rel_poly_iff)
  1.3093 +  thus "x mod y = x" by (rule mod_poly_eq)
  1.3094 +qed
  1.3095 +
  1.3096 +lemma eucl_rel_poly_smult_left:
  1.3097 +  "eucl_rel_poly x y (q, r)
  1.3098 +    \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
  1.3099 +  unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
  1.3100 +
  1.3101 +lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
  1.3102 +  by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  1.3103 +
  1.3104 +lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  1.3105 +  by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  1.3106 +
  1.3107 +lemma poly_div_minus_left [simp]:
  1.3108 +  fixes x y :: "'a::field poly"
  1.3109 +  shows "(- x) div y = - (x div y)"
  1.3110 +  using div_smult_left [of "- 1::'a"] by simp
  1.3111 +
  1.3112 +lemma poly_mod_minus_left [simp]:
  1.3113 +  fixes x y :: "'a::field poly"
  1.3114 +  shows "(- x) mod y = - (x mod y)"
  1.3115 +  using mod_smult_left [of "- 1::'a"] by simp
  1.3116 +
  1.3117 +lemma eucl_rel_poly_add_left:
  1.3118 +  assumes "eucl_rel_poly x y (q, r)"
  1.3119 +  assumes "eucl_rel_poly x' y (q', r')"
  1.3120 +  shows "eucl_rel_poly (x + x') y (q + q', r + r')"
  1.3121 +  using assms unfolding eucl_rel_poly_iff
  1.3122 +  by (auto simp add: algebra_simps degree_add_less)
  1.3123 +
  1.3124 +lemma poly_div_add_left:
  1.3125 +  fixes x y z :: "'a::field poly"
  1.3126 +  shows "(x + y) div z = x div z + y div z"
  1.3127 +  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  1.3128 +  by (rule div_poly_eq)
  1.3129 +
  1.3130 +lemma poly_mod_add_left:
  1.3131 +  fixes x y z :: "'a::field poly"
  1.3132 +  shows "(x + y) mod z = x mod z + y mod z"
  1.3133 +  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  1.3134 +  by (rule mod_poly_eq)
  1.3135 +
  1.3136 +lemma poly_div_diff_left:
  1.3137 +  fixes x y z :: "'a::field poly"
  1.3138 +  shows "(x - y) div z = x div z - y div z"
  1.3139 +  by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
  1.3140 +
  1.3141 +lemma poly_mod_diff_left:
  1.3142 +  fixes x y z :: "'a::field poly"
  1.3143 +  shows "(x - y) mod z = x mod z - y mod z"
  1.3144 +  by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
  1.3145 +
  1.3146 +lemma eucl_rel_poly_smult_right:
  1.3147 +  "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
  1.3148 +    \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
  1.3149 +  unfolding eucl_rel_poly_iff by simp
  1.3150 +
  1.3151 +lemma div_smult_right:
  1.3152 +  "(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  1.3153 +  by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  1.3154 +
  1.3155 +lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  1.3156 +  by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  1.3157 +
  1.3158 +lemma poly_div_minus_right [simp]:
  1.3159 +  fixes x y :: "'a::field poly"
  1.3160 +  shows "x div (- y) = - (x div y)"
  1.3161 +  using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
  1.3162 +
  1.3163 +lemma poly_mod_minus_right [simp]:
  1.3164 +  fixes x y :: "'a::field poly"
  1.3165 +  shows "x mod (- y) = x mod y"
  1.3166 +  using mod_smult_right [of "- 1::'a"] by simp
  1.3167 +
  1.3168 +lemma eucl_rel_poly_mult:
  1.3169 +  "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
  1.3170 +    \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
  1.3171 +apply (cases "z = 0", simp add: eucl_rel_poly_iff)
  1.3172 +apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
  1.3173 +apply (cases "r = 0")
  1.3174 +apply (cases "r' = 0")
  1.3175 +apply (simp add: eucl_rel_poly_iff)
  1.3176 +apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
  1.3177 +apply (cases "r' = 0")
  1.3178 +apply (simp add: eucl_rel_poly_iff degree_mult_eq)
  1.3179 +apply (simp add: eucl_rel_poly_iff field_simps)
  1.3180 +apply (simp add: degree_mult_eq degree_add_less)
  1.3181 +done
  1.3182 +
  1.3183 +lemma poly_div_mult_right:
  1.3184 +  fixes x y z :: "'a::field poly"
  1.3185 +  shows "x div (y * z) = (x div y) div z"
  1.3186 +  by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  1.3187 +
  1.3188 +lemma poly_mod_mult_right:
  1.3189 +  fixes x y z :: "'a::field poly"
  1.3190 +  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
  1.3191 +  by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  1.3192 +
  1.3193 +lemma mod_pCons:
  1.3194 +  fixes a and x
  1.3195 +  assumes y: "y \<noteq> 0"
  1.3196 +  defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  1.3197 +  shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
  1.3198 +unfolding b
  1.3199 +apply (rule mod_poly_eq)
  1.3200 +apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
  1.3201 +done
  1.3202 +
  1.3203 +definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  1.3204 +where
  1.3205 +  "pdivmod p q = (p div q, p mod q)"
  1.3206 +
  1.3207 +lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)"
  1.3208 +  by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique)
  1.3209 +
  1.3210 +lemma pdivmod_0:
  1.3211 +  "pdivmod 0 q = (0, 0)"
  1.3212 +  by (simp add: pdivmod_def)
  1.3213 +
  1.3214 +lemma pdivmod_pCons:
  1.3215 +  "pdivmod (pCons a p) q =
  1.3216 +    (if q = 0 then (0, pCons a p) else
  1.3217 +      (let (s, r) = pdivmod p q;
  1.3218 +           b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1.3219 +        in (pCons b s, pCons a r - smult b q)))"
  1.3220 +  apply (simp add: pdivmod_def Let_def, safe)
  1.3221 +  apply (rule div_poly_eq)
  1.3222 +  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
  1.3223 +  apply (rule mod_poly_eq)
  1.3224 +  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
  1.3225 +  done
  1.3226 +
  1.3227 +lemma pdivmod_fold_coeffs:
  1.3228 +  "pdivmod p q = (if q = 0 then (0, p)
  1.3229 +    else fold_coeffs (\<lambda>a (s, r).
  1.3230 +      let b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1.3231 +      in (pCons b s, pCons a r - smult b q)
  1.3232 +   ) p (0, 0))"
  1.3233 +  apply (cases "q = 0")
  1.3234 +  apply (simp add: pdivmod_def)
  1.3235 +  apply (rule sym)
  1.3236 +  apply (induct p)
  1.3237 +  apply (simp_all add: pdivmod_0 pdivmod_pCons)
  1.3238 +  apply (case_tac "a = 0 \<and> p = 0")
  1.3239 +  apply (auto simp add: pdivmod_def)
  1.3240 +  done
  1.3241 +
  1.3242 +    
  1.3243 +subsubsection \<open>List-based versions for fast implementation\<close>
  1.3244 +(* Subsection by:
  1.3245 +      Sebastiaan Joosten
  1.3246 +      René Thiemann
  1.3247 +      Akihisa Yamada
  1.3248 +    *)
  1.3249 +fun minus_poly_rev_list :: "'a :: group_add list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  1.3250 +  "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
  1.3251 +| "minus_poly_rev_list xs [] = xs"
  1.3252 +| "minus_poly_rev_list [] (y # ys) = []"
  1.3253 +
  1.3254 +fun pseudo_divmod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.3255 +  \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
  1.3256 +  "pseudo_divmod_main_list lc q r d (Suc n) = (let
  1.3257 +     rr = map (op * lc) r;
  1.3258 +     a = hd r;
  1.3259 +     qqq = cCons a (map (op * lc) q);
  1.3260 +     rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  1.3261 +     in pseudo_divmod_main_list lc qqq rrr d n)"
  1.3262 +| "pseudo_divmod_main_list lc q r d 0 = (q,r)"
  1.3263 +
  1.3264 +fun pseudo_mod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.3265 +  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.3266 +  "pseudo_mod_main_list lc r d (Suc n) = (let
  1.3267 +     rr = map (op * lc) r;
  1.3268 +     a = hd r;
  1.3269 +     rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  1.3270 +     in pseudo_mod_main_list lc rrr d n)"
  1.3271 +| "pseudo_mod_main_list lc r d 0 = r"
  1.3272 +
  1.3273 +
  1.3274 +fun divmod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.3275 +  \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
  1.3276 +  "divmod_poly_one_main_list q r d (Suc n) = (let
  1.3277 +     a = hd r;
  1.3278 +     qqq = cCons a q;
  1.3279 +     rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  1.3280 +     in divmod_poly_one_main_list qqq rr d n)"
  1.3281 +| "divmod_poly_one_main_list q r d 0 = (q,r)"
  1.3282 +
  1.3283 +fun mod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list 
  1.3284 +  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.3285 +  "mod_poly_one_main_list r d (Suc n) = (let
  1.3286 +     a = hd r;
  1.3287 +     rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  1.3288 +     in mod_poly_one_main_list rr d n)"
  1.3289 +| "mod_poly_one_main_list r d 0 = r"
  1.3290 +
  1.3291 +definition pseudo_divmod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list" where
  1.3292 +  "pseudo_divmod_list p q =
  1.3293 +  (if q = [] then ([],p) else
  1.3294 + (let rq = rev q;
  1.3295 +     (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in 
  1.3296 +   (qu,rev re)))"
  1.3297 +
  1.3298 +definition pseudo_mod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  1.3299 +  "pseudo_mod_list p q =
  1.3300 +  (if q = [] then p else
  1.3301 + (let rq = rev q;
  1.3302 +     re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in 
  1.3303 +   (rev re)))"
  1.3304 +
  1.3305 +lemma minus_zero_does_nothing:
  1.3306 +"(minus_poly_rev_list x (map (op * 0) y)) = (x :: 'a :: ring list)"
  1.3307 +  by(induct x y rule: minus_poly_rev_list.induct, auto)
  1.3308 +
  1.3309 +lemma length_minus_poly_rev_list[simp]:
  1.3310 + "length (minus_poly_rev_list xs ys) = length xs"
  1.3311 +  by(induct xs ys rule: minus_poly_rev_list.induct, auto)
  1.3312 +
  1.3313 +lemma if_0_minus_poly_rev_list:
  1.3314 +  "(if a = 0 then x else minus_poly_rev_list x (map (op * a) y))
  1.3315 +      = minus_poly_rev_list x (map (op * (a :: 'a :: ring)) y)"
  1.3316 +  by(cases "a=0",simp_all add:minus_zero_does_nothing)
  1.3317 +
  1.3318 +lemma Poly_append:
  1.3319 +  "Poly ((a::'a::comm_semiring_1 list) @ b) = Poly a + monom 1 (length a) * Poly b"
  1.3320 +  by (induct a,auto simp: monom_0 monom_Suc)
  1.3321 +
  1.3322 +lemma minus_poly_rev_list: "length p \<ge> length (q :: 'a :: comm_ring_1 list) \<Longrightarrow>
  1.3323 +  Poly (rev (minus_poly_rev_list (rev p) (rev q)))
  1.3324 +  = Poly p - monom 1 (length p - length q) * Poly q"
  1.3325 +proof (induct "rev p" "rev q" arbitrary: p q rule: minus_poly_rev_list.induct)
  1.3326 +  case (1 x xs y ys) 
  1.3327 +  have "length (rev q) \<le> length (rev p)" using 1 by simp
  1.3328 +  from this[folded 1(2,3)] have ys_xs:"length ys \<le> length xs" by simp
  1.3329 +  hence a:"Poly (rev (minus_poly_rev_list xs ys)) =
  1.3330 +           Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)"
  1.3331 +    by(subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev],auto)
  1.3332 +  have "Poly p - monom 1 (length p - length q) * Poly q
  1.3333 +      = Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))"
  1.3334 +    by simp
  1.3335 +  also have "\<dots> = Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))"
  1.3336 +    unfolding 1(2,3) by simp
  1.3337 +  also have "\<dots> = Poly (rev xs) + monom x (length xs) -
  1.3338 +  (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))" using ys_xs
  1.3339 +    by (simp add:Poly_append distrib_left mult_monom smult_monom)
  1.3340 +  also have "\<dots> = Poly (rev (minus_poly_rev_list xs ys)) + monom (x - y) (length xs)"
  1.3341 +    unfolding a diff_monom[symmetric] by(simp)
  1.3342 +  finally show ?case
  1.3343 +    unfolding 1(2,3)[symmetric] by (simp add: smult_monom Poly_append)
  1.3344 +qed auto
  1.3345 +
  1.3346 +lemma smult_monom_mult: "smult a (monom b n * f) = monom (a * b) n * f"
  1.3347 +  using smult_monom [of a _ n] by (metis mult_smult_left)
  1.3348 +
  1.3349 +lemma head_minus_poly_rev_list:
  1.3350 +  "length d \<le> length r \<Longrightarrow> d\<noteq>[] \<Longrightarrow>
  1.3351 +  hd (minus_poly_rev_list (map (op * (last d :: 'a :: comm_ring)) r) (map (op * (hd r)) (rev d))) = 0"
  1.3352 +proof(induct r)
  1.3353 +  case (Cons a rs)
  1.3354 +  thus ?case by(cases "rev d", simp_all add:ac_simps)
  1.3355 +qed simp
  1.3356 +
  1.3357 +lemma Poly_map: "Poly (map (op * a) p) = smult a (Poly p)"
  1.3358 +proof (induct p)
  1.3359 +  case(Cons x xs) thus ?case by (cases "Poly xs = 0",auto)
  1.3360 +qed simp
  1.3361 +
  1.3362 +lemma last_coeff_is_hd: "xs \<noteq> [] \<Longrightarrow> coeff (Poly xs) (length xs - 1) = hd (rev xs)"
  1.3363 +  by (simp_all add: hd_conv_nth rev_nth nth_default_nth nth_append)
  1.3364 +
  1.3365 +lemma pseudo_divmod_main_list_invar :
  1.3366 +  assumes leading_nonzero:"last d \<noteq> 0"
  1.3367 +  and lc:"last d = lc"
  1.3368 +  and dNonempty:"d \<noteq> []"
  1.3369 +  and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q',rev r')"
  1.3370 +  and "n = (1 + length r - length d)"
  1.3371 +  shows 
  1.3372 +  "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n = 
  1.3373 +  (Poly q', Poly r')"
  1.3374 +using assms(4-)
  1.3375 +proof(induct "n" arbitrary: r q)
  1.3376 +case (Suc n r q)
  1.3377 +  have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
  1.3378 +  have rNonempty:"r \<noteq> []"
  1.3379 +    using ifCond dNonempty using Suc_leI length_greater_0_conv list.size(3) by fastforce
  1.3380 +  let ?a = "(hd (rev r))"
  1.3381 +  let ?rr = "map (op * lc) (rev r)"
  1.3382 +  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (op * ?a) (rev d))))"
  1.3383 +  let ?qq = "cCons ?a (map (op * lc) q)"
  1.3384 +  have n: "n = (1 + length r - length d - 1)"
  1.3385 +    using ifCond Suc(3) by simp
  1.3386 +  have rr_val:"(length ?rrr) = (length r - 1)" using ifCond by auto
  1.3387 +  hence rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)"
  1.3388 +    using rNonempty ifCond unfolding One_nat_def by auto
  1.3389 +  from ifCond have id: "Suc (length r) - length d = Suc (length r - length d)" by auto
  1.3390 +  have "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')"
  1.3391 +    using Suc.prems ifCond by (simp add:Let_def if_0_minus_poly_rev_list id)
  1.3392 +  hence v:"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')"
  1.3393 +    using n by auto
  1.3394 +  have sucrr:"Suc (length r) - length d = Suc (length r - length d)"
  1.3395 +    using Suc_diff_le ifCond not_less_eq_eq by blast
  1.3396 +  have n_ok : "n = 1 + (length ?rrr) - length d" using Suc(3) rNonempty by simp
  1.3397 +  have cong: "\<And> x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  1.3398 +    pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n" by simp
  1.3399 +  have hd_rev:"coeff (Poly r) (length r - Suc 0) = hd (rev r)"
  1.3400 +    using last_coeff_is_hd[OF rNonempty] by simp
  1.3401 +  show ?case unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def
  1.3402 +  proof (rule cong[OF _ _ refl], goal_cases)
  1.3403 +    case 1 
  1.3404 +    show ?case unfolding monom_Suc hd_rev[symmetric]
  1.3405 +      by (simp add: smult_monom Poly_map)
  1.3406 +  next
  1.3407 +    case 2 
  1.3408 +    show ?case 
  1.3409 +    proof (subst Poly_on_rev_starting_with_0, goal_cases)
  1.3410 +      show "hd (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))) = 0"
  1.3411 +        by (fold lc, subst head_minus_poly_rev_list, insert ifCond dNonempty,auto)
  1.3412 +      from ifCond have "length d \<le> length r" by simp
  1.3413 +      then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
  1.3414 +        Poly (rev (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))))"
  1.3415 +        by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
  1.3416 +          minus_poly_rev_list)
  1.3417 +    qed
  1.3418 +  qed simp
  1.3419 +qed simp
  1.3420 +
  1.3421 +lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g =
  1.3422 +  map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
  1.3423 +proof (cases "g=0")
  1.3424 +case False
  1.3425 +  hence coeffs_g_nonempty:"(coeffs g) \<noteq> []" by simp
  1.3426 +  hence lastcoeffs:"last (coeffs g) = coeff g (degree g)"
  1.3427 +    by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil)
  1.3428 +  obtain q r where qr: "pseudo_divmod_main_list
  1.3429 +            (last (coeffs g)) (rev [])
  1.3430 +            (rev (coeffs f)) (rev (coeffs g))
  1.3431 +            (1 + length (coeffs f) -
  1.3432 +             length (coeffs g)) = (q,rev (rev r))"  by force
  1.3433 +  then have qr': "pseudo_divmod_main_list
  1.3434 +            (hd (rev (coeffs g))) []
  1.3435 +            (rev (coeffs f)) (rev (coeffs g))
  1.3436 +            (1 + length (coeffs f) -
  1.3437 +             length (coeffs g)) = (q,r)" using hd_rev[OF coeffs_g_nonempty] by(auto)
  1.3438 +  from False have cg: "(coeffs g = []) = False" by auto
  1.3439 +  have last_non0:"last (coeffs g) \<noteq> 0" using False by (simp add:last_coeffs_not_0)
  1.3440 +  show ?thesis
  1.3441 +    unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False
  1.3442 +    pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False]
  1.3443 +    poly_of_list_def
  1.3444 +    using False by (auto simp: degree_eq_length_coeffs)
  1.3445 +next
  1.3446 +  case True
  1.3447 +  show ?thesis unfolding True unfolding pseudo_divmod_def pseudo_divmod_list_def
  1.3448 +  by auto
  1.3449 +qed
  1.3450 +
  1.3451 +lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q 
  1.3452 +  xs ys n) = pseudo_mod_main_list l xs ys n"
  1.3453 +  by (induct n arbitrary: l q xs ys, auto simp: Let_def)
  1.3454 +
  1.3455 +lemma pseudo_mod_impl[code]: "pseudo_mod f g =
  1.3456 +  poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))"
  1.3457 +proof -
  1.3458 +  have snd_case: "\<And> f g p. snd ((\<lambda> (x,y). (f x, g y)) p) = g (snd p)" 
  1.3459 +    by auto
  1.3460 +  show ?thesis
  1.3461 +  unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
  1.3462 +    pseudo_mod_list_def Let_def
  1.3463 +  by (simp add: snd_case pseudo_mod_main_list)
  1.3464 +qed
  1.3465 +
  1.3466 +
  1.3467 +(* *************** *)
  1.3468 +subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
  1.3469 +
  1.3470 +lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f) 
  1.3471 +     else let 
  1.3472 +       ilc = inverse (coeff g (degree g));       
  1.3473 +       h = smult ilc g;
  1.3474 +       (q,r) = pseudo_divmod f h
  1.3475 +     in (smult ilc q, r))" (is "?l = ?r")
  1.3476 +proof (cases "g = 0")
  1.3477 +  case False
  1.3478 +  define lc where "lc = inverse (coeff g (degree g))"
  1.3479 +  define h where "h = smult lc g"
  1.3480 +  from False have h1: "coeff h (degree h) = 1" and lc: "lc \<noteq> 0" unfolding h_def lc_def by auto
  1.3481 +  hence h0: "h \<noteq> 0" by auto
  1.3482 +  obtain q r where p: "pseudo_divmod f h = (q,r)" by force
  1.3483 +  from False have id: "?r = (smult lc q, r)" 
  1.3484 +    unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
  1.3485 +  from pseudo_divmod[OF h0 p, unfolded h1] 
  1.3486 +  have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
  1.3487 +  have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
  1.3488 +  hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel)
  1.3489 +  hence "pdivmod f g = (smult lc q, r)" 
  1.3490 +    unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc]
  1.3491 +    using lc by auto
  1.3492 +  with id show ?thesis by auto
  1.3493 +qed (auto simp: pdivmod_def)
  1.3494 +
  1.3495 +lemma pdivmod_via_pseudo_divmod_list: "pdivmod f g = (let 
  1.3496 +  cg = coeffs g
  1.3497 +  in if cg = [] then (0,f)
  1.3498 +     else let 
  1.3499 +       cf = coeffs f;
  1.3500 +       ilc = inverse (last cg);       
  1.3501 +       ch = map (op * ilc) cg;
  1.3502 +       (q,r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
  1.3503 +     in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))"
  1.3504 +proof -
  1.3505 +  note d = pdivmod_via_pseudo_divmod
  1.3506 +      pseudo_divmod_impl pseudo_divmod_list_def
  1.3507 +  show ?thesis
  1.3508 +  proof (cases "g = 0")
  1.3509 +    case True thus ?thesis unfolding d by auto
  1.3510 +  next
  1.3511 +    case False
  1.3512 +    define ilc where "ilc = inverse (coeff g (degree g))"
  1.3513 +    from False have ilc: "ilc \<noteq> 0" unfolding ilc_def by auto
  1.3514 +    with False have id: "(g = 0) = False" "(coeffs g = []) = False" 
  1.3515 +      "last (coeffs g) = coeff g (degree g)" 
  1.3516 +      "(coeffs (smult ilc g) = []) = False"
  1.3517 +      by (auto simp: last_coeffs_eq_coeff_degree) 
  1.3518 +    have id2: "hd (rev (coeffs (smult ilc g))) = 1"      
  1.3519 +      by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
  1.3520 +    have id3: "length (coeffs (smult ilc g)) = length (coeffs g)" 
  1.3521 +      "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))" unfolding coeffs_smult using ilc by auto
  1.3522 +    obtain q r where pair: "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g)))
  1.3523 +           (1 + length (coeffs f) - length (coeffs g)) = (q,r)" by force
  1.3524 +    show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2 
  1.3525 +      unfolding id3 pair map_prod_def split by (auto simp: Poly_map)
  1.3526 +  qed
  1.3527 +qed
  1.3528 +
  1.3529 +lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
  1.3530 +proof (intro ext, goal_cases)
  1.3531 +  case (1 q r d n)
  1.3532 +  {
  1.3533 +    fix xs :: "'a list"
  1.3534 +    have "map (op * 1) xs = xs" by (induct xs, auto)
  1.3535 +  } note [simp] = this
  1.3536 +  show ?case by (induct n arbitrary: q r d, auto simp: Let_def)
  1.3537 +qed
  1.3538 +
  1.3539 +fun divide_poly_main_list :: "'a::idom_divide \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list 
  1.3540 +  \<Rightarrow> nat \<Rightarrow> 'a list" where
  1.3541 +  "divide_poly_main_list lc q r d (Suc n) = (let
  1.3542 +     cr = hd r
  1.3543 +     in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let 
  1.3544 +     a = cr div lc;
  1.3545 +     qq = cCons a q;
  1.3546 +     rr = minus_poly_rev_list r (map (op * a) d)
  1.3547 +     in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  1.3548 +| "divide_poly_main_list lc q r d 0 = q"
  1.3549 +
  1.3550 +
  1.3551 +lemma divide_poly_main_list_simp[simp]: "divide_poly_main_list lc q r d (Suc n) = (let
  1.3552 +     cr = hd r;
  1.3553 +     a = cr div lc;
  1.3554 +     qq = cCons a q;
  1.3555 +     rr = minus_poly_rev_list r (map (op * a) d)
  1.3556 +     in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  1.3557 +  by (simp add: Let_def minus_zero_does_nothing)
  1.3558 +
  1.3559 +declare divide_poly_main_list.simps(1)[simp del]
  1.3560 +
  1.3561 +definition divide_poly_list :: "'a::idom_divide poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
  1.3562 +  "divide_poly_list f g =
  1.3563 +    (let cg = coeffs g
  1.3564 +     in if cg = [] then g
  1.3565 +        else let cf = coeffs f; cgr = rev cg
  1.3566 +          in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
  1.3567 +
  1.3568 +lemmas pdivmod_via_divmod_list[code] = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1]
  1.3569 +
  1.3570 +lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n"
  1.3571 +  by  (induct n arbitrary: q r d, auto simp: Let_def)
  1.3572 +
  1.3573 +lemma mod_poly_code[code]: "f mod g =
  1.3574 +    (let cg = coeffs g
  1.3575 +     in if cg = [] then f
  1.3576 +        else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
  1.3577 +                 r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
  1.3578 +             in poly_of_list (rev r))" (is "?l = ?r")
  1.3579 +proof -
  1.3580 +  have "?l = snd (pdivmod f g)" unfolding pdivmod_def by simp
  1.3581 +  also have "\<dots> = ?r" unfolding pdivmod_via_divmod_list Let_def
  1.3582 +     mod_poly_one_main_list[symmetric, of _ _ _ Nil] by (auto split: prod.splits)
  1.3583 +  finally show ?thesis .
  1.3584 +qed
  1.3585 +
  1.3586 +definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 
  1.3587 +  "div_field_poly_impl f g = (
  1.3588 +    let cg = coeffs g
  1.3589 +      in if cg = [] then 0
  1.3590 +        else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
  1.3591 +                 q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
  1.3592 +             in poly_of_list ((map (op * ilc) q)))"
  1.3593 +
  1.3594 +text \<open>We do not declare the following lemma as code equation, since then polynomial division 
  1.3595 +  on non-fields will no longer be executable. However, a code-unfold is possible, since 
  1.3596 +  \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close>
  1.3597 +lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl"
  1.3598 +proof (intro ext)
  1.3599 +  fix f g :: "'a poly"
  1.3600 +  have "f div g = fst (pdivmod f g)" unfolding pdivmod_def by simp
  1.3601 +  also have "\<dots> = div_field_poly_impl f g" unfolding 
  1.3602 +    div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits)
  1.3603 +  finally show "f div g =  div_field_poly_impl f g" .
  1.3604 +qed
  1.3605 +
  1.3606 +
  1.3607 +lemma divide_poly_main_list:
  1.3608 +  assumes lc0: "lc \<noteq> 0"
  1.3609 +  and lc:"last d = lc"
  1.3610 +  and d:"d \<noteq> []"
  1.3611 +  and "n = (1 + length r - length d)"
  1.3612 +  shows 
  1.3613 +  "Poly (divide_poly_main_list lc q (rev r) (rev d) n) =
  1.3614 +  divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n"
  1.3615 +using assms(4-)
  1.3616 +proof(induct "n" arbitrary: r q)
  1.3617 +case (Suc n r q)
  1.3618 +  have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
  1.3619 +  have r: "r \<noteq> []"
  1.3620 +    using ifCond d using Suc_leI length_greater_0_conv list.size(3) by fastforce
  1.3621 +  then obtain rr lcr where r: "r = rr @ [lcr]" by (cases r rule: rev_cases, auto)
  1.3622 +  from d lc obtain dd where d: "d = dd @ [lc]" 
  1.3623 +    by (cases d rule: rev_cases, auto)
  1.3624 +  from Suc(2) ifCond have n: "n = 1 + length rr - length d" by (auto simp: r)
  1.3625 +  from ifCond have len: "length dd \<le> length rr" by (simp add: r d)
  1.3626 +  show ?case
  1.3627 +  proof (cases "lcr div lc * lc = lcr")
  1.3628 +    case False
  1.3629 +    thus ?thesis unfolding Suc(2)[symmetric] using r d
  1.3630 +      by (auto simp add: Let_def nth_default_append)
  1.3631 +  next
  1.3632 +    case True
  1.3633 +    hence id:
  1.3634 +    "?thesis = (Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
  1.3635 +         (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) = 
  1.3636 +      divide_poly_main lc
  1.3637 +           (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
  1.3638 +           (Poly r - monom (lcr div lc) n * Poly d)
  1.3639 +           (Poly d) (length rr - 1) n)"
  1.3640 +           using r d 
  1.3641 +      by (cases r rule: rev_cases; cases "d" rule: rev_cases; 
  1.3642 +        auto simp add: Let_def rev_map nth_default_append)      
  1.3643 +    have cong: "\<And> x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  1.3644 +      divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n" by simp
  1.3645 +    show ?thesis unfolding id 
  1.3646 +    proof (subst Suc(1), simp add: n,
  1.3647 +      subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases)
  1.3648 +      case 2 
  1.3649 +      have "monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)"
  1.3650 +        by (simp add: mult_monom len True)
  1.3651 +      thus ?case unfolding r d Poly_append n ring_distribs
  1.3652 +        by (auto simp: Poly_map smult_monom smult_monom_mult)
  1.3653 +    qed (auto simp: len monom_Suc smult_monom)
  1.3654 +  qed
  1.3655 +qed simp
  1.3656 +
  1.3657 +
  1.3658 +lemma divide_poly_list[code]: "f div g = divide_poly_list f g" 
  1.3659 +proof -
  1.3660 +  note d = divide_poly_def divide_poly_list_def
  1.3661 +  show ?thesis
  1.3662 +  proof (cases "g = 0")
  1.3663 +    case True
  1.3664 +    show ?thesis unfolding d True by auto
  1.3665 +  next
  1.3666 +    case False
  1.3667 +    then obtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases, auto)    
  1.3668 +    with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False" by auto
  1.3669 +    from cg False have lcg: "coeff g (degree g) = lcg" 
  1.3670 +      using last_coeffs_eq_coeff_degree last_snoc by force
  1.3671 +    with False have lcg0: "lcg \<noteq> 0" by auto
  1.3672 +    from cg have ltp: "Poly (cg @ [lcg]) = g"
  1.3673 +     using Poly_coeffs [of g] by auto
  1.3674 +    show ?thesis unfolding d cg Let_def id if_False poly_of_list_def
  1.3675 +      by (subst divide_poly_main_list, insert False cg lcg0, auto simp: lcg ltp,
  1.3676 +      simp add: degree_eq_length_coeffs)
  1.3677 +  qed
  1.3678  qed
  1.3679  
  1.3680  no_notation cCons (infixr "##" 65)
     2.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Thu Jan 05 14:49:21 2017 +0100
     2.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Thu Jan 05 17:11:21 2017 +0100
     2.3 @@ -19,40 +19,6 @@
     2.4  lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
     2.5    by (induction A) (simp_all add: one_poly_def mult_ac)
     2.6  
     2.7 -lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
     2.8 -proof -
     2.9 -  have "smult c p = [:c:] * p" by simp
    2.10 -  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
    2.11 -  proof safe
    2.12 -    assume A: "[:c:] * p dvd 1"
    2.13 -    thus "p dvd 1" by (rule dvd_mult_right)
    2.14 -    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
    2.15 -    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
    2.16 -    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
    2.17 -    also note B [symmetric]
    2.18 -    finally show "c dvd 1" by simp
    2.19 -  next
    2.20 -    assume "c dvd 1" "p dvd 1"
    2.21 -    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
    2.22 -    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
    2.23 -    hence "[:c:] dvd 1" by (rule dvdI)
    2.24 -    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
    2.25 -  qed
    2.26 -  finally show ?thesis .
    2.27 -qed
    2.28 -
    2.29 -lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
    2.30 -  using degree_mod_less[of b a] by auto
    2.31 -  
    2.32 -lemma smult_eq_iff:
    2.33 -  assumes "(b :: 'a :: field) \<noteq> 0"
    2.34 -  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
    2.35 -proof
    2.36 -  assume "smult a p = smult b q"
    2.37 -  also from assms have "smult (inverse b) \<dots> = q" by simp
    2.38 -  finally show "smult (a / b) p = q" by (simp add: field_simps)
    2.39 -qed (insert assms, auto)
    2.40 -
    2.41  lemma irreducible_const_poly_iff:
    2.42    fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
    2.43    shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
    2.44 @@ -160,145 +126,6 @@
    2.45    by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
    2.46  
    2.47  
    2.48 -subsection \<open>Content and primitive part of a polynomial\<close>
    2.49 -
    2.50 -definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
    2.51 -  "content p = Gcd (set (coeffs p))"
    2.52 -
    2.53 -lemma content_0 [simp]: "content 0 = 0"
    2.54 -  by (simp add: content_def)
    2.55 -
    2.56 -lemma content_1 [simp]: "content 1 = 1"
    2.57 -  by (simp add: content_def)
    2.58 -
    2.59 -lemma content_const [simp]: "content [:c:] = normalize c"
    2.60 -  by (simp add: content_def cCons_def)
    2.61 -
    2.62 -lemma const_poly_dvd_iff_dvd_content:
    2.63 -  fixes c :: "'a :: semiring_Gcd"
    2.64 -  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
    2.65 -proof (cases "p = 0")
    2.66 -  case [simp]: False
    2.67 -  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
    2.68 -  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
    2.69 -  proof safe
    2.70 -    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
    2.71 -    thus "c dvd coeff p n"
    2.72 -      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
    2.73 -  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
    2.74 -  also have "\<dots> \<longleftrightarrow> c dvd content p"
    2.75 -    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
    2.76 -          dvd_mult_unit_iff)
    2.77 -  finally show ?thesis .
    2.78 -qed simp_all
    2.79 -
    2.80 -lemma content_dvd [simp]: "[:content p:] dvd p"
    2.81 -  by (subst const_poly_dvd_iff_dvd_content) simp_all
    2.82 -  
    2.83 -lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
    2.84 -  by (cases "n \<le> degree p") 
    2.85 -     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
    2.86 -
    2.87 -lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
    2.88 -  by (simp add: content_def Gcd_dvd)
    2.89 -
    2.90 -lemma normalize_content [simp]: "normalize (content p) = content p"
    2.91 -  by (simp add: content_def)
    2.92 -
    2.93 -lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
    2.94 -proof
    2.95 -  assume "is_unit (content p)"
    2.96 -  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
    2.97 -  thus "content p = 1" by simp
    2.98 -qed auto
    2.99 -
   2.100 -lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
   2.101 -  by (simp add: content_def coeffs_smult Gcd_mult)
   2.102 -
   2.103 -lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   2.104 -  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
   2.105 -
   2.106 -definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
   2.107 -  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
   2.108 -  
   2.109 -lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
   2.110 -  by (simp add: primitive_part_def)
   2.111 -
   2.112 -lemma content_times_primitive_part [simp]:
   2.113 -  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
   2.114 -  shows "smult (content p) (primitive_part p) = p"
   2.115 -proof (cases "p = 0")
   2.116 -  case False
   2.117 -  thus ?thesis
   2.118 -  unfolding primitive_part_def
   2.119 -  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
   2.120 -           intro: map_poly_idI)
   2.121 -qed simp_all
   2.122 -
   2.123 -lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   2.124 -proof (cases "p = 0")
   2.125 -  case False
   2.126 -  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   2.127 -    by (simp add:  primitive_part_def)
   2.128 -  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   2.129 -    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   2.130 -  finally show ?thesis using False by simp
   2.131 -qed simp
   2.132 -
   2.133 -lemma content_primitive_part [simp]:
   2.134 -  assumes "p \<noteq> 0"
   2.135 -  shows   "content (primitive_part p) = 1"
   2.136 -proof -
   2.137 -  have "p = smult (content p) (primitive_part p)" by simp
   2.138 -  also have "content \<dots> = content p * content (primitive_part p)" 
   2.139 -    by (simp del: content_times_primitive_part)
   2.140 -  finally show ?thesis using assms by simp
   2.141 -qed
   2.142 -
   2.143 -lemma content_decompose:
   2.144 -  fixes p :: "'a :: semiring_Gcd poly"
   2.145 -  obtains p' where "p = smult (content p) p'" "content p' = 1"
   2.146 -proof (cases "p = 0")
   2.147 -  case True
   2.148 -  thus ?thesis by (intro that[of 1]) simp_all
   2.149 -next
   2.150 -  case False
   2.151 -  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
   2.152 -  have "content p * 1 = content p * content r" by (subst r) simp
   2.153 -  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
   2.154 -  with r show ?thesis by (intro that[of r]) simp_all
   2.155 -qed
   2.156 -
   2.157 -lemma smult_content_normalize_primitive_part [simp]:
   2.158 -  "smult (content p) (normalize (primitive_part p)) = normalize p"
   2.159 -proof -
   2.160 -  have "smult (content p) (normalize (primitive_part p)) = 
   2.161 -          normalize ([:content p:] * primitive_part p)" 
   2.162 -    by (subst normalize_mult) (simp_all add: normalize_const_poly)
   2.163 -  also have "[:content p:] * primitive_part p = p" by simp
   2.164 -  finally show ?thesis .
   2.165 -qed
   2.166 -
   2.167 -lemma content_dvd_contentI [intro]:
   2.168 -  "p dvd q \<Longrightarrow> content p dvd content q"
   2.169 -  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   2.170 -  
   2.171 -lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   2.172 -  by (simp add: primitive_part_def map_poly_pCons)
   2.173 - 
   2.174 -lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   2.175 -  by (auto simp: primitive_part_def)
   2.176 -  
   2.177 -lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   2.178 -proof (cases "p = 0")
   2.179 -  case False
   2.180 -  have "p = smult (content p) (primitive_part p)" by simp
   2.181 -  also from False have "degree \<dots> = degree (primitive_part p)"
   2.182 -    by (subst degree_smult_eq) simp_all
   2.183 -  finally show ?thesis ..
   2.184 -qed simp_all
   2.185 -
   2.186 -
   2.187  subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
   2.188  
   2.189  abbreviation (input) fract_poly