# HG changeset patch
# User huffman
# Date 1272336950 25200
# Node ID e76cb1d4663c5207b981e686c6f45a969274b9d9
# Parent  1c0f42fb92f1d2dd63931e81e0785fdee09225ef
reorganize subsection headings

diff -r 1c0f42fb92f1 -r e76cb1d4663c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 17:56:39 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 19:55:50 2010 -0700
@@ -250,8 +250,6 @@
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   by (simp add: expand_set_eq)
 
-subsection{* Topological properties of open balls *}
-
 lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
   "(a::real) - b < 0 \<longleftrightarrow> a < b"
   "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -965,7 +963,9 @@
   using frontier_complement frontier_subset_eq[of "- S"]
   unfolding open_closed by auto
 
-subsection{* Common nets and The "within" modifier for nets. *}
+subsection {* Nets and the ``eventually true'' quantifier *}
+
+text {* Common nets and The "within" modifier for nets. *}
 
 definition
   at_infinity :: "'a::real_normed_vector net" where
@@ -989,7 +989,7 @@
   then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
 qed auto
 
-subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
+text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
 
 definition
   trivial_limit :: "'a net \<Rightarrow> bool" where
@@ -1040,7 +1040,7 @@
 lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
   by (auto simp add: trivial_limit_def eventually_sequentially)
 
-subsection{* Some property holds "sufficiently close" to the limit point. *}
+text {* Some property holds "sufficiently close" to the limit point. *}
 
 lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
@@ -1096,7 +1096,7 @@
 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
   by (simp add: eventually_False)
 
-subsection{* Limits, defined as vacuously true when the limit is trivial. *}
+subsection {* Limits *}
 
   text{* Notation Lim to avoid collition with lim defined in analysis *}
 definition
@@ -1266,6 +1266,23 @@
   shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
   by (rule tendsto_diff)
 
+lemma Lim_mul:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes "(c ---> d) net"  "(f ---> l) net"
+  shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
+  using assms by (rule scaleR.tendsto)
+
+lemma Lim_inv:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "(f ---> l) (net::'a net)"  "l \<noteq> 0"
+  shows "((inverse o f) ---> inverse l) net"
+  unfolding o_def using assms by (rule tendsto_inverse)
+
+lemma Lim_vmul:
+  fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
+  by (intro tendsto_intros)
+
 lemma Lim_null:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
@@ -1441,6 +1458,8 @@
   unfolding tendsto_def Limits.eventually_within eventually_at_topological
   by auto
 
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
 lemma Lim_at_id: "(id ---> a) (at a)"
 apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
 
@@ -1673,7 +1692,7 @@
   thus ?thesis unfolding Lim_sequentially dist_norm by simp
 qed
 
-text{* More properties of closed balls. *}
+subsection {* More properties of closed balls. *}
 
 lemma closed_cball: "closed (cball x e)"
 unfolding cball_def closed_def
@@ -2156,7 +2175,9 @@
   apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   done
 
-subsection{* Compactness (the definition is the one based on convegent subsequences). *}
+subsection {* Equivalent versions of compactness *}
+
+subsubsection{* Sequential compactness *}
 
 definition
   compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
@@ -2390,7 +2411,7 @@
     using l r by fast
 qed
 
-subsection{* Completeness. *}
+subsubsection{* Completeness *}
 
 lemma cauchy_def:
   "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
@@ -2537,7 +2558,7 @@
   unfolding image_def
   by auto
 
-subsection{* Total boundedness. *}
+subsubsection{* Total boundedness *}
 
 fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
@@ -2570,7 +2591,9 @@
     using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
 qed
 
-subsection{* Heine-Borel theorem (following Burkill \& Burkill vol. 2) *}
+subsubsection{* Heine-Borel theorem *}
+
+text {* Following Burkill \& Burkill vol. 2. *}
 
 lemma heine_borel_lemma: fixes s::"'a::metric_space set"
   assumes "compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
@@ -2634,7 +2657,7 @@
   ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
 qed
 
-subsection{* Bolzano-Weierstrass property. *}
+subsubsection {* Bolzano-Weierstrass property *}
 
 lemma heine_borel_imp_bolzano_weierstrass:
   assumes "\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f) --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f'))"
@@ -2662,7 +2685,7 @@
   ultimately show False using g(2) using finite_subset by auto
 qed
 
-subsection{* Complete the chain of compactness variants. *}
+subsubsection {* Complete the chain of compactness variants *}
 
 primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_2 beyond 0 = beyond 0" |
@@ -3098,7 +3121,9 @@
   ultimately show ?thesis by auto
 qed
 
-subsection{* Define continuity over a net to take in restrictions of the set. *}
+subsection {* Continuity *}
+
+text {* Define continuity over a net to take in restrictions of the set. *}
 
 definition
   continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -3933,7 +3958,105 @@
   thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
 qed
 
-subsection {* Preservation of compactness and connectedness under continuous function.  *}
+text {* We can now extend limit compositions to consider the scalar multiplier.   *}
+
+lemma continuous_vmul:
+  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
+  unfolding continuous_def using Lim_vmul[of c] by auto
+
+lemma continuous_mul:
+  fixes c :: "'a::metric_space \<Rightarrow> real"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net c \<Longrightarrow> continuous net f
+             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
+  unfolding continuous_def by (intro tendsto_intros)
+
+lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
+
+lemma continuous_on_vmul:
+  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
+  unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
+
+lemma continuous_on_mul:
+  fixes c :: "'a::metric_space \<Rightarrow> real"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous_on s c \<Longrightarrow> continuous_on s f
+             ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
+  unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
+
+lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
+  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
+  continuous_on_mul continuous_on_vmul
+
+text{* And so we have continuity of inverse.                                     *}
+
+lemma continuous_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> real"
+  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
+           ==> continuous net (inverse o f)"
+  unfolding continuous_def using Lim_inv by auto
+
+lemma continuous_at_within_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+  assumes "continuous (at a within s) f" "f a \<noteq> 0"
+  shows "continuous (at a within s) (inverse o f)"
+  using assms unfolding continuous_within o_def
+  by (intro tendsto_intros)
+
+lemma continuous_at_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
+         ==> continuous (at a) (inverse o f) "
+  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
+
+text {* Topological properties of linear functions. *}
+
+lemma linear_lim_0:
+  assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
+proof-
+  interpret f: bounded_linear f by fact
+  have "(f ---> f 0) (at 0)"
+    using tendsto_ident_at by (rule f.tendsto)
+  thus ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
+  assumes "bounded_linear f"  shows "continuous (at a) f"
+  unfolding continuous_at using assms
+  apply (rule bounded_linear.tendsto)
+  apply (rule tendsto_ident_at)
+  done
+
+lemma linear_continuous_within:
+  shows "bounded_linear f ==> continuous (at x within s) f"
+  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
+
+lemma linear_continuous_on:
+  shows "bounded_linear f ==> continuous_on s f"
+  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+
+text{* Also bilinear functions, in composition form.                             *}
+
+lemma bilinear_continuous_at_compose:
+  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
+        ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
+
+lemma bilinear_continuous_within_compose:
+  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
+        ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
+
+lemma bilinear_continuous_on_compose:
+  fixes s :: "'a::metric_space set" (* TODO: generalize *)
+  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
+             ==> continuous_on s (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
+  using bilinear_continuous_within_compose[of _ s f g h] by auto
+
+text {* Preservation of compactness and connectedness under continuous function.  *}
 
 lemma compact_continuous_image:
   assumes "continuous_on s f"  "compact s"
@@ -4026,7 +4149,7 @@
   thus ?thesis unfolding continuous_on_closed by auto
 qed
 
-subsection{* A uniformly convergent limit of continuous functions is continuous.       *}
+text {* A uniformly convergent limit of continuous functions is continuous. *}
 
 lemma norm_triangle_lt:
   fixes x y :: "'a::real_normed_vector"
@@ -4056,51 +4179,6 @@
   thus ?thesis unfolding continuous_on_iff by auto
 qed
 
-subsection{* Topological properties of linear functions.                               *}
-
-lemma linear_lim_0:
-  assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
-proof-
-  interpret f: bounded_linear f by fact
-  have "(f ---> f 0) (at 0)"
-    using tendsto_ident_at by (rule f.tendsto)
-  thus ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
-  assumes "bounded_linear f"  shows "continuous (at a) f"
-  unfolding continuous_at using assms
-  apply (rule bounded_linear.tendsto)
-  apply (rule tendsto_ident_at)
-  done
-
-lemma linear_continuous_within:
-  shows "bounded_linear f ==> continuous (at x within s) f"
-  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
-  shows "bounded_linear f ==> continuous_on s f"
-  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
-text{* Also bilinear functions, in composition form.                             *}
-
-lemma bilinear_continuous_at_compose:
-  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
-        ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
-
-lemma bilinear_continuous_within_compose:
-  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
-        ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
-
-lemma bilinear_continuous_on_compose:
-  fixes s :: "'a::metric_space set" (* TODO: generalize *)
-  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
-             ==> continuous_on s (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
-  using bilinear_continuous_within_compose[of _ s f g h] by auto
-
 subsection{* Topological stuff lifted from and dropped to R                            *}
 
 
@@ -4256,79 +4334,7 @@
   thus ?thesis by fastsimp
 qed
 
-subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
-
-lemma Lim_mul:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes "(c ---> d) net"  "(f ---> l) net"
-  shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
-  using assms by (rule scaleR.tendsto)
-
-lemma Lim_vmul:
-  fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
-  by (intro tendsto_intros)
-
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
-lemma continuous_vmul:
-  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
-  unfolding continuous_def using Lim_vmul[of c] by auto
-
-lemma continuous_mul:
-  fixes c :: "'a::metric_space \<Rightarrow> real"
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net c \<Longrightarrow> continuous net f
-             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
-  unfolding continuous_def by (intro tendsto_intros)
-
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-
-lemma continuous_on_vmul:
-  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
-  unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
-  fixes c :: "'a::metric_space \<Rightarrow> real"
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous_on s c \<Longrightarrow> continuous_on s f
-             ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
-  unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
-  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
-  continuous_on_mul continuous_on_vmul
-
-text{* And so we have continuity of inverse.                                     *}
-
-lemma Lim_inv:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "(f ---> l) (net::'a net)"  "l \<noteq> 0"
-  shows "((inverse o f) ---> inverse l) net"
-  unfolding o_def using assms by (rule tendsto_inverse)
-
-lemma continuous_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
-           ==> continuous net (inverse o f)"
-  unfolding continuous_def using Lim_inv by auto
-
-lemma continuous_at_within_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  assumes "continuous (at a within s) f" "f a \<noteq> 0"
-  shows "continuous (at a within s) (inverse o f)"
-  using assms unfolding continuous_within o_def
-  by (intro tendsto_intros)
-
-lemma continuous_at_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
-         ==> continuous (at a) (inverse o f) "
-  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
-
-subsection{* Preservation properties for pasted sets.                                  *}
+subsection {* Pasted sets *}
 
 lemma bounded_pastecart:
   fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
@@ -5102,7 +5108,7 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-subsection{* Intervals in general, including infinite and mixtures of open and closed. *}
+subsection {* Intervals *}
 
 definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i)))  \<longrightarrow> x \<in> s)"
 
@@ -5265,7 +5271,7 @@
  "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s.  z$k = a)"
   using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
 
-subsection{* Basic homeomorphism definitions.                                          *}
+subsection {* Homeomorphisms *}
 
 definition "homeomorphism s t f g \<equiv>
      (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
@@ -5321,7 +5327,7 @@
 apply(erule_tac x="f x" in ballE) apply(erule_tac x="x" in ballE)
 apply auto apply(rule_tac x="f x" in bexI) by auto
 
-subsection{* Relatively weak hypotheses if a set is compact.                           *}
+text {* Relatively weak hypotheses if a set is compact. *}
 
 definition "inv_on f s = (\<lambda>x. SOME y. y\<in>s \<and> f y = x)"
 
@@ -5662,7 +5668,7 @@
   thus ?thesis using dim_subset[OF closure_subset, of s] by auto
 qed
 
-text{* Affine transformations of intervals.                                      *}
+subsection {* Affine transformations of intervals *}
 
 lemma affinity_inverses:
   assumes m0: "m \<noteq> (0::'a::field)"