simplify proof of LIMSEQ_unique
authorhuffman
Tue Nov 30 08:58:47 2010 -0800 (2010-11-30)
changeset 40811ab0a8cc7976a
parent 40810 142f890ceef6
child 40826 a3af470a55d2
simplify proof of LIMSEQ_unique
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/SEQ.thy	Tue Nov 30 08:35:04 2010 -0800
     1.2 +++ b/src/HOL/SEQ.thy	Tue Nov 30 08:58:47 2010 -0800
     1.3 @@ -221,15 +221,7 @@
     1.4  lemma LIMSEQ_unique:
     1.5    fixes a b :: "'a::metric_space"
     1.6    shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
     1.7 -apply (rule ccontr)
     1.8 -apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
     1.9 -apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
    1.10 -apply (clarify, rename_tac M N)
    1.11 -apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
    1.12 -apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
    1.13 -apply (erule le_less_trans, rule add_strict_mono, simp, simp)
    1.14 -apply (subst dist_commute, rule dist_triangle)
    1.15 -done
    1.16 +by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
    1.17  
    1.18  lemma (in bounded_linear) LIMSEQ:
    1.19    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"