--- a/src/HOL/Analysis/Gamma_Function.thy Fri Dec 25 11:44:18 2020 +0000
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Dec 25 15:37:27 2020 +0000
@@ -643,7 +643,8 @@
assumes "summable (\<lambda>n. f (n + k) :: 'a :: real_normed_vector)"
shows "summable f"
proof -
- from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))" by (simp add: summable_iff_convergent)
+ from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))"
+ using summable_iff_convergent by blast
hence "convergent (\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)))"
by (intro convergent_add convergent_const)
also have "(\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k))) = (\<lambda>m. \<Sum>n<m+k. f n)"
--- a/src/HOL/Analysis/Infinite_Products.thy Fri Dec 25 11:44:18 2020 +0000
+++ b/src/HOL/Analysis/Infinite_Products.thy Fri Dec 25 15:37:27 2020 +0000
@@ -175,8 +175,8 @@
lemma
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
assumes "convergent_prod f"
- shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"
- and convergent_prod_to_zero_iff: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"
+ shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"
+ and convergent_prod_to_zero_iff [simp]: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"
proof -
from assms obtain M L
where M: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" and "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0"
@@ -960,7 +960,7 @@
shows "prodinf f \<le> x"
by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)
-lemma prodinf_eq_one_iff:
+lemma prodinf_eq_one_iff [simp]:
fixes f :: "nat \<Rightarrow> real"
assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n"
shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)"
@@ -1227,7 +1227,7 @@
by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)
qed
-lemma convergent_prod_Suc_iff:
+lemma convergent_prod_Suc_iff [simp]:
shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
proof
assume "convergent_prod f"
@@ -1374,10 +1374,10 @@
fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
begin
-lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f"
+lemma convergent_prod_inverse_iff [simp]: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f"
by (auto dest: convergent_prod_inverse)
-lemma convergent_prod_const_iff:
+lemma convergent_prod_const_iff [simp]:
fixes c :: "'a :: {real_normed_field}"
shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1"
proof
@@ -1793,7 +1793,7 @@
obtains r where "q = of_real r"
using tendsto_eq_of_real_lim assms by blast
-lemma has_prod_of_real_iff:
+lemma has_prod_of_real_iff [simp]:
"(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"
(is "?lhs = ?rhs")
proof
--- a/src/HOL/Analysis/Lindelof_Spaces.thy Fri Dec 25 11:44:18 2020 +0000
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Fri Dec 25 15:37:27 2020 +0000
@@ -200,7 +200,7 @@
have UU_eq: "\<Union>\<U> = topspace X"
by (meson UU fin locally_finite_in_def subset_antisym)
obtain T where T: "\<And>x. x \<in> topspace X \<Longrightarrow> openin X (T x) \<and> x \<in> T x \<and> finite {U \<in> \<U>. U \<inter> T x \<noteq> {}}"
- using fin unfolding locally_finite_in_def by meson
+ using fin unfolding locally_finite_in_def by metis
then obtain I where "countable I" "I \<subseteq> topspace X" and I: "topspace X \<subseteq> \<Union>(T ` I)"
using X unfolding Lindelof_space_alt
by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image)
--- a/src/HOL/Series.thy Fri Dec 25 11:44:18 2020 +0000
+++ b/src/HOL/Series.thy Fri Dec 25 15:37:27 2020 +0000
@@ -432,7 +432,7 @@
shows "(\<lambda>i. f (i+n)) sums s \<longleftrightarrow> (\<lambda>i. f i) sums s"
by (simp add: assms sums_iff_shift)
-lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
+lemma summable_iff_shift [simp]: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
by (metis diff_add_cancel summable_def sums_iff_shift [abs_def])
lemma sums_split_initial_segment: "f sums s \<Longrightarrow> (\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i))"