# HG changeset patch
# User huffman
# Date 1379003942 25200
# Node ID ea99a796417417ce34967a3e6c9ce11b49402941
# Parent  d29d63460d842216d4dd10904a9507f981a560a6
remove duplicate lemmas

diff -r d29d63460d84 -r ea99a7964174 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Sep 12 09:33:36 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Sep 12 09:39:02 2013 -0700
@@ -4123,11 +4123,8 @@
   apply rule
   done
 
-lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
-  by (rule neutral_add) (* FIXME: duplicate *)
-
 lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
-  unfolding monoidal_def neutral_monoid
+  unfolding monoidal_def neutral_add
   by (auto simp add: algebra_simps)
 
 lemma operative_integral:
@@ -4855,12 +4852,12 @@
 proof -
   have *: "setsum f s = setsum f (support op + f s)"
     apply (rule setsum_mono_zero_right)
-    unfolding support_def neutral_monoid
+    unfolding support_def neutral_add
     using assms
     apply auto
     done
   then show ?thesis unfolding * iterate_def fold'_def setsum.eq_fold
-    unfolding neutral_monoid by (simp add: comp_def)
+    unfolding neutral_add by (simp add: comp_def)
 qed
 
 lemma additive_content_division:
@@ -5399,7 +5396,6 @@
   apply (rule iterate_nonzero_image_lemma)
   apply (rule assms monoidal_monoid)+
   unfolding assms
-  using neutral_add
   unfolding neutral_add
   using assms
   apply auto
@@ -8506,7 +8502,7 @@
     thus ?thesis using integrable_integral unfolding g_def by auto }
 
   note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
-  note * = this[unfolded neutral_monoid]
+  note * = this[unfolded neutral_add]
   have iterate:"iterate (lifted op +) (p - {{c..d}})
       (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
   proof(rule *,rule) case goal1 hence "x\<in>p" by auto note div = division_ofD(2-5)[OF p(1) this]
@@ -9415,7 +9411,7 @@
   next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
   next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
   next case goal4 thus ?case apply-apply(rule tendsto_diff)
-      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
+      using LIMSEQ_ignore_initial_segment[OF assms(3)[rule_format],of x 1] by auto
   next case goal5 thus ?case using assms(4) unfolding bounded_iff
       apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
       apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
@@ -9423,7 +9419,7 @@
   note conjunctD2[OF this] note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
     integrable_add[OF this(1) assms(1)[rule_format,of 0]]
   thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
-    using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
+    using assms(1) apply auto by(rule LIMSEQ_imp_Suc) qed
 
 lemma monotone_convergence_decreasing: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
   assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<le> (f k x)"
diff -r d29d63460d84 -r ea99a7964174 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 12 09:33:36 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 12 09:39:02 2013 -0700
@@ -978,9 +978,6 @@
     unfolding th0 th1 by simp
 qed
 
-lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
-  by simp
-
 
 subsection{* Limit points *}
 
@@ -2125,32 +2122,20 @@
 
 text{* Some other lemmas about sequences. *}
 
-lemma sequentially_offset:
+lemma sequentially_offset: (* TODO: move to Topological_Spaces.thy *)
   assumes "eventually (\<lambda>i. P i) sequentially"
   shows "eventually (\<lambda>i. P (i + k)) sequentially"
-  using assms unfolding eventually_sequentially by (metis trans_le_add1)
-
-lemma seq_offset:
-  assumes "(f ---> l) sequentially"
-  shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
-  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
-
-lemma seq_offset_neg:
+  using assms by (rule eventually_sequentially_seg [THEN iffD2])
+
+lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *)
   "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
-  apply (rule topological_tendstoI)
-  apply (drule (2) topological_tendstoD)
-  apply (simp only: eventually_sequentially)
-  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n \<Longrightarrow> N <= n - k")
-  apply metis
+  apply (erule filterlim_compose)
+  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially)
   apply arith
   done
 
-lemma seq_offset_rev:
-  "((\<lambda>i. f(i + k)) ---> l) sequentially \<Longrightarrow> (f ---> l) sequentially"
-  by (rule LIMSEQ_offset) (* FIXME: redundant *)
-
 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
-  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
+  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *)
 
 subsection {* More properties of closed balls *}