# HG changeset patch
# User eberlm
# Date 1452012850 -3600
# Node ID 1546a042e87b391e9802f492734ba6f745b6035b
# Parent  b75764fc4c350989d2b8e457e978d00079686ba1
Added some facts about polynomials

diff -r b75764fc4c35 -r 1546a042e87b src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -95,6 +95,17 @@
 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]: 
+  fixes p :: "'a :: {real_normed_field} poly"
+  assumes "continuous_on A f"
+  shows   "continuous_on A (\<lambda>x. poly p (f x))"
+proof -
+  have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))" 
+    by (intro continuous_intros assms)
+  also have "\<dots> = (\<lambda>x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac)
+  finally show ?thesis .
+qed
+
 text\<open>Consequences of the derivative theorem above\<close>
 
 lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
@@ -114,6 +125,12 @@
       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
 by (insert poly_IVT_pos [where p = "- p" ]) simp
 
+lemma poly_IVT:
+  fixes p::"real poly"
+  assumes "a<b" and "poly p a * poly p b < 0"
+  shows "\<exists>x>a. x < b \<and> poly p x = 0"
+by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
+
 lemma poly_MVT: "(a::real) < b ==>
      \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
 using MVT [of a b "poly p"]
@@ -122,6 +139,53 @@
 apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
 done
 
+lemma poly_MVT':
+  assumes "{min a b..max a b} \<subseteq> A"
+  shows   "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)"
+proof (cases a b rule: linorder_cases)
+  case less
+  from poly_MVT[OF less, of p] guess x by (elim exE conjE)
+  thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
+
+next
+  case greater
+  from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
+  thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
+qed (insert assms, auto)
+
+lemma poly_pinfty_gt_lc:
+  fixes p:: "real poly"
+  assumes  "lead_coeff p > 0" 
+  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
+proof (induct p)
+  case 0
+  thus ?case by auto
+next
+  case (pCons a p)
+  have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
+  moreover have "p\<noteq>0 \<Longrightarrow> ?case"
+    proof -
+      assume "p\<noteq>0"
+      then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
+      have gt_0:"lead_coeff p >0" using pCons(3) `p\<noteq>0` by auto
+      def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
+      show ?thesis 
+        proof (rule_tac x=n in exI,rule,rule) 
+          fix x assume "n \<le> x"
+          hence "lead_coeff p \<le> poly p x" 
+            using gte_lcoeff unfolding n_def by auto
+          hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
+            by (intro frac_le,auto)
+          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using `n\<le>x`[unfolded n_def] by auto
+          thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
+            using `lead_coeff p \<le> poly p x` `poly p x>0` `p\<noteq>0`
+            by (auto simp add:field_simps)
+        qed
+    qed
+  ultimately show ?case by fastforce
+qed
+
+
 text\<open>Lemmas for Derivatives\<close>
 
 lemma order_unique_lemma:
@@ -225,6 +289,51 @@
     done
 qed
 
+lemma order_smult:
+  assumes "c \<noteq> 0" 
+  shows "order x (smult c p) = order x p"
+proof (cases "p = 0")
+  case False
+  have "smult c p = [:c:] * p" by simp
+  also from assms False have "order x \<dots> = order x [:c:] + order x p" 
+    by (subst order_mult) simp_all
+  also from assms have "order x [:c:] = 0" by (intro order_0I) auto
+  finally show ?thesis by simp
+qed simp
+
+(* Next two lemmas contributed by Wenda Li *)
+lemma order_1_eq_0 [simp]:"order x 1 = 0" 
+  by (metis order_root poly_1 zero_neq_one)
+
+lemma order_power_n_n: "order a ([:-a,1:]^n)=n" 
+proof (induct n) (*might be proved more concisely using nat_less_induct*)
+  case 0
+  thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
+next 
+  case (Suc n)
+  have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" 
+    by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral 
+      one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
+  moreover have "order a [:-a,1:]=1" unfolding order_def
+    proof (rule Least_equality,rule ccontr)
+      assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
+      hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
+      hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )" 
+        by (rule dvd_imp_degree_le,auto) 
+      thus False by auto
+    next
+      fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
+      show "1 \<le> y" 
+        proof (rule ccontr)
+          assume "\<not> 1 \<le> y"
+          hence "y=0" by auto
+          hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
+          thus False using asm by auto
+        qed
+    qed
+  ultimately show ?case using Suc by auto
+qed
+
 text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
 
 lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
diff -r b75764fc4c35 -r 1546a042e87b src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -281,7 +281,10 @@
 lemma Poly_eq_0:
   "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
   by (induct as) (auto simp add: Cons_replicate_eq)
-
+  
+lemma degree_Poly: "degree (Poly xs) \<le> length xs"
+  by (induction xs) simp_all
+  
 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
 where
   "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
@@ -311,6 +314,14 @@
     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
 qed
 
+lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
+  by (simp add: coeffs_def)
+  
+lemma coeffs_nth:
+  assumes "p \<noteq> 0" "n \<le> degree p"
+  shows   "coeffs p ! n = coeff p n"
+  using assms unfolding coeffs_def by (auto simp del: upt_Suc)
+
 lemma not_0_cCons_eq [simp]:
   "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
   by (simp add: cCons_def)
@@ -450,6 +461,25 @@
   "poly (pCons a p) x = a + x * poly p x"
   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
 
+lemma poly_altdef: 
+  "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
+proof (induction p rule: pCons_induct)
+  case (pCons a p)
+    show ?case
+    proof (cases "p = 0")
+      case False
+      let ?p' = "pCons a p"
+      note poly_pCons[of a p x]
+      also note pCons.IH
+      also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
+                 coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
+          by (simp add: field_simps setsum_right_distrib coeff_pCons)
+      also note setsum_atMost_Suc_shift[symmetric]
+      also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
+      finally show ?thesis .
+   qed simp
+qed simp
+
 
 subsection \<open>Monomials\<close>
 
@@ -500,7 +530,7 @@
   by (cases "a = 0", simp_all)
     (induct n, simp_all add: mult.left_commute poly_def)
 
-
+    
 subsection \<open>Addition and subtraction\<close>
 
 instantiation poly :: (comm_monoid_add) comm_monoid_add
@@ -714,6 +744,9 @@
 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 Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
+  by (induction xs) (simp_all add: monom_0 monom_Suc)
+
 
 subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
 
@@ -924,6 +957,28 @@
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n) simp_all
 
+  
+subsection \<open>Conversions from natural numbers\<close>
+
+lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
+proof (induction n)
+  case (Suc n)
+  hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" 
+    by simp
+  also have "(of_nat n :: 'a poly) = [: of_nat n :]" 
+    by (subst Suc) (rule refl)
+  also have "1 = [:1:]" by (simp add: one_poly_def)
+  finally show ?case by (subst (asm) add_pCons) simp
+qed simp
+
+lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
+  by (simp add: of_nat_poly)
+
+lemma degree_numeral [simp]: "degree (numeral n) = 0"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+lemma numeral_poly: "numeral n = [:numeral n:]"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
 
 subsection \<open>Lemmas about divisibility\<close>
 
@@ -1787,6 +1842,9 @@
 apply (metis dvd_power dvd_trans order_1)
 done
 
+lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
+  by (subst (asm) order_root) auto
+
 
 subsection \<open>GCD of polynomials\<close>
 
@@ -1919,6 +1977,75 @@
   by (simp add: gcd_poly.simps)
 
 
+subsection \<open>Additional induction rules on polynomials\<close>
+
+text \<open>
+  An induction rule for induction over the roots of a polynomial with a certain property. 
+  (e.g. all positive roots)
+\<close>
+lemma poly_root_induct [case_names 0 no_roots root]:
+  fixes p :: "'a :: idom poly"
+  assumes "Q 0"
+  assumes "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
+  assumes "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
+  shows   "Q p"
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  case (less p)
+  show ?case
+  proof (cases "p = 0")
+    assume nz: "p \<noteq> 0"
+    show ?case
+    proof (cases "\<exists>a. P a \<and> poly p a = 0")
+      case False
+      thus ?thesis by (intro assms(2)) blast
+    next
+      case True
+      then obtain a where a: "P a" "poly p a = 0" 
+        by blast
+      hence "-[:-a, 1:] dvd p" 
+        by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
+      then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
+      with nz have q_nz: "q \<noteq> 0" by auto
+      have "degree p = Suc (degree q)"
+        by (subst q, subst degree_mult_eq) (simp_all add: q_nz)
+      hence "Q q" by (intro less) simp
+      from a(1) and this have "Q ([:a, -1:] * q)" 
+        by (rule assms(3))
+      with q show ?thesis by simp
+    qed
+  qed (simp add: assms(1))
+qed
+
+lemma dropWhile_replicate_append: 
+  "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys"
+  by (induction n) simp_all
+
+lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
+  by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
+
+text \<open>
+  An induction rule for simultaneous induction over two polynomials, 
+  prepending one coefficient in each step.
+\<close>
+lemma poly_induct2 [case_names 0 pCons]:
+  assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
+  shows   "P p q"
+proof -
+  def n \<equiv> "max (length (coeffs p)) (length (coeffs q))"
+  def xs \<equiv> "coeffs p @ (replicate (n - length (coeffs p)) 0)"
+  def ys \<equiv> "coeffs q @ (replicate (n - length (coeffs q)) 0)"
+  have "length xs = length ys" 
+    by (simp add: xs_def ys_def n_def)
+  hence "P (Poly xs) (Poly ys)" 
+    by (induction rule: list_induct2) (simp_all add: assms)
+  also have "Poly xs = p" 
+    by (simp add: xs_def Poly_append_replicate_0)
+  also have "Poly ys = q" 
+    by (simp add: ys_def Poly_append_replicate_0)
+  finally show ?thesis .
+qed
+
+
 subsection \<open>Composition of polynomials\<close>
 
 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
@@ -1945,6 +2072,212 @@
 apply (rule order_trans [OF degree_mult_le], simp)
 done
 
+lemma pcompose_add:
+  fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly"
+  shows "pcompose (p + q) r = pcompose p r + pcompose q r"
+proof (induction p q rule: poly_induct2)
+  case (pCons a p b q)
+  have "pcompose (pCons a p + pCons b q) r = 
+          [:a + b:] + r * pcompose p r + r * pcompose q r"
+    by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
+  also have "[:a + b:] = [:a:] + [:b:]" by simp
+  also have "\<dots> + r * pcompose p r + r * pcompose q r = 
+                 pcompose (pCons a p) r + pcompose (pCons b q) r"
+    by (simp only: pcompose_pCons add_ac)
+  finally show ?case .
+qed simp
+
+lemma pcompose_minus:
+  fixes p r :: "'a :: comm_ring poly"
+  shows "pcompose (-p) r = -pcompose p r"
+  by (induction p) (simp_all add: pcompose_pCons)
+
+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)
+
+lemma pcompose_smult:
+  fixes p r :: "'a :: comm_semiring_0 poly"
+  shows "pcompose (smult a p) r = smult a (pcompose p r)"
+  by (induction p) 
+     (simp_all add: pcompose_pCons pcompose_add smult_add_right)
+
+lemma pcompose_mult:
+  fixes p q r :: "'a :: comm_semiring_0 poly"
+  shows "pcompose (p * q) r = pcompose p r * pcompose q r"
+  by (induction p arbitrary: q)
+     (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
+
+lemma pcompose_assoc: 
+  "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) =
+     pcompose (pcompose p q) r"
+  by (induction p arbitrary: q) 
+     (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
+
+
+(* The remainder of this section and the next were contributed by Wenda Li *)
+
+lemma degree_mult_eq_0:
+  fixes p q:: "'a :: idom 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 degree_pcompose:
+  fixes p q:: "'a::idom poly"
+  shows "degree(pcompose p q) = degree p * degree q"
+proof (induct p)
+  case 0
+  thus ?case by auto
+next
+  case (pCons a p)
+  have "degree (q * pcompose p q) = 0 \<Longrightarrow> ?case" 
+    proof (cases "p=0")
+      case True
+      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)
+      moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0` 
+        proof -
+          assume "pcompose p q=0" "degree q\<noteq>0"
+          hence "degree p=0" using pCons.hyps(2) by auto
+          then obtain a1 where "p=[:a1:]"
+            by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
+          thus False using `pcompose p q=0` `p\<noteq>0` by auto
+        qed
+      ultimately have "degree (pCons a p) * degree q=0" by auto
+      moreover have "degree (pcompose (pCons a p) q) = 0" 
+        proof -
+          have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
+            using `degree (q * pcompose p q) = 0` by simp
+          also have "... \<ge> degree ([:a:] + q * pcompose p q)"
+            by (rule degree_add_le_max)
+          finally show ?thesis by (auto simp add:pcompose_pCons)
+        qed
+      ultimately show ?thesis by simp
+    qed
+  moreover have "degree (q * pcompose p q)>0 \<Longrightarrow> ?case" 
+    proof -
+      assume asm:"0 < degree (q * pcompose p q)"
+      hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto
+      have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"
+        unfolding pcompose_pCons
+        using degree_add_eq_right[of "[:a:]" ] asm by auto       
+      thus ?thesis 
+        using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
+    qed
+  ultimately show ?case by blast
+qed
+
+lemma pcompose_eq_0:
+  fixes p q:: "'a::idom 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:]" 
+    by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
+  hence "a=0" using assms(1) by auto
+  thus ?thesis using `p=[:a:]` by simp
+qed
+
+
+section{*lead coefficient*}
+
+definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
+  "lead_coeff p= coeff p (degree p)"
+
+lemma lead_coeff_pCons[simp]:
+    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
+    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
+unfolding lead_coeff_def by auto
+
+lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
+  unfolding lead_coeff_def by auto
+
+lemma lead_coeff_mult:
+   fixes p q::"'a ::idom poly"
+   shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
+by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
+
+lemma lead_coeff_add_le:
+  assumes "degree p < degree q"
+  shows "lead_coeff (p+q) = lead_coeff q" 
+using assms unfolding lead_coeff_def
+by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
+
+lemma lead_coeff_minus:
+  "lead_coeff (-p) = - lead_coeff p"
+by (metis coeff_minus degree_minus lead_coeff_def)
+
+
+lemma lead_coeff_comp:
+  fixes p q:: "'a::idom poly"
+  assumes "degree q > 0" 
+  shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
+proof (induct p)
+  case 0
+  thus ?case unfolding lead_coeff_def by auto
+next
+  case (pCons a p)
+  have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
+    proof -
+      assume "degree ( q * pcompose p q) = 0"
+      hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
+      hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp
+      thus ?thesis by auto
+    qed
+  moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
+    proof -
+      assume "degree ( q * pcompose p q) > 0"
+      hence "lead_coeff (pcompose (pCons a p) q) =lead_coeff ( q * pcompose p q)"
+        by (auto simp add:pcompose_pCons lead_coeff_add_le)
+      also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
+        using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
+      also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"
+        by auto
+      finally show ?thesis by auto
+    qed
+  ultimately show ?case by blast
+qed
+
+lemma lead_coeff_smult: 
+  "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"
+proof -
+  have "smult c p = [:c:] * p" by simp
+  also have "lead_coeff \<dots> = c * lead_coeff p" 
+    by (subst lead_coeff_mult) simp_all
+  finally show ?thesis .
+qed
+
+lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
+  by (simp add: lead_coeff_def)
+
+lemma lead_coeff_of_nat [simp]:
+  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
+  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
+
+lemma lead_coeff_numeral [simp]: 
+  "lead_coeff (numeral n) = numeral n"
+  unfolding lead_coeff_def
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+lemma lead_coeff_power: 
+  "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"
+  by (induction n) (simp_all add: lead_coeff_mult)
+
+lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
+  by (simp add: lead_coeff_def)
+  
+  
 
 no_notation cCons (infixr "##" 65)
 
diff -r b75764fc4c35 -r 1546a042e87b src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/List.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -3663,6 +3663,10 @@
   shows "remdups_adj (map f xs) = map f (remdups_adj xs)"
 by (induct xs rule: remdups_adj.induct) (auto simp add: injD[OF assms])
 
+lemma remdups_adj_replicate:
+  "remdups_adj (replicate n x) = (if n = 0 then [] else [x])"
+  by (induction n) (auto simp: remdups_adj_Cons)
+
 lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]"
 proof (cases "m \<le> n")
   case False then show ?thesis by simp
diff -r b75764fc4c35 -r 1546a042e87b src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -72,6 +72,9 @@
 lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})"
   unfolding harm_def by (intro setsum_nonneg) simp_all
 
+lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})"
+  unfolding harm_def by (intro setsum_pos) simp_all
+
 lemma of_real_harm: "of_real (harm n) = harm n"
   unfolding harm_def by simp
   
@@ -79,6 +82,7 @@
   by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
 
 lemma harm_expand: 
+  "harm 0 = 0"
   "harm (Suc 0) = 1"
   "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)"
 proof -
@@ -86,7 +90,7 @@
   also have "harm \<dots> = harm (pred_numeral n) + inverse (numeral n)"
     by (subst harm_Suc, subst numeral_eq_Suc[symmetric]) simp
   finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
-qed (simp add: harm_def)
+qed (simp_all add: harm_def)
 
 lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
 proof -
@@ -102,6 +106,32 @@
   finally show ?thesis by (blast dest: convergent_norm)
 qed
 
+lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0"
+  by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos)
+
+lemma ln_diff_le_inverse:
+  assumes "x \<ge> (1::real)"
+  shows   "ln (x + 1) - ln x < 1 / x"
+proof -
+  from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1) - ln x = (x + 1 - x) * inverse z"
+    by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps)
+  then obtain z where z: "z > x" "z < x + 1" "ln (x + 1) - ln x = inverse z" by auto
+  have "ln (x + 1) - ln x = inverse z" by fact
+  also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps)
+  finally show ?thesis .
+qed
+
+lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)"
+proof (induction n)
+  fix n assume IH: "ln (real n + 1) \<le> harm n"
+  have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2) - ln (real n + 1))" by simp
+  also have "(ln (real n + 2) - ln (real n + 1)) \<le> 1 / real (Suc n)"
+    using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac)
+  also note IH
+  also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps)
+  finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp
+qed (simp_all add: harm_def)
+
 
 subsection \<open>The Euler–Mascheroni constant\<close>