# HG changeset patch
# User hoelzl
# Date 1454957629 -3600
# Node ID 106569399cd60cfa1f4f8ecd54f0d3f63884d197
# Parent  d2bc8a7e5fec870af53b44039378a2b96eecb508
add type class for topological monoids

diff -r d2bc8a7e5fec -r 106569399cd6 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Limits.thy	Mon Feb 08 19:53:49 2016 +0100
@@ -573,28 +573,64 @@
   "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
   by (fold real_norm_def, rule tendsto_norm_zero_iff)
 
-subsubsection \<open>Addition and subtraction\<close>
+subsection \<open>Topological Monoid\<close>
+
+class topological_monoid_add = topological_space + monoid_add +
+  assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)"
+
+class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add
 
 lemma tendsto_add [tendsto_intros]:
-  fixes a b :: "'a::real_normed_vector"
-  shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
-  by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
+  fixes a b :: "'a::topological_monoid_add"
+  shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
+  using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F]
+  by (simp add: nhds_prod[symmetric] tendsto_Pair)
 
 lemma continuous_add [continuous_intros]:
-  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
   shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
   unfolding continuous_def by (rule tendsto_add)
 
 lemma continuous_on_add [continuous_intros]:
-  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
   unfolding continuous_on_def by (auto intro: tendsto_add)
 
 lemma tendsto_add_zero:
-  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
   shows "\<lbrakk>(f \<longlongrightarrow> 0) F; (g \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F"
   by (drule (1) tendsto_add, simp)
 
+lemma tendsto_setsum [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
+  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
+proof (cases "finite S")
+  assume "finite S" thus ?thesis using assms
+    by (induct, simp, simp add: tendsto_add)
+qed simp
+
+lemma continuous_setsum [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
+  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
+  unfolding continuous_def by (rule tendsto_setsum)
+
+lemma continuous_on_setsum [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add"
+  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
+  unfolding continuous_on_def by (auto intro: tendsto_setsum)
+
+subsubsection \<open>Addition and subtraction\<close>
+
+instance real_normed_vector < topological_comm_monoid_add
+proof
+  fix a b :: 'a show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
+    unfolding tendsto_Zfun_iff add_diff_add
+    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
+    by (intro Zfun_add)
+       (auto simp add: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
+qed
+
 lemma tendsto_minus [tendsto_intros]:
   fixes a :: "'a::real_normed_vector"
   shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> - a) F"
@@ -638,25 +674,6 @@
 lemma continuous_on_op_minus: "continuous_on (s::'a::real_normed_vector set) (op - x)"
   by (rule continuous_intros | simp)+
 
-lemma tendsto_setsum [tendsto_intros]:
-  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
-  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
-  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
-proof (cases "finite S")
-  assume "finite S" thus ?thesis using assms
-    by (induct, simp, simp add: tendsto_add)
-qed simp
-
-lemma continuous_setsum [continuous_intros]:
-  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
-  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
-  unfolding continuous_def by (rule tendsto_setsum)
-
-lemma continuous_on_setsum [continuous_intros]:
-  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
-  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
-  unfolding continuous_on_def by (auto intro: tendsto_setsum)
-
 lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
 
 subsubsection \<open>Linear operators and multiplication\<close>
@@ -1468,7 +1485,7 @@
 
 subsection \<open>Limits of Sequences\<close>
 
-lemma [trans]: "X=Y ==> Y \<longlonglongrightarrow> z ==> X \<longlonglongrightarrow> z"
+lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"
   by simp
 
 lemma LIMSEQ_iff:
@@ -2042,7 +2059,7 @@
   by (fact continuous_rabs)
 
 lemma isCont_add [simp]:
-  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::topological_monoid_add"
   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   by (fact continuous_add)
 
@@ -2081,7 +2098,7 @@
   by (fact continuous_power)
 
 lemma isCont_setsum [simp]:
-  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
+  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   by (auto intro: continuous_setsum)
 
@@ -2401,4 +2418,3 @@
   using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
 
 end
-
diff -r d2bc8a7e5fec -r 106569399cd6 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 08 19:53:49 2016 +0100
@@ -2143,4 +2143,3 @@
 qed
 
 end
-
diff -r d2bc8a7e5fec -r 106569399cd6 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Series.thy	Mon Feb 08 19:53:49 2016 +0100
@@ -271,12 +271,59 @@
       by (auto intro: le_less_trans simp: eventually_sequentially) }
 qed
 
+subsection \<open>Infinite summability on topological monoids\<close>
+
+lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
+  by auto
+
+context
+  fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
+begin
+
+lemma sums_Suc:
+  assumes "(\<lambda>n. f (Suc n)) sums l" shows "f sums (l + f 0)"
+proof  -
+  have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
+    using assms by (auto intro!: tendsto_add simp: sums_def)
+  moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
+    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
+  ultimately show ?thesis
+    by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
+qed
+
+lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
+  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
+
+lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
+  unfolding summable_def by (auto intro: sums_add)
+
+lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
+  by (intro sums_unique sums_add summable_sums)
+
+end
+
+context
+  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space, topological_comm_monoid_add}" and I :: "'i set"
+begin
+
+lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
+  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
+
+lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
+  using sums_unique[OF sums_setsum, OF summable_sums] by simp
+
+lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
+  using sums_summable[OF sums_setsum[OF summable_sums]] .
+
+end
 
 subsection \<open>Infinite summability on real normed vector spaces\<close>
 
-lemma sums_Suc_iff:
+context
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
-  shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
+begin
+
+lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
 proof -
   have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
     by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
@@ -292,7 +339,7 @@
   finally show ?thesis ..
 qed
 
-lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
+lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f"
 proof
   assume "summable f"
   hence "f sums suminf f" by (rule summable_sums)
@@ -300,19 +347,12 @@
   thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
 qed (auto simp: sums_Suc_iff summable_def)
 
+end
+
 context
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
 begin
 
-lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
-  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
-
-lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
-  unfolding summable_def by (auto intro: sums_add)
-
-lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
-  by (intro sums_unique sums_add summable_sums)
-
 lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)"
   unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
 
@@ -331,9 +371,6 @@
 lemma suminf_minus: "summable f \<Longrightarrow> (\<Sum>n. - f n) = - (\<Sum>n. f n)"
   by (intro sums_unique [symmetric] sums_minus summable_sums)
 
-lemma sums_Suc: "(\<lambda> n. f (Suc n)) sums l \<Longrightarrow> f sums (l + f 0)"
-  by (simp add: sums_Suc_iff)
-
 lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))"
 proof (induct n arbitrary: s)
   case (Suc n)
@@ -381,12 +418,10 @@
   apply (drule_tac x="n" in spec, simp)
   done
 
-lemma summable_imp_convergent:
-  "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
+lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
   by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
 
-lemma summable_imp_Bseq:
-  "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f"
   by (simp add: convergent_imp_Bseq summable_imp_convergent)
 
 end
@@ -396,22 +431,6 @@
   shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
   by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
 
-
-context
-  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
-begin
-
-lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
-  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
-
-lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
-  using sums_unique[OF sums_setsum, OF summable_sums] by simp
-
-lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
-  using sums_summable[OF sums_setsum[OF summable_sums]] .
-
-end
-
 lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   unfolding sums_def by (drule tendsto, simp only: setsum)
 
@@ -923,7 +942,7 @@
    fixes f :: "nat \<Rightarrow> real"
    assumes "summable f"
    and "inj g"
-   and pos: "!!x. 0 \<le> f x"
+   and pos: "\<And>x. 0 \<le> f x"
    shows summable_reindex: "summable (f o g)"
    and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
    and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"