# HG changeset patch
# User eberlm
# Date 1452526719 -3600
# Node ID 3201ddb00097498ff3b724d2cd43df0e7c60ead7
# Parent  d8e7738bd2e9c04bb23427fe5a983dbafba8632c
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Binomial.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -76,7 +76,7 @@
       by (metis of_nat_mult order_refl power_Suc)
     finally show ?case .
   qed simp
-
+  
 end
 
 text\<open>Note that @{term "fact 0 = fact 1"}\<close>
@@ -94,11 +94,17 @@
   shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
   by (induct n) (auto simp: dvdI le_Suc_eq)
 
+lemma fact_ge_self: "fact n \<ge> n"
+  by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
+
 lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
   by (induct n) (auto simp: atLeastAtMostSuc_conv)
 
-lemma fact_altdef: "fact n = setprod of_nat {1..n}"
+lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
   by (induct n) (auto simp: atLeastAtMostSuc_conv)
+  
+lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
+  by (subst fact_altdef_nat [symmetric]) simp
 
 lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
   by (induct m) (auto simp: le_Suc_eq)
@@ -1538,4 +1544,42 @@
        (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
 qed
 
+
+
+lemma fact_code [code]:
+  "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"
+proof -
+  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)" by (simp add: fact_altdef')
+  also have "\<Prod>{1..n} = \<Prod>{2..n}"
+    by (intro setprod.mono_neutral_right) auto
+  also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
+    by (simp add: setprod_atLeastAtMost_code)
+  finally show ?thesis .
+qed
+
+lemma pochhammer_code [code]:
+  "pochhammer a n = (if n = 0 then 1 else 
+       fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
+  by (simp add: setprod_atLeastAtMost_code pochhammer_def)
+
+lemma gbinomial_code [code]:
+  "a gchoose n = (if n = 0 then 1 else 
+     fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
+  by (simp add: setprod_atLeastAtMost_code gbinomial_def)
+
+lemma binomial_code [code]:
+  "(n choose k) =
+      (if k > n then 0
+       else if 2 * k > n then (n choose (n - k))
+       else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
+proof -
+  {
+    assume "k \<le> n"
+    hence "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
+    hence "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
+      by (simp add: setprod.union_disjoint fact_altdef_nat)
+  }
+  thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
+qed 
+
 end
diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Int.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -314,6 +314,12 @@
   "of_int z < 1 \<longleftrightarrow> z < 1"
   using of_int_less_iff [of z 1] by simp
 
+lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
+  by simp
+
+lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
+  by simp
+
 end
 
 text \<open>Comparisons involving @{term of_int}.\<close>
diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -1066,11 +1066,6 @@
   qed
 qed
 
-lemma divides_degree:
-  assumes pq: "p dvd (q:: complex poly)"
-  shows "degree p \<le> degree q \<or> q = 0"
-  by (metis dvd_imp_degree_le pq)
-
 text \<open>Arithmetic operations on multivariate polynomials.\<close>
 
 lemma mpoly_base_conv:
diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -11,7 +11,7 @@
 
 subsection \<open>Derivatives of univariate polynomials\<close>
 
-function pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly"
+function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
 where
   [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
   by (auto intro: pCons_cases)
@@ -27,27 +27,98 @@
   "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
   by (simp add: pderiv.simps)
 
+lemma pderiv_1 [simp]: "pderiv 1 = 0" 
+  unfolding one_poly_def by (simp add: pderiv_pCons)
+
+lemma pderiv_of_nat  [simp]: "pderiv (of_nat n) = 0"
+  and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
+  by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
+
 lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
   by (induct p arbitrary: n) 
      (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
 
-primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
-where
-  "pderiv_coeffs [] = []"
-| "pderiv_coeffs (x # xs) = plus_coeffs xs (cCons 0 (pderiv_coeffs xs))"
+fun pderiv_coeffs_code :: "('a :: semidom) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
+| "pderiv_coeffs_code f [] = []"
+
+definition pderiv_coeffs :: "('a :: semidom) list \<Rightarrow> 'a list" where
+  "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
 
-lemma coeffs_pderiv [code abstract]:
-  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
-  by (rule sym, induct p) (simp_all add: pderiv_pCons coeffs_plus_eq_plus_coeffs cCons_def)
+(* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
+lemma pderiv_coeffs_code: 
+  "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)"
+proof (induct xs arbitrary: f n)
+  case (Cons x xs f n)
+  show ?case 
+  proof (cases n)
+    case 0
+    thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0", auto simp: cCons_def)
+  next
+    case (Suc m) note n = this
+    show ?thesis 
+    proof (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0")
+      case False
+      hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 
+               nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" 
+        by (auto simp: cCons_def n)
+      also have "\<dots> = (f + of_nat n) * (nth_default 0 xs m)" 
+        unfolding Cons by (simp add: n add_ac)
+      finally show ?thesis by (simp add: n)
+    next
+      case True
+      {
+        fix g 
+        have "pderiv_coeffs_code g xs = [] \<Longrightarrow> g + of_nat m = 0 \<or> nth_default 0 xs m = 0"
+        proof (induct xs arbitrary: g m)
+          case (Cons x xs g)
+          from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []"
+                            and g: "(g = 0 \<or> x = 0)"
+            by (auto simp: cCons_def split: if_splits)
+          note IH = Cons(1)[OF empty]
+          from IH[of m] IH[of "m - 1"] g
+          show ?case by (cases m, auto simp: field_simps)
+        qed simp
+      } note empty = this
+      from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0"
+        by (auto simp: cCons_def n)
+      moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True
+        by (simp add: n, insert empty[of "f+1"], auto simp: field_simps)
+      ultimately show ?thesis by simp
+    qed
+  qed
+qed simp
 
-lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
+lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda> i. f (Suc i)) [0 ..< n]"
+  by (induct n arbitrary: f, auto)
+
+lemma coeffs_pderiv_code [code abstract]:
+  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def
+proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
+  case (1 n)
+  have id: "coeff p (Suc n) = nth_default 0 (map (\<lambda>i. coeff p (Suc i)) [0..<degree p]) n"
+    by (cases "n < degree p", auto simp: nth_default_def coeff_eq_0)
+  show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id)
+next
+  case 2
+  obtain n xs where id: "tl (coeffs p) = xs" "(1 :: 'a) = n" by auto
+  from 2 show ?case
+    unfolding id by (induct xs arbitrary: n, auto simp: cCons_def)
+qed
+
+context
+  assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})"
+begin
+
+lemma pderiv_eq_0_iff: 
+  "pderiv (p :: 'a poly) = 0 \<longleftrightarrow> degree p = 0"
   apply (rule iffI)
   apply (cases p, simp)
   apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
   apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
   done
 
-lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
+lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1"
   apply (rule order_antisym [OF degree_le])
   apply (simp add: coeff_pderiv coeff_eq_0)
   apply (cases "degree p", simp)
@@ -56,14 +127,30 @@
   apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
   done
 
+lemma not_dvd_pderiv: 
+  assumes "degree (p :: 'a poly) \<noteq> 0"
+  shows "\<not> p dvd pderiv p"
+proof
+  assume dvd: "p dvd pderiv p"
+  then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto
+  from dvd have le: "degree p \<le> degree (pderiv p)"
+    by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff)
+  from this[unfolded degree_pderiv] assms show False by auto
+qed
+
+lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \<longleftrightarrow> degree p = 0"
+  using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
+
+end
+
 lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
 by (simp add: pderiv_pCons)
 
 lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
 
-lemma pderiv_minus: "pderiv (- p) = - pderiv p"
-by (rule poly_eqI, simp add: coeff_pderiv)
+lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
+by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
 
 lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
@@ -85,6 +172,27 @@
 apply (simp add: algebra_simps)
 done
 
+lemma pderiv_setprod: "pderiv (setprod f (as)) = 
+  (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
+proof (induct as rule: infinite_finite_induct)
+  case (insert a as)
+  hence id: "setprod f (insert a as) = f a * setprod f as" 
+    "\<And> g. setsum g (insert a as) = g a + setsum g as"
+    "insert a as - {a} = as"
+    by auto
+  {
+    fix b
+    assume "b \<in> as"
+    hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto
+    have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
+      unfolding id2
+      by (subst setprod.insert, insert insert, auto)
+  } note id2 = this
+  show ?case
+    unfolding id pderiv_mult insert(3) setsum_right_distrib
+    by (auto simp add: ac_simps id2 intro!: setsum.cong)
+qed auto
+
 lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
 by (rule DERIV_cong, rule DERIV_pow, simp)
 declare DERIV_pow2 [simp] DERIV_pow [simp]
@@ -92,7 +200,7 @@
 lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: 'a::real_normed_field) x :> D"
 by (rule DERIV_cong, rule DERIV_add, auto)
 
-lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
+lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
   by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
 
 lemma continuous_on_poly [continuous_intros]: 
@@ -186,6 +294,104 @@
 qed
 
 
+subsection \<open>Algebraic numbers\<close>
+
+text \<open>
+  Algebraic numbers can be defined in two equivalent ways: all real numbers that are 
+  roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry 
+  uses the rational definition, but we need the integer definition.
+
+  The equivalence is obvious since any rational polynomial can be multiplied with the 
+  LCM of its coefficients, yielding an integer polynomial with the same roots.
+\<close>
+subsection \<open>Algebraic numbers\<close>
+
+definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
+  "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
+
+lemma algebraicI:
+  assumes "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
+  shows   "algebraic x"
+  using assms unfolding algebraic_def by blast
+  
+lemma algebraicE:
+  assumes "algebraic x"
+  obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
+  using assms unfolding algebraic_def by blast
+
+lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
+  using quotient_of_denom_pos[OF surjective_pairing] .
+  
+lemma of_int_div_in_Ints: 
+  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: ring_div set)"
+proof (cases "of_int b = (0 :: 'a)")
+  assume "b dvd a" "of_int b \<noteq> (0::'a)"
+  then obtain c where "a = b * c" by (elim dvdE)
+  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
+qed auto
+
+lemma of_int_divide_in_Ints: 
+  "b dvd a \<Longrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: field set)"
+proof (cases "of_int b = (0 :: 'a)")
+  assume "b dvd a" "of_int b \<noteq> (0::'a)"
+  then obtain c where "a = b * c" by (elim dvdE)
+  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
+qed auto
+
+lemma algebraic_altdef:
+  fixes p :: "'a :: field_char_0 poly"
+  shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
+proof safe
+  fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
+  def cs \<equiv> "coeffs p"
+  from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
+  then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
+    by (subst (asm) bchoice_iff) blast
+  def cs' \<equiv> "map (quotient_of \<circ> f) (coeffs p)"
+  def d \<equiv> "Lcm (set (map snd cs'))"
+  def p' \<equiv> "smult (of_int d) p"
+  
+  have "\<forall>n. coeff p' n \<in> \<int>"
+  proof
+    fix n :: nat
+    show "coeff p' n \<in> \<int>"
+    proof (cases "n \<le> degree p")
+      case True
+      def c \<equiv> "coeff p n"
+      def a \<equiv> "fst (quotient_of (f (coeff p n)))" and b \<equiv> "snd (quotient_of (f (coeff p n)))"
+      have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp
+      have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def)
+      also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def
+        by (subst quotient_of_div [of "f (coeff p n)", symmetric])
+           (simp_all add: f [symmetric])
+      also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
+        by (simp add: of_rat_mult of_rat_divide)
+      also from nz True have "b \<in> snd ` set cs'" unfolding cs'_def
+        by (force simp: o_def b_def coeffs_def simp del: upt_Suc)
+      hence "b dvd (a * d)" unfolding d_def by simp
+      hence "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
+        by (rule of_int_divide_in_Ints)
+      hence "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
+      finally show ?thesis .
+    qed (auto simp: p'_def not_le coeff_eq_0)
+  qed
+  
+  moreover have "set (map snd cs') \<subseteq> {0<..}"
+    unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) 
+  hence "d \<noteq> 0" unfolding d_def by (induction cs') simp_all
+  with nz have "p' \<noteq> 0" by (simp add: p'_def)
+  moreover from root have "poly p' x = 0" by (simp add: p'_def)
+  ultimately show "algebraic x" unfolding algebraic_def by blast
+next
+
+  assume "algebraic x"
+  then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
+    by (force simp: algebraic_def)
+  moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
+  ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
+qed
+
+
 text\<open>Lemmas for Derivatives\<close>
 
 lemma order_unique_lemma:
@@ -209,12 +415,8 @@
 apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
 done
 
-lemma dvd_add_cancel1:
-  fixes a b c :: "'a::comm_ring_1"
-  shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
-  by (drule (1) Rings.dvd_diff, simp)
-
 lemma lemma_order_pderiv:
+  fixes p :: "'a :: field_char_0 poly"
   assumes n: "0 < n" 
       and pd: "pderiv p \<noteq> 0" 
       and pe: "p = [:- a, 1:] ^ n * q" 
@@ -226,8 +428,8 @@
     using assms by auto
   obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
     using assms by (cases n) auto
-  then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
-    by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2))
+  have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
+    by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
   have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
   proof (rule order_unique_lemma)
     show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
@@ -262,8 +464,9 @@
   from C D show ?thesis by blast
 qed
 
-lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
-      ==> (order a p = Suc (order a (pderiv p)))"
+lemma order_pderiv:
+  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
+     (order a p = Suc (order a (pderiv p)))"
 apply (case_tac "p = 0", simp)
 apply (drule_tac a = a and p = p in order_decomp)
 using neq0_conv
@@ -344,7 +547,7 @@
 done
 
 lemma poly_squarefree_decomp_order:
-  assumes "pderiv p \<noteq> 0"
+  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
   and p: "p = q * d"
   and p': "pderiv p = e * d"
   and d: "d = r * p + s * pderiv p"
@@ -379,28 +582,31 @@
     by auto
 qed
 
-lemma poly_squarefree_decomp_order2: "[| pderiv p \<noteq> 0;
-         p = q * d;
-         pderiv p = e * d;
-         d = r * p + s * pderiv p
-      |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
+lemma poly_squarefree_decomp_order2: 
+     "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
+       p = q * d;
+       pderiv p = e * d;
+       d = r * p + s * pderiv p
+      \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
 by (blast intro: poly_squarefree_decomp_order)
 
-lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
-      ==> (order a (pderiv p) = n) = (order a p = Suc n)"
+lemma order_pderiv2: 
+  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
+      \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
 by (auto dest: order_pderiv)
 
 definition
   rsquarefree :: "'a::idom poly => bool" where
   "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
 
-lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]"
+lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
 apply (simp add: pderiv_eq_0_iff)
 apply (case_tac p, auto split: if_splits)
 done
 
 lemma rsquarefree_roots:
-  "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
+  fixes p :: "'a :: field_char_0 poly"
+  shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
 apply (simp add: rsquarefree_def)
 apply (case_tac "p = 0", simp, simp)
 apply (case_tac "pderiv p = 0")
@@ -411,7 +617,7 @@
 done
 
 lemma poly_squarefree_decomp:
-  assumes "pderiv p \<noteq> 0"
+  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
     and "p = q * d"
     and "pderiv p = e * d"
     and "d = r * p + s * pderiv p"
diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -456,7 +456,7 @@
 lemma poly_0 [simp]:
   "poly 0 x = 0"
   by (simp add: poly_def)
-
+  
 lemma poly_pCons [simp]:
   "poly (pCons a p) x = a + x * poly p x"
   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
@@ -480,6 +480,9 @@
    qed simp
 qed simp
 
+lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
+  by (cases p) (auto simp: poly_altdef)
+
 
 subsection \<open>Monomials\<close>
 
@@ -744,6 +747,28 @@
 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
   by (induct A rule: infinite_finite_induct) simp_all
 
+lemma degree_setsum_le: "finite S \<Longrightarrow> (\<And> p . p \<in> S \<Longrightarrow> degree (f p) \<le> n)
+  \<Longrightarrow> degree (setsum f S) \<le> n"
+proof (induct S rule: finite_induct)
+  case (insert p S)
+  hence "degree (setsum f S) \<le> n" "degree (f p) \<le> n" by auto
+  thus ?case unfolding setsum.insert[OF insert(1-2)] by (metis degree_add_le)
+qed simp
+
+lemma poly_as_sum_of_monoms': 
+  assumes n: "degree p \<le> n" 
+  shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
+proof -
+  have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
+    by auto
+  show ?thesis
+    using n by (simp add: poly_eq_iff coeff_setsum coeff_eq_0 setsum.If_cases eq 
+                  if_distrib[where f="\<lambda>x. x * a" for a])
+qed
+
+lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
+  by (intro poly_as_sum_of_monoms' order_refl)
+
 lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
   by (induction xs) (simp_all add: monom_0 monom_Suc)
 
@@ -957,7 +982,16 @@
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n) simp_all
 
-  
+lemma poly_setprod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma degree_setprod_setsum_le: "finite S \<Longrightarrow> degree (setprod f S) \<le> setsum (degree o f) S"
+proof (induct S rule: finite_induct)
+  case (insert a S)
+  show ?case unfolding setprod.insert[OF insert(1-2)] setsum.insert[OF insert(1-2)]
+    by (rule le_trans[OF degree_mult_le], insert insert, auto)
+qed simp
+
 subsection \<open>Conversions from natural numbers\<close>
 
 lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
@@ -991,7 +1025,7 @@
 qed
 
 lemma dvd_smult_cancel:
-  fixes a :: "'a::field"
+  fixes a :: "'a :: field"
   shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
   by (drule dvd_smult [where a="inverse a"]) simp
 
@@ -1041,29 +1075,33 @@
 qed
 
 lemma degree_mult_eq:
-  fixes p q :: "'a::idom poly"
+  fixes p q :: "'a::semidom poly"
   shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
 apply (rule order_antisym [OF degree_mult_le le_degree])
 apply (simp add: coeff_mult_degree_sum)
 done
 
 lemma degree_mult_right_le:
-  fixes p q :: "'a::idom poly"
+  fixes p q :: "'a::semidom poly"
   assumes "q \<noteq> 0"
   shows "degree p \<le> degree (p * q)"
   using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
 
 lemma coeff_degree_mult:
-  fixes p q :: "'a::idom poly"
+  fixes p q :: "'a::semidom poly"
   shows "coeff (p * q) (degree (p * q)) =
     coeff q (degree q) * coeff p (degree p)"
-  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum)
+  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum mult_ac)
 
 lemma dvd_imp_degree_le:
-  fixes p q :: "'a::idom poly"
+  fixes p q :: "'a::semidom poly"
   shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
-  by (erule dvdE, simp add: degree_mult_eq)
+  by (erule dvdE, hypsubst, subst degree_mult_eq) auto
 
+lemma divides_degree:
+  assumes pq: "p dvd (q :: 'a :: semidom poly)"
+  shows "degree p \<le> degree q \<or> q = 0"
+  by (metis dvd_imp_degree_le pq)
 
 subsection \<open>Polynomials form an ordered integral domain\<close>
 
@@ -2048,18 +2086,27 @@
 
 subsection \<open>Composition of polynomials\<close>
 
+(* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
+
 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
 where
   "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
 
+notation pcompose (infixl "\<circ>\<^sub>p" 71)
+
 lemma pcompose_0 [simp]:
   "pcompose 0 q = 0"
   by (simp add: pcompose_def)
-
+  
 lemma pcompose_pCons:
   "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
   by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
 
+lemma pcompose_1:
+  fixes p :: "'a :: comm_semiring_1 poly"
+  shows "pcompose 1 p = 1"
+  unfolding one_poly_def by (auto simp: pcompose_pCons)
+
 lemma poly_pcompose:
   "poly (pcompose p q) x = poly p (poly q x)"
   by (induct p) (simp_all add: pcompose_pCons)
@@ -2087,7 +2134,7 @@
   finally show ?case .
 qed simp
 
-lemma pcompose_minus:
+lemma pcompose_uminus:
   fixes p r :: "'a :: comm_ring poly"
   shows "pcompose (-p) r = -pcompose p r"
   by (induction p) (simp_all add: pcompose_pCons)
@@ -2095,7 +2142,7 @@
 lemma pcompose_diff:
   fixes p q r :: "'a :: comm_ring poly"
   shows "pcompose (p - q) r = pcompose p r - pcompose q r"
-  using pcompose_add[of p "-q"] by (simp add: pcompose_minus)
+  using pcompose_add[of p "-q"] by (simp add: pcompose_uminus)
 
 lemma pcompose_smult:
   fixes p r :: "'a :: comm_semiring_0 poly"
@@ -2115,24 +2162,27 @@
   by (induction p arbitrary: q) 
      (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
 
+lemma pcompose_idR[simp]:
+  fixes p :: "'a :: comm_semiring_1 poly"
+  shows "pcompose p [: 0, 1 :] = p"
+  by (induct p; simp add: pcompose_pCons)
+
 
 (* The remainder of this section and the next were contributed by Wenda Li *)
 
 lemma degree_mult_eq_0:
-  fixes p q:: "'a :: idom poly"
+  fixes p q:: "'a :: semidom poly"
   shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
 by (auto simp add:degree_mult_eq)
 
 lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) 
 
-lemma pcompose_0':"pcompose p 0=[:coeff p 0:]"
-  apply (induct p)
-  apply (auto simp add:pcompose_pCons)
-done
+lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
+  by (induct p) (auto simp add:pcompose_pCons)
 
 lemma degree_pcompose:
-  fixes p q:: "'a::idom poly"
-  shows "degree(pcompose p q) = degree p * degree q"
+  fixes p q:: "'a::semidom poly"
+  shows "degree (pcompose p q) = degree p * degree q"
 proof (induct p)
   case 0
   thus ?case by auto
@@ -2144,7 +2194,7 @@
       thus ?thesis by auto
     next
       case False assume "degree (q * pcompose p q) = 0"
-      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
+      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add: degree_mult_eq_0)
       moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close> 
         proof -
           assume "pcompose p q=0" "degree q\<noteq>0"
@@ -2178,9 +2228,9 @@
 qed
 
 lemma pcompose_eq_0:
-  fixes p q:: "'a::idom poly"
-  assumes "pcompose p q=0" "degree q>0" 
-  shows "p=0"
+  fixes p q:: "'a :: semidom poly"
+  assumes "pcompose p q = 0" "degree q > 0" 
+  shows "p = 0"
 proof -
   have "degree p=0" using assms degree_pcompose[of p q] by auto
   then obtain a where "p=[:a:]" 
diff -r d8e7738bd2e9 -r 3201ddb00097 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jan 11 15:20:17 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Jan 11 16:38:39 2016 +0100
@@ -1902,4 +1902,52 @@
   finally show ?thesis .
 qed
 
+
+subsection \<open>Efficient folding over intervals\<close>
+
+function fold_atLeastAtMost_nat where
+  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
+                 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"
+by pat_completeness auto
+termination by (relation "measure (\<lambda>(_,a,b,_). Suc b - a)") auto
+
+lemma fold_atLeastAtMost_nat:
+  assumes "comp_fun_commute f"
+  shows   "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
+using assms
+proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
+  case (1 f a b acc)
+  interpret comp_fun_commute f by fact
+  show ?case
+  proof (cases "a > b")
+    case True
+    thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
+  next
+    case False
+    with 1 show ?thesis
+      by (subst fold_atLeastAtMost_nat.simps)
+         (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
+  qed
+qed
+
+lemma setsum_atLeastAtMost_code:
+  "setsum f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a + acc) a b 0"
+proof -
+  have "comp_fun_commute (\<lambda>a. op + (f a))"
+    by unfold_locales (auto simp: o_def add_ac)
+  thus ?thesis
+    by (simp add: setsum.eq_fold fold_atLeastAtMost_nat o_def)
+qed
+
+lemma setprod_atLeastAtMost_code:
+  "setprod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
+proof -
+  have "comp_fun_commute (\<lambda>a. op * (f a))"
+    by unfold_locales (auto simp: o_def mult_ac)
+  thus ?thesis
+    by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
+qed
+
+(* TODO: Add support for more kinds of intervals here *)
+
 end