# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1608910647 0
# Node ID 83b114a6545f8960e693a6b54510ec79b8a2ae83
# Parent  cf14976d4fdb7a00784bfb7e2bb8cdaf382f2897
A few more simprules for iff-reasoning

diff -r cf14976d4fdb -r 83b114a6545f src/HOL/Analysis/Gamma_Function.thy
--- 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)"
diff -r cf14976d4fdb -r 83b114a6545f src/HOL/Analysis/Infinite_Products.thy
--- 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
diff -r cf14976d4fdb -r 83b114a6545f src/HOL/Analysis/Lindelof_Spaces.thy
--- 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)
diff -r cf14976d4fdb -r 83b114a6545f src/HOL/Series.thy
--- 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))"