--- a/CONTRIBUTORS Mon Nov 02 11:56:38 2015 +0100
+++ b/CONTRIBUTORS Mon Nov 02 16:17:09 2015 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
+ A large number of additional binomial identities.
+
* Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
Isar subgoal command for proof structure within unstructured proof
scripts.
--- a/src/HOL/Binomial.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Binomial.thy Mon Nov 02 16:17:09 2015 +0100
@@ -13,7 +13,7 @@
subsection \<open>Factorial\<close>
-fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)"
+fun (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
lemmas fact_Suc = fact.simps(2)
@@ -442,7 +442,7 @@
text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
-definition "pochhammer (a::'a::comm_semiring_1) n =
+definition (in comm_semiring_1) "pochhammer (a :: 'a) n =
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
@@ -621,6 +621,40 @@
"m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
using pochhammer_product'[of z m "n - m"] by simp
+lemma pochhammer_times_pochhammer_half:
+ fixes z :: "'a :: field_char_0"
+ shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
+proof (induction n)
+ case (Suc n)
+ def n' \<equiv> "Suc n"
+ have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
+ (pochhammer z n' * pochhammer (z + 1 / 2) n') *
+ ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")
+ by (simp_all add: pochhammer_rec' mult_ac)
+ also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
+ (is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult)
+ also note Suc[folded n'_def]
+ also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"
+ by (simp add: setprod_nat_ivl_Suc)
+ finally show ?case by (simp add: n'_def)
+qed (simp add: setprod_nat_ivl_Suc)
+
+lemma pochhammer_double:
+ fixes z :: "'a :: field_char_0"
+ shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
+proof (induction n)
+ case (Suc n)
+ have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
+ (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
+ by (simp add: pochhammer_rec' ac_simps of_nat_mult)
+ also note Suc
+ also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *
+ (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
+ of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
+ by (simp add: of_nat_mult field_simps pochhammer_rec')
+ finally show ?case .
+qed simp
+
lemma pochhammer_absorb_comp:
"((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
(is "?lhs = ?rhs")
@@ -633,7 +667,7 @@
subsection\<open>Generalized binomial coefficients\<close>
-definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
where "a gchoose n =
(if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
@@ -654,6 +688,15 @@
eq setprod.distrib[symmetric])
qed
+lemma gbinomial_pochhammer':
+ "(s :: 'a :: field_char_0) gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
+proof -
+ have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"
+ by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
+ also have "(-1 :: 'a)^n * (-1)^n = 1" by (subst power_add [symmetric]) simp
+ finally show ?thesis by simp
+qed
+
lemma binomial_gbinomial:
"of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof -
--- a/src/HOL/Complex.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Complex.thy Mon Nov 02 16:17:09 2015 +0100
@@ -166,6 +166,12 @@
lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
by (simp add: Im_divide sqr_conv_mult)
+
+lemma Re_divide_of_nat: "Re (z / of_nat n) = Re z / of_nat n"
+ by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc)
+
+lemma Im_divide_of_nat: "Im (z / of_nat n) = Im z / of_nat n"
+ by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc)
lemma of_real_Re [simp]:
"z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
--- a/src/HOL/Deriv.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Deriv.thy Mon Nov 02 16:17:09 2015 +0100
@@ -745,7 +745,7 @@
by (rule DERIV_continuous)
lemma DERIV_continuous_on:
- "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative D) (at x)) \<Longrightarrow> continuous_on s f"
+ "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x)) \<Longrightarrow> continuous_on s f"
by (metis DERIV_continuous continuous_at_imp_continuous_on)
lemma DERIV_mult':
--- a/src/HOL/Int.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Int.thy Mon Nov 02 16:17:09 2015 +0100
@@ -686,6 +686,9 @@
lemma Ints_1 [simp]: "1 \<in> \<int>"
using Ints_of_int [of "1"] by simp
+lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
+ by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
+
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
apply (auto simp add: Ints_def)
apply (rule range_eqI)
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Nov 02 16:17:09 2015 +0100
@@ -3115,7 +3115,7 @@
then show ?thesis by simp
qed
-lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
+lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
(is "?l = inverse ?r")
proof-
have th: "?r$0 \<noteq> 0" by simp
--- a/src/HOL/Limits.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Limits.thy Mon Nov 02 16:17:09 2015 +0100
@@ -1148,6 +1148,32 @@
qed
qed
+lemma tendsto_add_filterlim_at_infinity:
+ assumes "(f ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
+ assumes "filterlim g at_infinity F"
+ shows "filterlim (\<lambda>x. f x + g x) at_infinity F"
+proof (subst filterlim_at_infinity[OF order_refl], safe)
+ fix r :: real assume r: "r > 0"
+ from assms(1) have "((\<lambda>x. norm (f x)) ---> norm c) F" by (rule tendsto_norm)
+ hence "eventually (\<lambda>x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all
+ moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all
+ with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F"
+ unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all
+ ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F"
+ proof eventually_elim
+ fix x :: 'a assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 \<le> norm (g x)"
+ from A B have "r \<le> norm (g x) - norm (f x)" by simp
+ also have "norm (g x) - norm (f x) \<le> norm (g x + f x)" by (rule norm_diff_ineq)
+ finally show "r \<le> norm (f x + g x)" by (simp add: add_ac)
+ qed
+qed
+
+lemma tendsto_add_filterlim_at_infinity':
+ assumes "filterlim f at_infinity F"
+ assumes "(g ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
+ shows "filterlim (\<lambda>x. f x + g x) at_infinity F"
+ by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+
+
lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
unfolding filterlim_at
by (auto simp: eventually_at_top_dense)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 02 16:17:09 2015 +0100
@@ -3164,6 +3164,9 @@
unfolding bounded_any_center [where a=0]
by (simp add: dist_norm)
+lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
+ by (simp add: bounded_iff bdd_above_def)
+
lemma bounded_realI:
assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
shows "bounded s"
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Nov 02 16:17:09 2015 +0100
@@ -479,4 +479,22 @@
"uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
+
+
+lemma uniformly_convergent_add:
+ "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
+ uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
+ unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add)
+
+lemma uniformly_convergent_minus:
+ "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
+ uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
+ unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus)
+
+lemma uniformly_convergent_mult:
+ "uniformly_convergent_on A f \<Longrightarrow>
+ uniformly_convergent_on A (\<lambda>k x. c * f k x :: 'a :: {real_normed_algebra})"
+ unfolding uniformly_convergent_on_def
+ by (blast dest: bounded_linear_uniform_limit_intros(13))
+
end
\ No newline at end of file
--- a/src/HOL/Transcendental.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Transcendental.thy Mon Nov 02 16:17:09 2015 +0100
@@ -792,6 +792,29 @@
done
qed
+lemma termdiffs_strong_converges_everywhere:
+ fixes K x :: "'a::{real_normed_field,banach}"
+ assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)"
+ shows "((\<lambda>x. \<Sum>n. c n * x^n) has_field_derivative (\<Sum>n. diffs c n * x^n)) (at x)"
+ using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
+ by (force simp del: of_real_add)
+
+lemma isCont_powser:
+ fixes K x :: "'a::{real_normed_field,banach}"
+ assumes "summable (\<lambda>n. c n * K ^ n)"
+ assumes "norm x < norm K"
+ shows "isCont (\<lambda>x. \<Sum>n. c n * x^n) x"
+ using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont)
+
+lemmas isCont_powser' = isCont_o2[OF _ isCont_powser]
+
+lemma isCont_powser_converges_everywhere:
+ fixes K x :: "'a::{real_normed_field,banach}"
+ assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)"
+ shows "isCont (\<lambda>x. \<Sum>n. c n * x^n) x"
+ using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
+ by (force intro!: DERIV_isCont simp del: of_real_add)
+
lemma powser_limit_0:
fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
assumes s: "0 < s"