removed subseq_bigger (replaced by seq_suble)
authorhoelzl
Thu Jan 17 12:09:21 2013 +0100 (2013-01-17)
changeset 50937d249ef928ae1
parent 50936 b28f258ebc1a
child 50938 5b193d3dd6b6
removed subseq_bigger (replaced by seq_suble)
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:59:12 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:21 2013 +0100
     1.3 @@ -3016,26 +3016,10 @@
     1.4      using `l \<in> s` r l by blast
     1.5  qed
     1.6  
     1.7 -lemma subseq_bigger: assumes "subseq r" shows "n \<le> r n"
     1.8 -proof(induct n)
     1.9 -  show "0 \<le> r 0" by auto
    1.10 -next
    1.11 -  fix n assume "n \<le> r n"
    1.12 -  moreover have "r n < r (Suc n)"
    1.13 -    using assms [unfolded subseq_def] by auto
    1.14 -  ultimately show "Suc n \<le> r (Suc n)" by auto
    1.15 -qed
    1.16 -
    1.17 -lemma eventually_subseq:
    1.18 -  assumes r: "subseq r"
    1.19 -  shows "eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
    1.20 -unfolding eventually_sequentially
    1.21 -by (metis subseq_bigger [OF r] le_trans)
    1.22 -
    1.23  lemma lim_subseq:
    1.24    "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
    1.25  unfolding tendsto_def eventually_sequentially o_def
    1.26 -by (metis subseq_bigger le_trans)
    1.27 +by (metis seq_suble le_trans)
    1.28  
    1.29  lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
    1.30    unfolding Ex1_def
    1.31 @@ -3292,7 +3276,7 @@
    1.32    { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
    1.33      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
    1.34  
    1.35 -    note lr' = subseq_bigger [OF lr(2)]
    1.36 +    note lr' = seq_suble [OF lr(2)]
    1.37  
    1.38      { fix e::real assume "e>0"
    1.39        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
    1.40 @@ -3431,7 +3415,7 @@
    1.41    obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
    1.42    have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
    1.43      apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
    1.44 -    using subseq_bigger[OF r, of "N1 + N2"] by auto
    1.45 +    using seq_suble[OF r, of "N1 + N2"] by auto
    1.46  
    1.47    def x \<equiv> "(f (r (N1 + N2)))"
    1.48    have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
    1.49 @@ -3771,7 +3755,7 @@
    1.50        with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
    1.51        hence "dist ((x \<circ> r) (max N n)) l < e" by auto
    1.52        moreover
    1.53 -      have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto
    1.54 +      have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"] by auto
    1.55        hence "(x \<circ> r) (max N n) \<in> s n"
    1.56          using x apply(erule_tac x=n in allE)
    1.57          using x apply(erule_tac x="r (max N n)" in allE)
    1.58 @@ -6784,7 +6768,7 @@
    1.59        moreover
    1.60        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)"
    1.61          using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
    1.62 -        using subseq_bigger[OF r, of "Na+Nb+n"]
    1.63 +        using seq_suble[OF r, of "Na+Nb+n"]
    1.64          using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
    1.65        ultimately have False by simp
    1.66      }
     2.1 --- a/src/HOL/SEQ.thy	Thu Jan 17 11:59:12 2013 +0100
     2.2 +++ b/src/HOL/SEQ.thy	Thu Jan 17 12:09:21 2013 +0100
     2.3 @@ -171,8 +171,12 @@
     2.4    thus ?case by arith
     2.5  qed
     2.6  
     2.7 +lemma eventually_subseq:
     2.8 +  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
     2.9 +  unfolding eventually_sequentially by (metis seq_suble le_trans)
    2.10 +
    2.11  lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
    2.12 -  unfolding filterlim_iff eventually_sequentially by (metis le_trans seq_suble)
    2.13 +  unfolding filterlim_iff by (metis eventually_subseq)
    2.14  
    2.15  lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
    2.16    unfolding subseq_def by simp