# HG changeset patch
# User huffman
# Date 1272345663 25200
# Node ID 89a70297564deae5505d01b9a12cda1f0a7d248f
# Parent  a65320184de97350e1df69993e3e6bfdb0981f38
simplify definition of continuous_on; generalize some lemmas

diff -r a65320184de9 -r 89a70297564d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 20:03:01 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 22:21:03 2010 -0700
@@ -3191,43 +3191,37 @@
     apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x="f xa" in allE) by (auto simp add: dist_commute dist_nz)
 qed
 
-text{* For setwise continuity, just start from the epsilon-delta definitions. *}
+text{* Define setwise continuity in terms of limits within the set. *}
 
 definition
   continuous_on ::
     "'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
 where
+  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+
+lemma continuous_on_topological:
   "continuous_on s f \<longleftrightarrow>
     (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
-      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>x'\<in>s. x' \<in> A \<longrightarrow> f x' \<in> B)))"
+      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_on_def tendsto_def
+unfolding Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
 
 lemma continuous_on_iff:
   "continuous_on s f \<longleftrightarrow>
-    (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d --> dist (f x') (f x) < e)"
-unfolding continuous_on_def
-apply safe
-apply (drule (1) bspec)
-apply (drule_tac x="ball (f x) e" in spec, simp, clarify)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec])
-apply (clarify, rename_tac d)
-apply (rule_tac x=d in exI, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (drule_tac x=x' in spec, simp add: dist_commute)
-apply (drule_tac x=x in bspec, assumption)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec], clarify)
-apply (drule_tac x=e in spec, simp, clarify)
-apply (rule_tac x="ball x d" in exI, simp, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (simp add: dist_commute)
+    (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+unfolding continuous_on_def Lim_within
+apply (intro ball_cong [OF refl] all_cong ex_cong)
+apply (rename_tac y, case_tac "y = x", simp)
+apply (simp add: dist_nz)
 done
 
 definition
   uniformly_continuous_on ::
-    "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+    "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
+where
   "uniformly_continuous_on s f \<longleftrightarrow>
-        (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
-                           --> dist (f x') (f x) < e)"
-
+    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
 
 text{* Some simple consequential lemmas. *}
 
@@ -3239,50 +3233,44 @@
  "continuous (at x) f ==> continuous (at x within s) f"
   unfolding continuous_within continuous_at using Lim_at_within by auto
 
+lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
+unfolding tendsto_def by (simp add: trivial_limit_eq)
+
 lemma continuous_at_imp_continuous_on:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  assumes "(\<forall>x \<in> s. continuous (at x) f)"
+  assumes "\<forall>x\<in>s. continuous (at x) f"
   shows "continuous_on s f"
-proof(simp add: continuous_at continuous_on_iff, rule, rule, rule)
-  fix x and e::real assume "x\<in>s" "e>0"
-  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
-  then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
-  { fix x' assume "\<not> 0 < dist x' x"
-    hence "x=x'"
-      using dist_nz[of x' x] by auto
-    hence "dist (f x') (f x) < e" using `e>0` by auto
-  }
-  thus "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using d by auto
+unfolding continuous_on_def
+proof
+  fix x assume "x \<in> s"
+  with assms have *: "(f ---> f (netlimit (at x))) (at x)"
+    unfolding continuous_def by simp
+  have "(f ---> f x) (at x)"
+  proof (cases "trivial_limit (at x)")
+    case True thus ?thesis
+      by (rule Lim_trivial_limit)
+  next
+    case False
+    hence "netlimit (at x) = x"
+      using netlimit_within [of x UNIV]
+      by (simp add: within_UNIV)
+    with * show ?thesis by simp
+  qed
+  thus "(f ---> f x) (at x within s)"
+    by (rule Lim_at_within)
 qed
 
 lemma continuous_on_eq_continuous_within:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
-    (is "?lhs = ?rhs")
-proof
-  assume ?rhs
-  { fix x assume "x\<in>s"
-    fix e::real assume "e>0"
-    assume "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
-    then obtain d where "d>0" and d:"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" by auto
-    { fix x' assume as:"x'\<in>s" "dist x' x < d"
-      hence "dist (f x') (f x) < e" using `e>0` d `x'\<in>s` dist_eq_0_iff[of x' x] zero_le_dist[of x' x] as(2) by (metis dist_eq_0_iff dist_nz) }
-    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by auto
-  }
-  thus ?lhs using `?rhs` unfolding continuous_on_iff continuous_within Lim_within by auto
-next
-  assume ?lhs
-  thus ?rhs unfolding continuous_on_iff continuous_within Lim_within by blast
-qed
-
-lemma continuous_on:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. (f ---> f(x)) (at x within s))"
-  by (auto simp add: continuous_on_eq_continuous_within continuous_within)
-  (* BH: maybe this should be the definition? *)
+  "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
+unfolding continuous_on_def continuous_def
+apply (rule ball_cong [OF refl])
+apply (case_tac "trivial_limit (at x within s)")
+apply (simp add: Lim_trivial_limit)
+apply (simp add: netlimit_within)
+done
+
+lemmas continuous_on = continuous_on_def -- "legacy theorem name"
 
 lemma continuous_on_eq_continuous_at:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
   by (auto simp add: continuous_on continuous_at Lim_within_open)
 
@@ -3292,22 +3280,19 @@
   unfolding continuous_within by(metis Lim_within_subset)
 
 lemma continuous_on_subset:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
   unfolding continuous_on by (metis subset_eq Lim_within_subset)
 
 lemma continuous_on_interior:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
 unfolding interior_def
 apply simp
 by (meson continuous_on_eq_continuous_at continuous_on_subset)
 
 lemma continuous_on_eq:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f
-           ==> continuous_on s g"
-  by (simp add: continuous_on_iff)
+  "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
+  unfolding continuous_on_def tendsto_def Limits.eventually_within
+  by simp
 
 text{* Characterization of various kinds of continuity in terms of sequences.  *}
 
@@ -3360,7 +3345,7 @@
   using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
 
 lemma continuous_on_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   shows "continuous_on s f \<longleftrightarrow>
     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
                     --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3418,7 +3403,7 @@
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
@@ -3434,7 +3419,7 @@
 qed
 
 lemma continuous_transform_at:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
@@ -3484,26 +3469,26 @@
   unfolding continuous_on_def by auto
 
 lemma continuous_on_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous_on s f ==>  continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
-  unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_neg:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
-  unfolding continuous_on_eq_continuous_within using continuous_neg by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_add:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g
            \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
-  unfolding continuous_on_eq_continuous_within using continuous_add by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_sub:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g
            \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
-  unfolding continuous_on_eq_continuous_within using continuous_sub by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 text{* Same thing for uniform continuity, using sequential formulations. *}
 
@@ -3569,7 +3554,7 @@
 
 lemma continuous_on_id:
  "continuous_on s (\<lambda>x. x)"
-  unfolding continuous_on_def by auto
+  unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
 
 lemma uniformly_continuous_on_id:
  "uniformly_continuous_on s (\<lambda>x. x)"
@@ -3604,10 +3589,8 @@
 qed
 
 lemma continuous_on_compose:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
-  unfolding continuous_on_eq_continuous_within using continuous_within_compose[of _ s f g] by auto
+  "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
+  unfolding continuous_on_topological by simp metis
 
 lemma uniformly_continuous_on_compose:
   assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"