# HG changeset patch
# User huffman
# Date 1316541128 25200
# Node ID 9583f2b56f85e50860a1f5c4877c701a9670dfad
# Parent  436ea69d5d379a7d840b4b67bf4c54e522d11f8f
add lemmas within_empty and tendsto_bot;
declare within_UNIV [simp];
tuned some proofs;

diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Lim.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -422,8 +422,7 @@
   assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
     eventually (\<lambda>n. P (f n)) sequentially"
   shows "eventually P (at a)"
-  using assms sequentially_imp_eventually_within [where s=UNIV]
-  unfolding within_UNIV by simp
+  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
 
 lemma LIMSEQ_SEQ_conv1:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Limits.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -298,7 +298,10 @@
   by (rule eventually_Abs_filter, rule is_filter.intro)
      (auto elim!: eventually_rev_mp)
 
-lemma within_UNIV: "F within UNIV = F"
+lemma within_UNIV [simp]: "F within UNIV = F"
+  unfolding filter_eq_iff eventually_within by simp
+
+lemma within_empty [simp]: "F within {} = bot"
   unfolding filter_eq_iff eventually_within by simp
 
 lemma eventually_nhds:
@@ -584,6 +587,9 @@
 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
   by (simp only: tendsto_iff Zfun_def dist_norm)
 
+lemma tendsto_bot [simp]: "(f ---> a) bot"
+  unfolding tendsto_def by simp
+
 lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
   unfolding tendsto_def eventually_at_topological by auto
 
diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -1913,7 +1913,7 @@
 
 lemma has_derivative_at_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
   "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
-  using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV)
+  using has_derivative_within_dest_vec1[where s=UNIV] by simp
 
 subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
 
diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -62,7 +62,7 @@
 
 lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
          bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
-  apply(subst within_UNIV[THEN sym]) unfolding has_derivative_within unfolding within_UNIV by auto
+  using has_derivative_within [of f f' x UNIV] by simp
 
 text {* More explicit epsilon-delta forms. *}
 
@@ -77,7 +77,7 @@
  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm(x' - x) \<and> norm(x' - x) < d
         \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
-  apply(subst within_UNIV[THEN sym]) unfolding has_derivative_within' by auto
+  using has_derivative_within' [of f f' x UNIV] by simp
 
 lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
   unfolding has_derivative_within' has_derivative_at' by meson
@@ -218,8 +218,7 @@
 lemma has_derivative_transform_at:
   assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x)"
   shows "(g has_derivative f') (at x)"
-  apply(subst within_UNIV[THEN sym]) apply(rule has_derivative_transform_within[OF assms(1)])
-  using assms(2-3) unfolding within_UNIV by auto
+  using has_derivative_transform_within [of d x UNIV f g f'] assms by simp
 
 lemma has_derivative_transform_within_open:
   assumes "open s" "x \<in> s" "\<forall>y\<in>s. f y = g y" "(f has_derivative f') (at x)"
@@ -386,7 +385,7 @@
 lemma has_derivative_at_alt:
   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
   (\<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))"
-  using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto
+  using has_derivative_within_alt[where s=UNIV] by simp
 
 subsection {* The chain rule. *}
 
@@ -464,7 +463,7 @@
   "(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)"
   using diff_chain_within[of f f' x UNIV g g']
   using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
-  unfolding within_UNIV by auto
+  by simp
 
 subsection {* Composition rules stated just for differentiability. *}
 
@@ -1674,8 +1673,7 @@
   assumes "(g has_derivative g') (at x)"
   assumes "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
-  using has_derivative_bilinear_within[of f f' x UNIV g g' h]
-  unfolding within_UNIV using assms by auto
+  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
 
 subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
 
@@ -1806,12 +1804,12 @@
   assumes "(g has_vector_derivative g') (at x)"
   assumes "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
-  apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto
+  using has_vector_derivative_bilinear_within[where s=UNIV] assms by simp
 
 lemma has_vector_derivative_at_within:
   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
   unfolding has_vector_derivative_def
-  by (rule has_derivative_at_within) auto
+  by (rule has_derivative_at_within)
 
 lemma has_vector_derivative_transform_within:
   assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -729,25 +729,25 @@
 lemma Liminf_within_UNIV:
   fixes f :: "'a::metric_space => ereal"
   shows "Liminf (at x) f = Liminf (at x within UNIV) f"
-by (metis within_UNIV)
+  by simp (* TODO: delete *)
 
 
 lemma Liminf_at:
   fixes f :: "'a::metric_space => ereal"
   shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
-using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto
+  using Liminf_within[of x UNIV f] by simp
 
 
 lemma Limsup_within_UNIV:
   fixes f :: "'a::metric_space => ereal"
   shows "Limsup (at x) f = Limsup (at x within UNIV) f"
-by (metis within_UNIV)
+  by simp (* TODO: delete *)
 
 
 lemma Limsup_at:
   fixes f :: "'a::metric_space => ereal"
   shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
-using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto
+  using Limsup_within[of x UNIV f] by simp
 
 lemma Lim_within_constant:
   fixes f :: "'a::metric_space => 'b::topological_space"
@@ -1150,7 +1150,7 @@
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
   unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
-  by (auto intro: complete_lattice_class.Sup_upper image_eqI)
+  by (auto intro: complete_lattice_class.Sup_upper)
 
 lemma suminf_0_le:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
diff -r 436ea69d5d37 -r 9583f2b56f85 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 20 10:52:08 2011 -0700
@@ -842,8 +842,7 @@
 qed
 
 lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
-  using trivial_limit_within [of a UNIV]
-  by (simp add: within_UNIV)
+  using trivial_limit_within [of a UNIV] by simp
 
 lemma trivial_limit_at:
   fixes a :: "'a::perfect_space"
@@ -880,7 +879,7 @@
   by (auto elim: eventually_rev_mp)
 
 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
-  unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
+  by simp
 
 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   by (simp add: filter_eq_iff)
@@ -1177,11 +1176,10 @@
 text{* These are special for limits out of the same vector space. *}
 
 lemma Lim_within_id: "(id ---> a) (at a within s)"
-  unfolding tendsto_def Limits.eventually_within eventually_at_topological
-  by auto
+  unfolding id_def by (rule tendsto_ident_at_within)
 
 lemma Lim_at_id: "(id ---> a) (at a)"
-apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
+  unfolding id_def by (rule tendsto_ident_at)
 
 lemma Lim_at_zero:
   fixes a :: "'a::real_normed_vector"
@@ -1210,9 +1208,7 @@
 lemma netlimit_at:
   fixes a :: "'a::{perfect_space,t2_space}"
   shows "netlimit (at a) = a"
-  apply (subst within_UNIV[symmetric])
-  using netlimit_within[of a UNIV]
-  by (simp add: within_UNIV)
+  using netlimit_within [of a UNIV] by simp
 
 lemma lim_within_interior:
   "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
@@ -1281,7 +1277,7 @@
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
   using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl
-  by (auto simp add: within_UNIV)
+  by simp
 
 text{* Alternatively, within an open set. *}
 
@@ -3005,7 +3001,7 @@
   by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
 
 lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
-  using continuous_within [of x UNIV f] by (simp add: within_UNIV)
+  using continuous_within [of x UNIV f] by simp
 
 lemma continuous_at_within:
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
@@ -3021,8 +3017,7 @@
 
 lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow>  (\<forall>e>0. \<exists>d>0.
                            \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
-  using continuous_within_eps_delta[of x UNIV f]
-  unfolding within_UNIV by blast
+  using continuous_within_eps_delta [of x UNIV f] by simp
 
 text{* Versions in terms of open balls. *}
 
@@ -3116,8 +3111,7 @@
   next
     case False
     hence 1: "netlimit (at x) = x"
-      using netlimit_within [of x UNIV]
-      by (simp add: within_UNIV)
+      using netlimit_within [of x UNIV] by simp
     with * show ?thesis by simp
   qed
   thus "(f ---> f x) (at x within s)"
@@ -3190,8 +3184,7 @@
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
                   --> ((f o x) ---> f a) sequentially)"
-  using continuous_within_sequentially[of a UNIV f]
-  unfolding within_UNIV by auto
+  using continuous_within_sequentially[of a UNIV f] by simp
 
 lemma continuous_on_sequentially:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
@@ -3269,8 +3262,7 @@
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
-  using continuous_transform_within [of d x UNIV f g] assms
-  by (simp add: within_UNIV)
+  using continuous_transform_within [of d x UNIV f g] assms by simp
 
 subsubsection {* Structural rules for pointwise continuity *}
 
@@ -3523,11 +3515,13 @@
 using assms unfolding continuous_within_topological by simp metis
 
 lemma continuous_at_compose:
-  assumes "continuous (at x) f"  "continuous (at (f x)) g"
+  assumes "continuous (at x) f" and "continuous (at (f x)) g"
   shows "continuous (at x) (g o f)"
 proof-
-  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
-  thus ?thesis using assms(1) using continuous_within_compose[of x UNIV f g, unfolded within_UNIV] by auto
+  have "continuous (at (f x) within range f) g" using assms(2)
+    using continuous_within_subset[of "f x" UNIV g "range f"] by simp
+  thus ?thesis using assms(1)
+    using continuous_within_compose[of x UNIV f g] by simp
 qed
 
 lemma continuous_on_compose:
@@ -3764,9 +3758,9 @@
 
 lemma continuous_at_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  assumes "continuous (at x) f"  "f x \<noteq> a"
+  assumes "continuous (at x) f" and "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
-using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto
+  using assms continuous_within_avoid[of x UNIV f a] by simp
 
 lemma continuous_on_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)