add lemmas within_empty and tendsto_bot;
authorhuffman
Tue Sep 20 10:52:08 2011 -0700 (2011-09-20)
changeset 450319583f2b56f85
parent 45011 436ea69d5d37
child 45032 5a4d62f9e88d
add lemmas within_empty and tendsto_bot;
declare within_UNIV [simp];
tuned some proofs;
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Lim.thy	Tue Sep 20 15:23:17 2011 +0200
     1.2 +++ b/src/HOL/Lim.thy	Tue Sep 20 10:52:08 2011 -0700
     1.3 @@ -422,8 +422,7 @@
     1.4    assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
     1.5      eventually (\<lambda>n. P (f n)) sequentially"
     1.6    shows "eventually P (at a)"
     1.7 -  using assms sequentially_imp_eventually_within [where s=UNIV]
     1.8 -  unfolding within_UNIV by simp
     1.9 +  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
    1.10  
    1.11  lemma LIMSEQ_SEQ_conv1:
    1.12    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
     2.1 --- a/src/HOL/Limits.thy	Tue Sep 20 15:23:17 2011 +0200
     2.2 +++ b/src/HOL/Limits.thy	Tue Sep 20 10:52:08 2011 -0700
     2.3 @@ -298,7 +298,10 @@
     2.4    by (rule eventually_Abs_filter, rule is_filter.intro)
     2.5       (auto elim!: eventually_rev_mp)
     2.6  
     2.7 -lemma within_UNIV: "F within UNIV = F"
     2.8 +lemma within_UNIV [simp]: "F within UNIV = F"
     2.9 +  unfolding filter_eq_iff eventually_within by simp
    2.10 +
    2.11 +lemma within_empty [simp]: "F within {} = bot"
    2.12    unfolding filter_eq_iff eventually_within by simp
    2.13  
    2.14  lemma eventually_nhds:
    2.15 @@ -584,6 +587,9 @@
    2.16  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
    2.17    by (simp only: tendsto_iff Zfun_def dist_norm)
    2.18  
    2.19 +lemma tendsto_bot [simp]: "(f ---> a) bot"
    2.20 +  unfolding tendsto_def by simp
    2.21 +
    2.22  lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
    2.23    unfolding tendsto_def eventually_at_topological by auto
    2.24  
     3.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 20 15:23:17 2011 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 20 10:52:08 2011 -0700
     3.3 @@ -1913,7 +1913,7 @@
     3.4  
     3.5  lemma has_derivative_at_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
     3.6    "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
     3.7 -  using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV)
     3.8 +  using has_derivative_within_dest_vec1[where s=UNIV] by simp
     3.9  
    3.10  subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
    3.11  
     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 20 15:23:17 2011 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 20 10:52:08 2011 -0700
     4.3 @@ -62,7 +62,7 @@
     4.4  
     4.5  lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
     4.6           bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
     4.7 -  apply(subst within_UNIV[THEN sym]) unfolding has_derivative_within unfolding within_UNIV by auto
     4.8 +  using has_derivative_within [of f f' x UNIV] by simp
     4.9  
    4.10  text {* More explicit epsilon-delta forms. *}
    4.11  
    4.12 @@ -77,7 +77,7 @@
    4.13   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    4.14     (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm(x' - x) \<and> norm(x' - x) < d
    4.15          \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
    4.16 -  apply(subst within_UNIV[THEN sym]) unfolding has_derivative_within' by auto
    4.17 +  using has_derivative_within' [of f f' x UNIV] by simp
    4.18  
    4.19  lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
    4.20    unfolding has_derivative_within' has_derivative_at' by meson
    4.21 @@ -218,8 +218,7 @@
    4.22  lemma has_derivative_transform_at:
    4.23    assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x)"
    4.24    shows "(g has_derivative f') (at x)"
    4.25 -  apply(subst within_UNIV[THEN sym]) apply(rule has_derivative_transform_within[OF assms(1)])
    4.26 -  using assms(2-3) unfolding within_UNIV by auto
    4.27 +  using has_derivative_transform_within [of d x UNIV f g f'] assms by simp
    4.28  
    4.29  lemma has_derivative_transform_within_open:
    4.30    assumes "open s" "x \<in> s" "\<forall>y\<in>s. f y = g y" "(f has_derivative f') (at x)"
    4.31 @@ -386,7 +385,7 @@
    4.32  lemma has_derivative_at_alt:
    4.33    "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    4.34    (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))"
    4.35 -  using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto
    4.36 +  using has_derivative_within_alt[where s=UNIV] by simp
    4.37  
    4.38  subsection {* The chain rule. *}
    4.39  
    4.40 @@ -464,7 +463,7 @@
    4.41    "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
    4.42    using diff_chain_within[of f f' x UNIV g g']
    4.43    using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
    4.44 -  unfolding within_UNIV by auto
    4.45 +  by simp
    4.46  
    4.47  subsection {* Composition rules stated just for differentiability. *}
    4.48  
    4.49 @@ -1674,8 +1673,7 @@
    4.50    assumes "(g has_derivative g') (at x)"
    4.51    assumes "bounded_bilinear h"
    4.52    shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
    4.53 -  using has_derivative_bilinear_within[of f f' x UNIV g g' h]
    4.54 -  unfolding within_UNIV using assms by auto
    4.55 +  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
    4.56  
    4.57  subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
    4.58  
    4.59 @@ -1806,12 +1804,12 @@
    4.60    assumes "(g has_vector_derivative g') (at x)"
    4.61    assumes "bounded_bilinear h"
    4.62    shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
    4.63 -  apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto
    4.64 +  using has_vector_derivative_bilinear_within[where s=UNIV] assms by simp
    4.65  
    4.66  lemma has_vector_derivative_at_within:
    4.67    "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
    4.68    unfolding has_vector_derivative_def
    4.69 -  by (rule has_derivative_at_within) auto
    4.70 +  by (rule has_derivative_at_within)
    4.71  
    4.72  lemma has_vector_derivative_transform_within:
    4.73    assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
     5.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 15:23:17 2011 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 10:52:08 2011 -0700
     5.3 @@ -729,25 +729,25 @@
     5.4  lemma Liminf_within_UNIV:
     5.5    fixes f :: "'a::metric_space => ereal"
     5.6    shows "Liminf (at x) f = Liminf (at x within UNIV) f"
     5.7 -by (metis within_UNIV)
     5.8 +  by simp (* TODO: delete *)
     5.9  
    5.10  
    5.11  lemma Liminf_at:
    5.12    fixes f :: "'a::metric_space => ereal"
    5.13    shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
    5.14 -using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto
    5.15 +  using Liminf_within[of x UNIV f] by simp
    5.16  
    5.17  
    5.18  lemma Limsup_within_UNIV:
    5.19    fixes f :: "'a::metric_space => ereal"
    5.20    shows "Limsup (at x) f = Limsup (at x within UNIV) f"
    5.21 -by (metis within_UNIV)
    5.22 +  by simp (* TODO: delete *)
    5.23  
    5.24  
    5.25  lemma Limsup_at:
    5.26    fixes f :: "'a::metric_space => ereal"
    5.27    shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
    5.28 -using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto
    5.29 +  using Limsup_within[of x UNIV f] by simp
    5.30  
    5.31  lemma Lim_within_constant:
    5.32    fixes f :: "'a::metric_space => 'b::topological_space"
    5.33 @@ -1150,7 +1150,7 @@
    5.34    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
    5.35    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
    5.36    unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
    5.37 -  by (auto intro: complete_lattice_class.Sup_upper image_eqI)
    5.38 +  by (auto intro: complete_lattice_class.Sup_upper)
    5.39  
    5.40  lemma suminf_0_le:
    5.41    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 20 15:23:17 2011 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 20 10:52:08 2011 -0700
     6.3 @@ -842,8 +842,7 @@
     6.4  qed
     6.5  
     6.6  lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
     6.7 -  using trivial_limit_within [of a UNIV]
     6.8 -  by (simp add: within_UNIV)
     6.9 +  using trivial_limit_within [of a UNIV] by simp
    6.10  
    6.11  lemma trivial_limit_at:
    6.12    fixes a :: "'a::perfect_space"
    6.13 @@ -880,7 +879,7 @@
    6.14    by (auto elim: eventually_rev_mp)
    6.15  
    6.16  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
    6.17 -  unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
    6.18 +  by simp
    6.19  
    6.20  lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
    6.21    by (simp add: filter_eq_iff)
    6.22 @@ -1177,11 +1176,10 @@
    6.23  text{* These are special for limits out of the same vector space. *}
    6.24  
    6.25  lemma Lim_within_id: "(id ---> a) (at a within s)"
    6.26 -  unfolding tendsto_def Limits.eventually_within eventually_at_topological
    6.27 -  by auto
    6.28 +  unfolding id_def by (rule tendsto_ident_at_within)
    6.29  
    6.30  lemma Lim_at_id: "(id ---> a) (at a)"
    6.31 -apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
    6.32 +  unfolding id_def by (rule tendsto_ident_at)
    6.33  
    6.34  lemma Lim_at_zero:
    6.35    fixes a :: "'a::real_normed_vector"
    6.36 @@ -1210,9 +1208,7 @@
    6.37  lemma netlimit_at:
    6.38    fixes a :: "'a::{perfect_space,t2_space}"
    6.39    shows "netlimit (at a) = a"
    6.40 -  apply (subst within_UNIV[symmetric])
    6.41 -  using netlimit_within[of a UNIV]
    6.42 -  by (simp add: within_UNIV)
    6.43 +  using netlimit_within [of a UNIV] by simp
    6.44  
    6.45  lemma lim_within_interior:
    6.46    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
    6.47 @@ -1281,7 +1277,7 @@
    6.48    and fl: "(f ---> l) (at a)"
    6.49    shows "(g ---> l) (at a)"
    6.50    using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl
    6.51 -  by (auto simp add: within_UNIV)
    6.52 +  by simp
    6.53  
    6.54  text{* Alternatively, within an open set. *}
    6.55  
    6.56 @@ -3005,7 +3001,7 @@
    6.57    by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
    6.58  
    6.59  lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
    6.60 -  using continuous_within [of x UNIV f] by (simp add: within_UNIV)
    6.61 +  using continuous_within [of x UNIV f] by simp
    6.62  
    6.63  lemma continuous_at_within:
    6.64    assumes "continuous (at x) f"  shows "continuous (at x within s) f"
    6.65 @@ -3021,8 +3017,7 @@
    6.66  
    6.67  lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow>  (\<forall>e>0. \<exists>d>0.
    6.68                             \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
    6.69 -  using continuous_within_eps_delta[of x UNIV f]
    6.70 -  unfolding within_UNIV by blast
    6.71 +  using continuous_within_eps_delta [of x UNIV f] by simp
    6.72  
    6.73  text{* Versions in terms of open balls. *}
    6.74  
    6.75 @@ -3116,8 +3111,7 @@
    6.76    next
    6.77      case False
    6.78      hence 1: "netlimit (at x) = x"
    6.79 -      using netlimit_within [of x UNIV]
    6.80 -      by (simp add: within_UNIV)
    6.81 +      using netlimit_within [of x UNIV] by simp
    6.82      with * show ?thesis by simp
    6.83    qed
    6.84    thus "(f ---> f x) (at x within s)"
    6.85 @@ -3190,8 +3184,7 @@
    6.86    fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
    6.87    shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
    6.88                    --> ((f o x) ---> f a) sequentially)"
    6.89 -  using continuous_within_sequentially[of a UNIV f]
    6.90 -  unfolding within_UNIV by auto
    6.91 +  using continuous_within_sequentially[of a UNIV f] by simp
    6.92  
    6.93  lemma continuous_on_sequentially:
    6.94    fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
    6.95 @@ -3269,8 +3262,7 @@
    6.96    assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
    6.97            "continuous (at x) f"
    6.98    shows "continuous (at x) g"
    6.99 -  using continuous_transform_within [of d x UNIV f g] assms
   6.100 -  by (simp add: within_UNIV)
   6.101 +  using continuous_transform_within [of d x UNIV f g] assms by simp
   6.102  
   6.103  subsubsection {* Structural rules for pointwise continuity *}
   6.104  
   6.105 @@ -3523,11 +3515,13 @@
   6.106  using assms unfolding continuous_within_topological by simp metis
   6.107  
   6.108  lemma continuous_at_compose:
   6.109 -  assumes "continuous (at x) f"  "continuous (at (f x)) g"
   6.110 +  assumes "continuous (at x) f" and "continuous (at (f x)) g"
   6.111    shows "continuous (at x) (g o f)"
   6.112  proof-
   6.113 -  have " continuous (at (f x) within range f) g" using assms(2) using continuous_within_subset[of "f x" UNIV g "range f", unfolded within_UNIV] by auto
   6.114 -  thus ?thesis using assms(1) using continuous_within_compose[of x UNIV f g, unfolded within_UNIV] by auto
   6.115 +  have "continuous (at (f x) within range f) g" using assms(2)
   6.116 +    using continuous_within_subset[of "f x" UNIV g "range f"] by simp
   6.117 +  thus ?thesis using assms(1)
   6.118 +    using continuous_within_compose[of x UNIV f g] by simp
   6.119  qed
   6.120  
   6.121  lemma continuous_on_compose:
   6.122 @@ -3764,9 +3758,9 @@
   6.123  
   6.124  lemma continuous_at_avoid:
   6.125    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   6.126 -  assumes "continuous (at x) f"  "f x \<noteq> a"
   6.127 +  assumes "continuous (at x) f" and "f x \<noteq> a"
   6.128    shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
   6.129 -using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto
   6.130 +  using assms continuous_within_avoid[of x UNIV f a] by simp
   6.131  
   6.132  lemma continuous_on_avoid:
   6.133    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)