generalize constant 'lim' and limit uniqueness theorems to class t2_space
authorhuffman
Sun Aug 14 10:25:43 2011 -0700 (2011-08-14)
changeset 4420518da2a87421c
parent 44195 f5363511b212
child 44206 5e4a1664106e
generalize constant 'lim' and limit uniqueness theorems to class t2_space
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Sun Aug 14 08:45:38 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 14 10:25:43 2011 -0700
     1.3 @@ -181,32 +181,32 @@
     1.4  lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
     1.5    by (rule tendsto_rabs_zero_iff)
     1.6  
     1.7 -lemma at_neq_bot:
     1.8 +lemma trivial_limit_at:
     1.9    fixes a :: "'a::real_normed_algebra_1"
    1.10 -  shows "at a \<noteq> bot"  -- {* TODO: find a more appropriate class *}
    1.11 -unfolding eventually_False [symmetric]
    1.12 +  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
    1.13 +unfolding trivial_limit_def
    1.14  unfolding eventually_at dist_norm
    1.15  by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
    1.16  
    1.17  lemma LIM_const_not_eq:
    1.18    fixes a :: "'a::real_normed_algebra_1"
    1.19 -  fixes k L :: "'b::metric_space"
    1.20 +  fixes k L :: "'b::t2_space"
    1.21    shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
    1.22 -by (simp add: tendsto_const_iff at_neq_bot)
    1.23 +by (simp add: tendsto_const_iff trivial_limit_at)
    1.24  
    1.25  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
    1.26  
    1.27  lemma LIM_const_eq:
    1.28    fixes a :: "'a::real_normed_algebra_1"
    1.29 -  fixes k L :: "'b::metric_space"
    1.30 +  fixes k L :: "'b::t2_space"
    1.31    shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
    1.32 -by (simp add: tendsto_const_iff at_neq_bot)
    1.33 +  by (simp add: tendsto_const_iff trivial_limit_at)
    1.34  
    1.35  lemma LIM_unique:
    1.36    fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
    1.37 -  fixes L M :: "'b::metric_space"
    1.38 +  fixes L M :: "'b::t2_space"
    1.39    shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
    1.40 -by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)
    1.41 +  using trivial_limit_at by (rule tendsto_unique)
    1.42  
    1.43  lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
    1.44  by (rule tendsto_ident_at)
     2.1 --- a/src/HOL/Limits.thy	Sun Aug 14 08:45:38 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Sun Aug 14 10:25:43 2011 -0700
     2.3 @@ -581,15 +581,37 @@
     2.4  lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
     2.5    by (simp add: tendsto_def)
     2.6  
     2.7 +lemma tendsto_unique:
     2.8 +  fixes f :: "'a \<Rightarrow> 'b::t2_space"
     2.9 +  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
    2.10 +  shows "a = b"
    2.11 +proof (rule ccontr)
    2.12 +  assume "a \<noteq> b"
    2.13 +  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
    2.14 +    using hausdorff [OF `a \<noteq> b`] by fast
    2.15 +  have "eventually (\<lambda>x. f x \<in> U) F"
    2.16 +    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
    2.17 +  moreover
    2.18 +  have "eventually (\<lambda>x. f x \<in> V) F"
    2.19 +    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
    2.20 +  ultimately
    2.21 +  have "eventually (\<lambda>x. False) F"
    2.22 +  proof (rule eventually_elim2)
    2.23 +    fix x
    2.24 +    assume "f x \<in> U" "f x \<in> V"
    2.25 +    hence "f x \<in> U \<inter> V" by simp
    2.26 +    with `U \<inter> V = {}` show "False" by simp
    2.27 +  qed
    2.28 +  with `\<not> trivial_limit F` show "False"
    2.29 +    by (simp add: trivial_limit_def)
    2.30 +qed
    2.31 +
    2.32  lemma tendsto_const_iff:
    2.33 -  fixes k l :: "'a::metric_space"
    2.34 -  assumes "F \<noteq> bot" shows "((\<lambda>n. k) ---> l) F \<longleftrightarrow> k = l"
    2.35 -  apply (safe intro!: tendsto_const)
    2.36 -  apply (rule ccontr)
    2.37 -  apply (drule_tac e="dist k l" in tendstoD)
    2.38 -  apply (simp add: zero_less_dist_iff)
    2.39 -  apply (simp add: eventually_False assms)
    2.40 -  done
    2.41 +  fixes a b :: "'a::t2_space"
    2.42 +  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
    2.43 +  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
    2.44 +
    2.45 +subsubsection {* Distance and norms *}
    2.46  
    2.47  lemma tendsto_dist [tendsto_intros]:
    2.48    assumes f: "(f ---> l) F" and g: "(g ---> m) F"
    2.49 @@ -611,8 +633,6 @@
    2.50    qed
    2.51  qed
    2.52  
    2.53 -subsubsection {* Norms *}
    2.54 -
    2.55  lemma norm_conv_dist: "norm x = dist x 0"
    2.56    unfolding dist_norm by simp
    2.57  
    2.58 @@ -865,31 +885,4 @@
    2.59    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
    2.60    unfolding sgn_div_norm by (simp add: tendsto_intros)
    2.61  
    2.62 -subsubsection {* Uniqueness *}
    2.63 -
    2.64 -lemma tendsto_unique:
    2.65 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
    2.66 -  assumes "\<not> trivial_limit F"  "(f ---> l) F"  "(f ---> l') F"
    2.67 -  shows "l = l'"
    2.68 -proof (rule ccontr)
    2.69 -  assume "l \<noteq> l'"
    2.70 -  obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
    2.71 -    using hausdorff [OF `l \<noteq> l'`] by fast
    2.72 -  have "eventually (\<lambda>x. f x \<in> U) F"
    2.73 -    using `(f ---> l) F` `open U` `l \<in> U` by (rule topological_tendstoD)
    2.74 -  moreover
    2.75 -  have "eventually (\<lambda>x. f x \<in> V) F"
    2.76 -    using `(f ---> l') F` `open V` `l' \<in> V` by (rule topological_tendstoD)
    2.77 -  ultimately
    2.78 -  have "eventually (\<lambda>x. False) F"
    2.79 -  proof (rule eventually_elim2)
    2.80 -    fix x
    2.81 -    assume "f x \<in> U" "f x \<in> V"
    2.82 -    hence "f x \<in> U \<inter> V" by simp
    2.83 -    with `U \<inter> V = {}` show "False" by simp
    2.84 -  qed
    2.85 -  with `\<not> trivial_limit F` show "False"
    2.86 -    by (simp add: trivial_limit_def)
    2.87 -qed
    2.88 -
    2.89  end
     3.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 08:45:38 2011 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
     3.3 @@ -189,7 +189,7 @@
     3.4    "X ----> L \<equiv> (X ---> L) sequentially"
     3.5  
     3.6  definition
     3.7 -  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
     3.8 +  lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
     3.9      --{*Standard definition of limit using choice operator*}
    3.10    "lim X = (THE L. X ----> L)"
    3.11  
    3.12 @@ -301,9 +301,9 @@
    3.13  by (rule tendsto_const)
    3.14  
    3.15  lemma LIMSEQ_const_iff:
    3.16 -  fixes k l :: "'a::metric_space"
    3.17 +  fixes k l :: "'a::t2_space"
    3.18    shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    3.19 -by (rule tendsto_const_iff, rule sequentially_bot)
    3.20 +  using trivial_limit_sequentially by (rule tendsto_const_iff)
    3.21  
    3.22  lemma LIMSEQ_norm:
    3.23    fixes a :: "'a::real_normed_vector"
    3.24 @@ -366,9 +366,9 @@
    3.25  by (rule tendsto_diff)
    3.26  
    3.27  lemma LIMSEQ_unique:
    3.28 -  fixes a b :: "'a::metric_space"
    3.29 +  fixes a b :: "'a::t2_space"
    3.30    shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    3.31 -by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
    3.32 +  using trivial_limit_sequentially by (rule tendsto_unique)
    3.33  
    3.34  lemma (in bounded_linear) LIMSEQ:
    3.35    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"