author paulson Fri, 25 Dec 2020 15:37:27 +0000 changeset 73245 83b114a6545f parent 73244 cf14976d4fdb child 73246 b60c4ba462d4
A few more simprules for iff-reasoning
 src/HOL/Analysis/Gamma_Function.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Infinite_Products.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Lindelof_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Series.thy file | annotate | diff | comparison | revisions
```--- 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)))"
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"