src/HOL/SEQ.thy
changeset 36662 621122eeb138
parent 36660 1cc4ab4b7ff7
child 36663 f75b13ed4898
     1.1 --- a/src/HOL/SEQ.thy	Tue May 04 10:42:47 2010 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Tue May 04 13:08:56 2010 -0700
     1.3 @@ -14,7 +14,7 @@
     1.4  begin
     1.5  
     1.6  abbreviation
     1.7 -  LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
     1.8 +  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
     1.9      ("((_)/ ----> (_))" [60, 60] 60) where
    1.10    "X ----> L \<equiv> (X ---> L) sequentially"
    1.11  
    1.12 @@ -153,13 +153,10 @@
    1.13  lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
    1.14  by (rule tendsto_const)
    1.15  
    1.16 -lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    1.17 -apply (safe intro!: LIMSEQ_const)
    1.18 -apply (rule ccontr)
    1.19 -apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
    1.20 -apply (simp add: zero_less_dist_iff)
    1.21 -apply auto
    1.22 -done
    1.23 +lemma LIMSEQ_const_iff:
    1.24 +  fixes k l :: "'a::metric_space"
    1.25 +  shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    1.26 +by (rule tendsto_const_iff, rule sequentially_bot)
    1.27  
    1.28  lemma LIMSEQ_norm:
    1.29    fixes a :: "'a::real_normed_vector"
    1.30 @@ -168,8 +165,9 @@
    1.31  
    1.32  lemma LIMSEQ_ignore_initial_segment:
    1.33    "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
    1.34 -apply (rule metric_LIMSEQ_I)
    1.35 -apply (drule (1) metric_LIMSEQ_D)
    1.36 +apply (rule topological_tendstoI)
    1.37 +apply (drule (2) topological_tendstoD)
    1.38 +apply (simp only: eventually_sequentially)
    1.39  apply (erule exE, rename_tac N)
    1.40  apply (rule_tac x=N in exI)
    1.41  apply simp
    1.42 @@ -177,8 +175,9 @@
    1.43  
    1.44  lemma LIMSEQ_offset:
    1.45    "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
    1.46 -apply (rule metric_LIMSEQ_I)
    1.47 -apply (drule (1) metric_LIMSEQ_D)
    1.48 +apply (rule topological_tendstoI)
    1.49 +apply (drule (2) topological_tendstoD)
    1.50 +apply (simp only: eventually_sequentially)
    1.51  apply (erule exE, rename_tac N)
    1.52  apply (rule_tac x="N + k" in exI)
    1.53  apply clarify
    1.54 @@ -196,7 +195,7 @@
    1.55  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
    1.56  
    1.57  lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
    1.58 -  unfolding LIMSEQ_def
    1.59 +  unfolding tendsto_def eventually_sequentially
    1.60    by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    1.61  
    1.62  lemma LIMSEQ_add:
    1.63 @@ -219,7 +218,9 @@
    1.64    shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
    1.65  by (rule tendsto_diff)
    1.66  
    1.67 -lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    1.68 +lemma LIMSEQ_unique:
    1.69 +  fixes a b :: "'a::metric_space"
    1.70 +  shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    1.71  apply (rule ccontr)
    1.72  apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
    1.73  apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
    1.74 @@ -750,9 +751,10 @@
    1.75  
    1.76  lemma LIMSEQ_subseq_LIMSEQ:
    1.77    "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
    1.78 -apply (auto simp add: LIMSEQ_def) 
    1.79 -apply (drule_tac x=r in spec, clarify)  
    1.80 -apply (rule_tac x=no in exI, clarify) 
    1.81 +apply (rule topological_tendstoI)
    1.82 +apply (drule (2) topological_tendstoD)
    1.83 +apply (simp only: eventually_sequentially)
    1.84 +apply (clarify, rule_tac x=N in exI, clarsimp)
    1.85  apply (blast intro: seq_suble le_trans dest!: spec) 
    1.86  done
    1.87  
    1.88 @@ -836,12 +838,8 @@
    1.89  apply (blast dest: order_antisym)+
    1.90  done
    1.91  
    1.92 -text{* The best of both worlds: Easier to prove this result as a standard
    1.93 -   theorem and then use equivalence to "transfer" it into the
    1.94 -   equivalent nonstandard form if needed!*}
    1.95 -
    1.96  lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
    1.97 -apply (simp add: LIMSEQ_def)
    1.98 +unfolding tendsto_def eventually_sequentially
    1.99  apply (rule_tac x = "X m" in exI, safe)
   1.100  apply (rule_tac x = m in exI, safe)
   1.101  apply (drule spec, erule impE, auto)