--- a/src/HOL/Library/Poly_Deriv.thy Tue Jan 05 15:53:17 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy Tue Jan 05 17:54:21 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"
--- a/src/HOL/Library/Polynomial.thy Tue Jan 05 15:53:17 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Tue Jan 05 17:54:21 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)
--- a/src/HOL/List.thy Tue Jan 05 15:53:17 2016 +0100
+++ b/src/HOL/List.thy Tue Jan 05 17:54:21 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
--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy Tue Jan 05 15:53:17 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy Tue Jan 05 17:54:21 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>