# HG changeset patch
# User hoelzl
# Date 1358420961 -3600
# Node ID d249ef928ae10bd88091f0c31632746e06ae5484
# Parent  b28f258ebc1aecd83e9b84aa64e8110db8f09992
removed subseq_bigger (replaced by seq_suble)

diff -r b28f258ebc1a -r d249ef928ae1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:59:12 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:21 2013 +0100
@@ -3016,26 +3016,10 @@
     using `l \<in> s` r l by blast
 qed
 
-lemma subseq_bigger: assumes "subseq r" shows "n \<le> r n"
-proof(induct n)
-  show "0 \<le> r 0" by auto
-next
-  fix n assume "n \<le> r n"
-  moreover have "r n < r (Suc n)"
-    using assms [unfolded subseq_def] by auto
-  ultimately show "Suc n \<le> r (Suc n)" by auto
-qed
-
-lemma eventually_subseq:
-  assumes r: "subseq r"
-  shows "eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
-unfolding eventually_sequentially
-by (metis subseq_bigger [OF r] le_trans)
-
 lemma lim_subseq:
   "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
 unfolding tendsto_def eventually_sequentially o_def
-by (metis subseq_bigger le_trans)
+by (metis seq_suble le_trans)
 
 lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   unfolding Ex1_def
@@ -3292,7 +3276,7 @@
   { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
     from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
 
-    note lr' = subseq_bigger [OF lr(2)]
+    note lr' = seq_suble [OF lr(2)]
 
     { fix e::real assume "e>0"
       from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
@@ -3431,7 +3415,7 @@
   obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
   have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
     apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
-    using subseq_bigger[OF r, of "N1 + N2"] by auto
+    using seq_suble[OF r, of "N1 + N2"] by auto
 
   def x \<equiv> "(f (r (N1 + N2)))"
   have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
@@ -3771,7 +3755,7 @@
       with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
       hence "dist ((x \<circ> r) (max N n)) l < e" by auto
       moreover
-      have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto
+      have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"] by auto
       hence "(x \<circ> r) (max N n) \<in> s n"
         using x apply(erule_tac x=n in allE)
         using x apply(erule_tac x="r (max N n)" in allE)
@@ -6784,7 +6768,7 @@
       moreover
       have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
         using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
-        using subseq_bigger[OF r, of "Na+Nb+n"]
+        using seq_suble[OF r, of "Na+Nb+n"]
         using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
       ultimately have False by simp
     }
diff -r b28f258ebc1a -r d249ef928ae1 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu Jan 17 11:59:12 2013 +0100
+++ b/src/HOL/SEQ.thy	Thu Jan 17 12:09:21 2013 +0100
@@ -171,8 +171,12 @@
   thus ?case by arith
 qed
 
+lemma eventually_subseq:
+  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
+  unfolding eventually_sequentially by (metis seq_suble le_trans)
+
 lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
-  unfolding filterlim_iff eventually_sequentially by (metis le_trans seq_suble)
+  unfolding filterlim_iff by (metis eventually_subseq)
 
 lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
   unfolding subseq_def by simp