# HG changeset patch
# User huffman
# Date 1314380309 25200
# Node ID 002b431171154dfd4b0805895d3281601fab6050
# Parent  7abe4a59f75d1f50c8652211f4193ccfc82468af# Parent  f7259c9064ea546215dfd3ef1eb43d88ea042921
merged

diff -r f7259c9064ea -r 002b43117115 NEWS
--- a/NEWS	Fri Aug 26 22:53:04 2011 +0900
+++ b/NEWS	Fri Aug 26 10:38:29 2011 -0700
@@ -200,6 +200,38 @@
   tendsto_vector   ~> vec_tendstoI
   Cauchy_vector    ~> vec_CauchyI
 
+* Session Multivariate_Analysis: Several duplicate theorems have been
+removed, and other theorems have been renamed. INCOMPATIBILITY.
+
+  eventually_conjI ~> eventually_conj
+  eventually_and ~> eventually_conj_iff
+  eventually_false ~> eventually_False
+  Lim_ident_at ~> LIM_ident
+  Lim_const ~> tendsto_const
+  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
+  Lim_neg ~> tendsto_minus
+  Lim_add ~> tendsto_add
+  Lim_sub ~> tendsto_diff
+  Lim_mul ~> tendsto_scaleR
+  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
+  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
+  Lim_linear ~> bounded_linear.tendsto
+  Lim_component ~> tendsto_euclidean_component
+  Lim_component_cart ~> tendsto_vec_nth
+  Lim_inner ~> tendsto_inner [OF tendsto_const]
+  dot_lsum ~> inner_setsum_left
+  dot_rsum ~> inner_setsum_right
+  continuous_on_neg ~> continuous_on_minus
+  continuous_on_sub ~> continuous_on_diff
+  continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
+  continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
+  continuous_on_mul ~> continuous_on_scaleR
+  continuous_on_mul_real ~> continuous_on_mult
+  continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
+  subset_interior ~> interior_mono
+  subset_closure ~> closure_mono
+  closure_univ ~> closure_UNIV
+
 * Complex_Main: The locale interpretations for the bounded_linear and
 bounded_bilinear locales have been removed, in order to reduce the
 number of duplicate lemmas. Users must use the original names for
@@ -213,6 +245,16 @@
   mult_right.setsum ~> setsum_right_distrib
   mult_left.diff ~> left_diff_distrib
 
+* Complex_Main: Several redundant theorems about real numbers have
+been removed or generalized and renamed. INCOMPATIBILITY.
+
+  real_0_le_divide_iff ~> zero_le_divide_iff
+  realpow_two_disj ~> power2_eq_iff
+  real_squared_diff_one_factored ~> square_diff_one_factored
+  realpow_two_diff ~> square_diff_square_factored
+  exp_ln_eq ~> ln_unique
+  lemma_DERIV_subst ~> DERIV_cong
+
 
 *** Document preparation ***
 
diff -r f7259c9064ea -r 002b43117115 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/IsaMakefile	Fri Aug 26 10:38:29 2011 -0700
@@ -1175,6 +1175,7 @@
   Multivariate_Analysis/L2_Norm.thy					\
   Multivariate_Analysis/Linear_Algebra.thy				\
   Multivariate_Analysis/Multivariate_Analysis.thy			\
+  Multivariate_Analysis/Norm_Arith.thy					\
   Multivariate_Analysis/Operator_Norm.thy				\
   Multivariate_Analysis/Path_Connected.thy				\
   Multivariate_Analysis/ROOT.ML						\
diff -r f7259c9064ea -r 002b43117115 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Library/Extended_Real.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -2391,8 +2391,6 @@
   shows "limsup X \<le> limsup Y"
   using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
 
-declare trivial_limit_sequentially[simp]
-
 lemma
   fixes X :: "nat \<Rightarrow> ereal"
   shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
diff -r f7259c9064ea -r 002b43117115 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Lim.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -444,46 +444,51 @@
 
 subsection {* Relation of LIM and LIMSEQ *}
 
+lemma sequentially_imp_eventually_within:
+  fixes a :: "'a::metric_space"
+  assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+    eventually (\<lambda>n. P (f n)) sequentially"
+  shows "eventually P (at a within s)"
+proof (rule ccontr)
+  let ?I = "\<lambda>n. inverse (real (Suc n))"
+  def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+  assume "\<not> eventually P (at a within s)"
+  hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+    unfolding Limits.eventually_within Limits.eventually_at by fast
+  hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+  hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
+    unfolding F_def by (rule someI_ex)
+  hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
+    and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
+    by fast+
+  from LIMSEQ_inverse_real_of_nat have "F ----> a"
+    by (rule metric_tendsto_imp_tendsto,
+      simp add: dist_norm F2 less_imp_le)
+  hence "eventually (\<lambda>n. P (F n)) sequentially"
+    using assms F0 F1 by simp
+  thus "False" by (simp add: F3)
+qed
+
+lemma sequentially_imp_eventually_at:
+  fixes a :: "'a::metric_space"
+  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
+
 lemma LIMSEQ_SEQ_conv1:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes f: "f -- a --> l"
   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
 
-lemma LIMSEQ_SEQ_conv2_lemma:
-  fixes a :: "'a::metric_space"
-  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
-  shows "eventually P (at a)"
-proof (rule ccontr)
-  let ?I = "\<lambda>n. inverse (real (Suc n))"
-  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
-  assume "\<not> eventually P (at a)"
-  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
-    unfolding eventually_at by simp
-  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
-  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
-    by (rule someI_ex)
-  hence F1: "\<And>n. ?F n \<noteq> a"
-    and F2: "\<And>n. dist (?F n) a < ?I n"
-    and F3: "\<And>n. \<not> P (?F n)"
-    by fast+
-  have "?F ----> a"
-    using LIMSEQ_inverse_real_of_nat
-    by (rule metric_tendsto_imp_tendsto,
-      simp add: dist_norm F2 [THEN less_imp_le])
-  moreover have "\<forall>n. ?F n \<noteq> a"
-    by (rule allI) (rule F1)
-  ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
-    using assms by simp
-  thus "False" by (simp add: F3)
-qed
-
 lemma LIMSEQ_SEQ_conv2:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   shows "f -- a --> l"
   using assms unfolding tendsto_def [where l=l]
-  by (simp add: LIMSEQ_SEQ_conv2_lemma)
+  by (simp add: sequentially_imp_eventually_at)
 
 lemma LIMSEQ_SEQ_conv:
   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -792,7 +792,7 @@
  have "subspace ?P"
    by (auto simp add: subspace_def)
  ultimately show ?thesis
-   using x span_induct[of ?B ?P x] iS by blast
+   using x span_induct[of x ?B ?P] iS by blast
 qed
 
 lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
@@ -2001,8 +2001,4 @@
     apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
     apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
 
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
 end
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -229,12 +229,18 @@
   from g(1) gS giS gBC show ?thesis by blast
 qed
 
+lemma closure_bounded_linear_image:
+  assumes f: "bounded_linear f"
+  shows "f ` (closure S) \<subseteq> closure (f ` S)"
+  using linear_continuous_on [OF f] closed_closure closure_subset
+  by (rule image_closure_subset)
+
 lemma closure_linear_image:
 fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
 assumes "linear f"
 shows "f ` (closure S) <= closure (f ` S)"
-using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f] 
-linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
+  using assms unfolding linear_conv_bounded_linear
+  by (rule closure_bounded_linear_image)
 
 lemma closure_injective_linear_image:
 fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
@@ -254,23 +260,16 @@
 shows "closure (S <*> T) = closure S <*> closure T"
   by (rule closure_Times)
 
-lemma closure_scaleR:  (* TODO: generalize to real_normed_vector *)
-fixes S :: "('n::euclidean_space) set"
-shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
-proof-
-{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
-      linear_scaleR injective_scaleR by auto 
-}
-moreover
-{ assume zero: "c=0 & S ~= {}"
-  hence "closure S ~= {}" using closure_subset by auto
-  hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
-  moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
-  ultimately have ?thesis using zero by auto
-}
-moreover
-{ assume "S={}" hence ?thesis by auto }
-ultimately show ?thesis by blast
+lemma closure_scaleR:
+  fixes S :: "('a::real_normed_vector) set"
+  shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+proof
+  show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
+    using bounded_linear_scaleR_right
+    by (rule closure_bounded_linear_image)
+  show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
+    by (intro closure_minimal image_mono closure_subset
+      closed_scaling closed_closure)
 qed
 
 lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
@@ -859,9 +858,8 @@
 qed
 
 lemma cone_closure:
-fixes S :: "('m::euclidean_space) set"
-assumes "cone S"
-shows "cone (closure S)"
+  fixes S :: "('a::real_normed_vector) set"
+  assumes "cone S" shows "cone (closure S)"
 proof-
 { assume "S = {}" hence ?thesis by auto }
 moreover
@@ -2310,12 +2308,7 @@
 lemma closure_affine_hull:
   fixes S :: "('n::euclidean_space) set"
   shows "closure S <= affine hull S"
-proof-
-have "closure S <= closure (affine hull S)" using subset_closure by auto
-moreover have "closure (affine hull S) = affine hull S" 
-   using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
-ultimately show ?thesis by auto  
-qed
+  by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
 
 lemma closure_same_affine_hull:
   fixes S :: "('n::euclidean_space) set"
@@ -2580,6 +2573,37 @@
     done
 qed
 
+lemma finite_imp_compact_convex_hull:
+  fixes s :: "('a::real_normed_vector) set"
+  assumes "finite s" shows "compact (convex hull s)"
+proof (cases "s = {}")
+  case True thus ?thesis by simp
+next
+  case False with assms show ?thesis
+  proof (induct rule: finite_ne_induct)
+    case (singleton x) show ?case by simp
+  next
+    case (insert x A)
+    let ?f = "\<lambda>(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y"
+    let ?T = "{0..1::real} \<times> (convex hull A)"
+    have "continuous_on ?T ?f"
+      unfolding split_def continuous_on by (intro ballI tendsto_intros)
+    moreover have "compact ?T"
+      by (intro compact_Times compact_interval insert)
+    ultimately have "compact (?f ` ?T)"
+      by (rule compact_continuous_image)
+    also have "?f ` ?T = convex hull (insert x A)"
+      unfolding convex_hull_insert [OF `A \<noteq> {}`]
+      apply safe
+      apply (rule_tac x=a in exI, simp)
+      apply (rule_tac x="1 - a" in exI, simp)
+      apply fast
+      apply (rule_tac x="(u, b)" in image_eqI, simp_all)
+      done
+    finally show "compact (convex hull (insert x A))" .
+  qed
+qed
+
 lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
   assumes "compact s"  shows "compact(convex hull s)"
 proof(cases "s={}")
@@ -2654,11 +2678,6 @@
   qed
 qed
 
-lemma finite_imp_compact_convex_hull:
-  fixes s :: "('a::euclidean_space) set"
-  shows "finite s \<Longrightarrow> compact(convex hull s)"
-by (metis compact_convex_hull finite_imp_compact)
-
 subsection {* Extremal points of a simplex are some vertices. *}
 
 lemma dist_increases_online:
@@ -2738,7 +2757,7 @@
 qed (auto simp add: assms)
 
 lemma simplex_furthest_le:
-  fixes s :: "('a::euclidean_space) set"
+  fixes s :: "('a::real_inner) set"
   assumes "finite s" "s \<noteq> {}"
   shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
 proof-
@@ -2754,12 +2773,12 @@
 qed
 
 lemma simplex_furthest_le_exists:
-  fixes s :: "('a::euclidean_space) set"
+  fixes s :: "('a::real_inner) set"
   shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
   using simplex_furthest_le[of s] by (cases "s={}")auto
 
 lemma simplex_extremal_le:
-  fixes s :: "('a::euclidean_space) set"
+  fixes s :: "('a::real_inner) set"
   assumes "finite s" "s \<noteq> {}"
   shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
 proof-
@@ -2780,7 +2799,7 @@
 qed 
 
 lemma simplex_extremal_le_exists:
-  fixes s :: "('a::euclidean_space) set"
+  fixes s :: "('a::real_inner) set"
   shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
   \<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
   using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
@@ -3094,7 +3113,6 @@
 subsection {* Convexity of cone hulls *}
 
 lemma convex_cone_hull:
-fixes S :: "('m::euclidean_space) set"
 assumes "convex S"
 shows "convex (cone hull S)"
 proof-
@@ -3126,7 +3144,6 @@
 qed
 
 lemma cone_convex_hull:
-fixes S :: "('m::euclidean_space) set"
 assumes "cone S"
 shows "cone (convex hull S)"
 proof-
@@ -3453,22 +3470,27 @@
         ultimately show ?thesis using injpi by auto qed qed
   qed auto qed
 
-lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set"
-  assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
+lemma homeomorphic_convex_compact_lemma:
+  fixes s :: "('a::euclidean_space) set"
+  assumes "convex s" and "compact s" and "cball 0 1 \<subseteq> s"
   shows "s homeomorphic (cball (0::'a) 1)"
-  apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
-  fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
-  hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq
-    apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball)
-    unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
-    fix y assume "dist (u *\<^sub>R x) y < 1 - u"
-    hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
-      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
-      unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
-      apply (rule mult_left_le_imp_le[of "1 - u"])
-      unfolding mult_assoc[symmetric] using `u<1` by auto
-    thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
-      using as unfolding scaleR_scaleR by auto qed auto
+proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
+  fix x u assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+  have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball)
+  moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
+    unfolding centre_in_ball using `u < 1` by simp
+  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+  proof
+    fix y assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
+    hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball .
+    with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
+      by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
+    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
+    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
+      using `x \<in> s` `0 \<le> u` `u < 1` [THEN less_imp_le] by (rule mem_convex)
+    thus "y \<in> s" using `u < 1` by simp
+  qed
+  ultimately have "u *\<^sub>R x \<in> interior s" ..
   thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
 
 lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set"
@@ -3621,8 +3643,8 @@
   assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
   shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
   apply(subst neg_equal_iff_equal[THEN sym])
-  using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
-  by auto
+  using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
+  using assms using continuous_on_minus by auto
 
 lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -4042,7 +4064,7 @@
   then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
   def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
   have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
-  have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
+  have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
     unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
     by(auto simp add:field_simps norm_minus_commute)
   thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
@@ -4380,7 +4402,7 @@
 shows "closure(rel_interior S) = closure S"
 proof-
 have h1: "closure(rel_interior S) <= closure S" 
-   using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
+   using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
 { assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" 
     using rel_interior_convex_nonempty assms by auto
   { fix x assume x_def: "x : closure S"
@@ -4517,7 +4539,7 @@
 proof-
 have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
 moreover have "?B --> (closure S1 <= closure S2)" 
-     by (metis assms(1) convex_closure_rel_interior subset_closure)
+     by (metis assms(1) convex_closure_rel_interior closure_mono)
 moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
 ultimately show ?thesis by blast
 qed
@@ -4777,7 +4799,7 @@
   using convex_closure_rel_interior_inter assms by auto
 moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
     using rel_interior_inter_aux 
-          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
 ultimately show ?thesis using closure_inter[of I] by auto
 qed
 
@@ -4790,7 +4812,7 @@
   using convex_closure_rel_interior_inter assms by auto
 moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
     using rel_interior_inter_aux 
-          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
 ultimately show ?thesis using closure_inter[of I] by auto
 qed
 
@@ -4886,7 +4908,7 @@
 proof-
 have *: "S Int closure T = S" using assms by auto
 have "~(rel_interior S <= rel_frontier T)"
-     using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
+     using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
      closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" 
      using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
@@ -4911,8 +4933,8 @@
 also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto  
 also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto 
 finally have "closure (f ` S) = closure (f ` rel_interior S)"
-   using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
-         subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
+   using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
+         closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
 hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
    linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] 
    closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -785,7 +785,7 @@
   have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
     apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
     defer
-    apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+    apply(rule continuous_on_intros assms(2))+
   proof
     fix x assume x:"x \<in> {a<..<b}"
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
@@ -869,7 +869,7 @@
     unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
     by (auto simp add: algebra_simps)
   hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
-    apply(rule continuous_on_intros continuous_on_vmul)+
+    apply(rule continuous_on_intros)+
     unfolding continuous_on_eq_continuous_within
     apply(rule,rule differentiable_imp_continuous_within)
     unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -149,7 +149,7 @@
   assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
 proof -
   from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
-    by (simp add: euclidean_component_diff)
+    by simp
   then show "x = y"
     unfolding euclidean_component_def euclidean_all_zero by simp
 qed
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -44,7 +44,7 @@
   have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
     prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
     apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
-    apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+    apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
     apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
     show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
       show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -378,7 +378,7 @@
       interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
       interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
       \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
-  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
+  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
     using division_ofD(5)[OF assms(1) k1(2) k2(2)]
     using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
 
@@ -407,9 +407,9 @@
   show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
   show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
   { fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
-  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
+  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
       using assms(3) by blast } moreover
-  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
+  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
       using assms(3) by blast} ultimately
   show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
   fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
@@ -573,7 +573,7 @@
         show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
         show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
         have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
-          apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+          apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
 
 lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
   unfolding division_of_def by(metis bounded_Union bounded_interval) 
@@ -823,7 +823,7 @@
   fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
   show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
   fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
-  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
+  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
   show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
     apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
     using p1(3) p2(3) using xk xk' by auto qed 
@@ -842,7 +842,7 @@
   show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
   fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
   have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
-    using assms(3)[rule_format] subset_interior by blast
+    using assms(3)[rule_format] interior_mono by blast
   show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
     using assm(5)[OF i _ xk'(2)]  i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
 qed
@@ -1703,7 +1703,7 @@
           by(rule le_less_trans[OF norm_le_l1])
         hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
         thus False unfolding mem_Collect_eq using e x k by auto
-      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
+      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
       thus "content b *\<^sub>R f a = 0" by auto
     qed auto
     also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
@@ -2563,7 +2563,7 @@
         proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
           assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}"  "{m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}"
           have "({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
-          note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
+          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
           hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
           thus "content ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[THEN sym] .
         qed qed
@@ -3516,7 +3516,7 @@
             proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
-              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
               moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
                 unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
               ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
@@ -3528,7 +3528,7 @@
             proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
-              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
               moreover have " ((b + ?v)/2) \<in> {?v <..<  b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
               hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
@@ -4390,7 +4390,7 @@
     from this(2) guess u v apply-by(erule exE)+ note uv=this
     have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
     hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
-    note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+    note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
     thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
 
   hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
@@ -4403,7 +4403,7 @@
     have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
       using as unfolding r_def by auto
     have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
-      apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+      apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
     thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto 
   qed(insert qq, auto)
 
@@ -4462,6 +4462,61 @@
   proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
     show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
 
+subsection {* Geometric progression *}
+
+text {* FIXME: Should one or more of these theorems be moved to @{file
+"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+
+lemma sum_gp_basic:
+  fixes x :: "'a::ring_1"
+  shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+proof-
+  def y \<equiv> "1 - x"
+  have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
+    by (induct n, simp, simp add: algebra_simps)
+  thus ?thesis
+    unfolding y_def by simp
+qed
+
+lemma sum_gp_multiplied: assumes mn: "m <= n"
+  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+  (is "?lhs = ?rhs")
+proof-
+  let ?S = "{0..(n - m)}"
+  from mn have mn': "n - m \<ge> 0" by arith
+  let ?f = "op + m"
+  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
+  have f: "?f ` ?S = {m..n}"
+    using mn apply (auto simp add: image_iff Bex_def) by arith
+  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
+    by (rule ext, simp add: power_add power_mult)
+  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
+  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
+  then show ?thesis unfolding sum_gp_basic using mn
+    by (simp add: field_simps power_add[symmetric])
+qed
+
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
+   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
+                    else (x^ m - x^ (Suc n)) / (1 - x))"
+proof-
+  {assume nm: "n < m" hence ?thesis by simp}
+  moreover
+  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
+    {assume x: "x = 1"  hence ?thesis by simp}
+    moreover
+    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
+      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+    ultimately have ?thesis by metis
+  }
+  ultimately show ?thesis by metis
+qed
+
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
+  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+  unfolding sum_gp[of x m "m + n"] power_Suc
+  by (simp add: field_simps power_add)
+
 subsection {* monotone convergence (bounded interval first). *}
 
 lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -8,11 +8,6 @@
 imports
   Euclidean_Space
   "~~/src/HOL/Library/Infinite_Set"
-  L2_Norm
-  "~~/src/HOL/Library/Convex"
-  "~~/src/HOL/Library/Sum_of_Squares"
-uses
-  ("normarith.ML")
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -66,7 +61,7 @@
 *)
 
 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
-  by (simp add: setL2_def power2_eq_square)
+  by (simp add: power2_eq_square)
 
 lemma norm_cauchy_schwarz:
   shows "inner x y <= norm x * norm y"
@@ -154,111 +149,6 @@
   then show "x = y" by (simp)
 qed
 
-subsection{* General linear decision procedure for normed spaces. *}
-
-lemma norm_cmul_rule_thm:
-  fixes x :: "'a::real_normed_vector"
-  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
-  unfolding norm_scaleR
-  apply (erule mult_left_mono)
-  apply simp
-  done
-
-  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm:
-  fixes x1 x2 :: "'a::real_normed_vector"
-  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
-  by (rule order_trans [OF norm_triangle_ineq add_mono])
-
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
-  by (simp add: field_simps)
-
-lemma pth_1:
-  fixes x :: "'a::real_normed_vector"
-  shows "x == scaleR 1 x" by simp
-
-lemma pth_2:
-  fixes x :: "'a::real_normed_vector"
-  shows "x - y == x + -y" by (atomize (full)) simp
-
-lemma pth_3:
-  fixes x :: "'a::real_normed_vector"
-  shows "- x == scaleR (-1) x" by simp
-
-lemma pth_4:
-  fixes x :: "'a::real_normed_vector"
-  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
-
-lemma pth_5:
-  fixes x :: "'a::real_normed_vector"
-  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
-
-lemma pth_6:
-  fixes x :: "'a::real_normed_vector"
-  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
-  by (simp add: scaleR_right_distrib)
-
-lemma pth_7:
-  fixes x :: "'a::real_normed_vector"
-  shows "0 + x == x" and "x + 0 == x" by simp_all
-
-lemma pth_8:
-  fixes x :: "'a::real_normed_vector"
-  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
-  by (simp add: scaleR_left_distrib)
-
-lemma pth_9:
-  fixes x :: "'a::real_normed_vector" shows
-  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
-  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
-  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
-  by (simp_all add: algebra_simps)
-
-lemma pth_a:
-  fixes x :: "'a::real_normed_vector"
-  shows "scaleR 0 x + y == y" by simp
-
-lemma pth_b:
-  fixes x :: "'a::real_normed_vector" shows
-  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
-  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
-  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
-  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
-  by (simp_all add: algebra_simps)
-
-lemma pth_c:
-  fixes x :: "'a::real_normed_vector" shows
-  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
-  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
-  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
-  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
-  by (simp_all add: algebra_simps)
-
-lemma pth_d:
-  fixes x :: "'a::real_normed_vector"
-  shows "x + 0 == x" by simp
-
-lemma norm_imp_pos_and_ge:
-  fixes x :: "'a::real_normed_vector"
-  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
-  by atomize auto
-
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
-
-lemma norm_pths:
-  fixes x :: "'a::real_normed_vector" shows
-  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
-  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
-  using norm_ge_zero[of "x - y"] by auto
-
-use "normarith.ML"
-
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "prove simple linear statements about vector norms"
-
-
-text{* Hence more metric properties. *}
-
 lemma norm_triangle_half_r:
   shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
   using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
@@ -274,16 +164,6 @@
 lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
   by (metis basic_trans_rules(21) norm_triangle_ineq)
 
-lemma dist_triangle_add:
-  fixes x y x' y' :: "'a::real_normed_vector"
-  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-  by norm
-
-lemma dist_triangle_add_half:
-  fixes x x' y y' :: "'a::real_normed_vector"
-  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
-  by norm
-
 lemma setsum_clauses:
   shows "setsum f {} = 0"
   and "finite S \<Longrightarrow> setsum f (insert x S) =
@@ -311,12 +191,6 @@
   apply (rule setsum_mono_zero_right[OF fT fST])
   by (auto intro: setsum_0')
 
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
-  apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
-lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
-  apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
 proof
   assume "\<forall>x. x \<bullet> y = x \<bullet> z"
@@ -702,65 +576,6 @@
   then show ?thesis by blast
 qed
 
-subsection {* Geometric progression *}
-
-lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
-  (is "?lhs = ?rhs")
-proof-
-  {assume x1: "x = 1" hence ?thesis by simp}
-  moreover
-  {assume x1: "x\<noteq>1"
-    hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
-    from geometric_sum[OF x1, of "Suc n", unfolded x1']
-    have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
-      unfolding atLeastLessThanSuc_atLeastAtMost
-      using x1' apply (auto simp only: field_simps)
-      apply (simp add: field_simps)
-      done
-    then have ?thesis by (simp add: field_simps) }
-  ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_multiplied: assumes mn: "m <= n"
-  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
-  (is "?lhs = ?rhs")
-proof-
-  let ?S = "{0..(n - m)}"
-  from mn have mn': "n - m \<ge> 0" by arith
-  let ?f = "op + m"
-  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
-  have f: "?f ` ?S = {m..n}"
-    using mn apply (auto simp add: image_iff Bex_def) by arith
-  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
-    by (rule ext, simp add: power_add power_mult)
-  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
-  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
-  then show ?thesis unfolding sum_gp_basic using mn
-    by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
-   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
-                    else (x^ m - x^ (Suc n)) / (1 - x))"
-proof-
-  {assume nm: "n < m" hence ?thesis by simp}
-  moreover
-  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
-    {assume x: "x = 1"  hence ?thesis by simp}
-    moreover
-    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
-      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
-    ultimately have ?thesis by metis
-  }
-  ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
-  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
-  unfolding sum_gp[of x m "m + n"] power_Suc
-  by (simp add: field_simps power_add)
-
-
 subsection{* A bit of linear algebra. *}
 
 definition (in real_vector)
@@ -807,6 +622,9 @@
   apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
   done
 
+lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
+  by (auto simp add: subspace_def linear_def linear_0[of f])
+
 lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
   by (auto simp add: subspace_def linear_def linear_0[of f])
 
@@ -816,6 +634,11 @@
 lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
   by (simp add: subspace_def)
 
+lemma subspace_Times: "\<lbrakk>subspace A; subspace B\<rbrakk> \<Longrightarrow> subspace (A \<times> B)"
+  unfolding subspace_def zero_prod_def by simp
+
+text {* Properties of span. *}
+
 lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
   by (metis span_def hull_mono)
 
@@ -834,8 +657,16 @@
   by (metis span_def hull_subset subset_eq)
      (metis subspace_span subspace_def)+
 
-lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
-  and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
+lemma span_unique:
+  "\<lbrakk>S \<subseteq> T; subspace T; \<And>T'. \<lbrakk>S \<subseteq> T'; subspace T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk> \<Longrightarrow> span S = T"
+  unfolding span_def by (rule hull_unique)
+
+lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
+  unfolding span_def by (rule hull_minimal)
+
+lemma (in real_vector) span_induct:
+  assumes x: "x \<in> span S" and P: "subspace P" and SP: "\<And>x. x \<in> S ==> x \<in> P"
+  shows "x \<in> P"
 proof-
   from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
   from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
@@ -967,105 +798,76 @@
 
 text {* Mapping under linear image. *}
 
-lemma span_linear_image: assumes lf: "linear f"
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+  by auto (* TODO: move *)
+
+lemma span_linear_image:
+  assumes lf: "linear f"
   shows "span (f ` S) = f ` (span S)"
-proof-
-  {fix x
-    assume x: "x \<in> span (f ` S)"
-    have "x \<in> f ` span S"
-      apply (rule span_induct[where x=x and S = "f ` S"])
-      apply (clarsimp simp add: image_iff)
-      apply (frule span_superset)
-      apply blast
-      apply (rule subspace_linear_image[OF lf])
-      apply (rule subspace_span)
-      apply (rule x)
-      done}
-  moreover
-  {fix x assume x: "x \<in> span S"
-    have "x \<in> {x. f x \<in> span (f ` S)}"
-      apply (rule span_induct[where S=S])
-      apply simp
-      apply (rule span_superset)
-      apply simp
-      apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
-      apply (rule x)
-      done
-    hence "f x \<in> span (f ` S)" by simp
-  }
-  ultimately show ?thesis by blast
+proof (rule span_unique)
+  show "f ` S \<subseteq> f ` span S"
+    by (intro image_mono span_inc)
+  show "subspace (f ` span S)"
+    using lf subspace_span by (rule subspace_linear_image)
+next
+  fix T assume "f ` S \<subseteq> T" and "subspace T" thus "f ` span S \<subseteq> T"
+    unfolding image_subset_iff_subset_vimage
+    by (intro span_minimal subspace_linear_vimage lf)
+qed
+
+lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+proof (rule span_unique)
+  show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+    by safe (force intro: span_clauses)+
+next
+  have "linear (\<lambda>(a, b). a + b)"
+    by (simp add: linear_def scaleR_add_right)
+  moreover have "subspace (span A \<times> span B)"
+    by (intro subspace_Times subspace_span)
+  ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
+    by (rule subspace_linear_image)
+next
+  fix T assume "A \<union> B \<subseteq> T" and "subspace T"
+  thus "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
+    by (auto intro!: subspace_add elim: span_induct)
 qed
 
 text {* The key breakdown property. *}
 
+lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
+proof (rule span_unique)
+  show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
+    by (fast intro: scaleR_one [symmetric])
+  show "subspace (range (\<lambda>k. k *\<^sub>R x))"
+    unfolding subspace_def
+    by (auto intro: scaleR_add_left [symmetric])
+  fix T assume "{x} \<subseteq> T" and "subspace T" thus "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
+    unfolding subspace_def by auto
+qed
+
+lemma span_insert:
+  "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+proof -
+  have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+    unfolding span_union span_singleton
+    apply safe
+    apply (rule_tac x=k in exI, simp)
+    apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
+    apply simp
+    apply (rule right_minus)
+    done
+  thus ?thesis by simp
+qed
+
 lemma span_breakdown:
   assumes bS: "b \<in> S" and aS: "a \<in> span S"
-  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
-proof-
-  {fix x assume xS: "x \<in> S"
-    {assume ab: "x = b"
-      then have "?P x"
-        apply simp
-        apply (rule exI[where x="1"], simp)
-        by (rule span_0)}
-    moreover
-    {assume ab: "x \<noteq> b"
-      then have "?P x"  using xS
-        apply -
-        apply (rule exI[where x=0])
-        apply (rule span_superset)
-        by simp}
-    ultimately have "x \<in> Collect ?P" by blast}
-  moreover have "subspace (Collect ?P)"
-    unfolding subspace_def
-    apply auto
-    apply (rule exI[where x=0])
-    using span_0[of "S - {b}"]
-    apply simp
-    apply (rule_tac x="k + ka" in exI)
-    apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
-    apply (simp only: )
-    apply (rule span_add)
-    apply assumption+
-    apply (simp add: algebra_simps)
-    apply (rule_tac x= "c*k" in exI)
-    apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
-    apply (simp only: )
-    apply (rule span_mul)
-    apply assumption
-    by (simp add: algebra_simps)
-  ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
-  thus "?P a" by simp
-qed
+  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
+  using assms span_insert [of b "S - {b}"]
+  by (simp add: insert_absorb)
 
 lemma span_breakdown_eq:
-  "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume x: "x \<in> span (insert a S)"
-    from x span_breakdown[of "a" "insert a S" "x"]
-    have ?rhs apply clarsimp
-      apply (rule_tac x= "k" in exI)
-      apply (rule set_rev_mp[of _ "span (S - {a})" _])
-      apply assumption
-      apply (rule span_mono)
-      apply blast
-      done}
-  moreover
-  { fix k assume k: "x - k *\<^sub>R a \<in> span S"
-    have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
-    have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
-      apply (rule span_add)
-      apply (rule set_rev_mp[of _ "span S" _])
-      apply (rule k)
-      apply (rule span_mono)
-      apply blast
-      apply (rule span_mul)
-      apply (rule span_superset)
-      apply blast
-      done
-    then have ?lhs using eq by metis}
-  ultimately show ?thesis by blast
-qed
+  "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)"
+  by (simp add: span_insert)
 
 text {* Hence some "reversal" results. *}
 
@@ -1122,26 +924,16 @@
 
 text {* Transitivity property. *}
 
+lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
+  unfolding span_def by (rule hull_redundant)
+
 lemma span_trans:
   assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
   shows "y \<in> span S"
-proof-
-  from span_breakdown[of x "insert x S" y, OF insertI1 y]
-  obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
-  have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
-  show ?thesis
-    apply (subst eq)
-    apply (rule span_add)
-    apply (rule set_rev_mp)
-    apply (rule k)
-    apply (rule span_mono)
-    apply blast
-    apply (rule span_mul)
-    by (rule x)
-qed
+  using assms by (simp only: span_redundant)
 
 lemma span_insert_0[simp]: "span (insert 0 S) = span S"
-  using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)
+  by (simp only: span_redundant span_0)
 
 text {* An explicit expansion is sometimes needed. *}
 
@@ -1273,43 +1065,6 @@
   ultimately show ?thesis by blast
 qed
 
-lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
-
-lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
-proof safe
-  fix x assume "x \<in> span (A \<union> B)"
-  then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
-    unfolding span_explicit by auto
-
-  let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
-  let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
-  show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
-  proof
-    show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
-      unfolding x using S
-      by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
-
-    from S have "?Sa \<in> span A" unfolding span_explicit
-      by (auto intro!: exI[of _ "S \<inter> A"])
-    moreover from S have "?Sb \<in> span B" unfolding span_explicit
-      by (auto intro!: exI[of _ "S \<inter> (B - A)"])
-    ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
-  qed
-next
-  fix a b assume "a \<in> span A" and "b \<in> span B"
-  then obtain Sa ua Sb ub where span:
-    "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
-    "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
-    unfolding span_explicit by auto
-  let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
-  from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
-    and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
-    unfolding setsum_addf scaleR_left_distrib
-    by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
-  thus "a + b \<in> span (A \<union> B)"
-    unfolding span_explicit by (auto intro!: exI[of _ ?u])
-qed
-
 text {* This is useful for building a basis step-by-step. *}
 
 lemma independent_insert:
@@ -1495,30 +1250,6 @@
   apply (simp add: inner_setsum_right dot_basis)
   done
 
-lemma dimensionI:
-  assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
-    independent (basis ` {..<d} :: 'a set);
-    inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
-  shows "P DIM('a::euclidean_space)"
-  using DIM_positive basis_finite independent_basis basis_inj
-  by (rule assms)
-
-lemma (in euclidean_space) dimension_eq:
-  assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
-  assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
-  shows "DIM('a) = d"
-proof (rule linorder_cases [of "DIM('a)" d])
-  assume "DIM('a) < d"
-  hence "basis DIM('a) \<noteq> 0" by (rule assms)
-  thus ?thesis by simp
-next
-  assume "d < DIM('a)"
-  hence "basis d \<noteq> 0" by simp
-  thus ?thesis by (simp add: assms)
-next
-  assume "DIM('a) = d" thus ?thesis .
-qed
-
 lemma (in euclidean_space) range_basis:
     "range basis = insert 0 (basis ` {..<DIM('a)})"
 proof -
@@ -1628,22 +1359,6 @@
   ultimately show ?thesis by metis
 qed
 
-subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
-
-class ordered_euclidean_space = ord + euclidean_space +
-  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
-  and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
-
-lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
-  unfolding eucl_less[where 'a='a] by auto
-
-lemma euclidean_trans[trans]:
-  fixes x y z :: "'a::ordered_euclidean_space"
-  shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-  and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-  and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
-  by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
-
 subsection {* Linearity and Bilinearity continued *}
 
 lemma linear_bounded:
@@ -2035,8 +1750,15 @@
 lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
   unfolding inner_simps by auto
 
+lemma pairwise_orthogonal_insert:
+  assumes "pairwise orthogonal S"
+  assumes "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+  shows "pairwise orthogonal (insert x S)"
+  using assms unfolding pairwise_def
+  by (auto simp add: orthogonal_commute)
+
 lemma basis_orthogonal:
-  fixes B :: "('a::euclidean_space) set"
+  fixes B :: "('a::real_inner) set"
   assumes fB: "finite B"
   shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
   (is " \<exists>C. ?P B C")
@@ -2064,48 +1786,20 @@
       by (rule span_superset)}
   then have SC: "span ?C = span (insert a B)"
     unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
-  thm pairwise_def
-  {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
-    {assume xa: "x = ?a" and ya: "y = ?a"
-      have "orthogonal x y" using xa ya xy by blast}
-    moreover
-    {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C"
-      from ya have Cy: "C = insert y (C - {y})" by blast
-      have fth: "finite (C - {y})" using C by simp
-      have "orthogonal x y"
-        using xa ya
-        unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
-        apply simp
-        apply (subst Cy)
-        using C(1) fth
-        apply (simp only: setsum_clauses)
-        apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
-        apply (rule setsum_0')
-        apply clarsimp
-        apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
-        by auto}
-    moreover
-    {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a"
-      from xa have Cx: "C = insert x (C - {x})" by blast
-      have fth: "finite (C - {x})" using C by simp
-      have "orthogonal x y"
-        using xa ya
-        unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
-        apply simp
-        apply (subst Cx)
-        using C(1) fth
-        apply (simp only: setsum_clauses)
-        apply (subst inner_commute[of x])
-        apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
-        apply (rule setsum_0')
-        apply clarsimp
-        apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
-        by auto}
-    moreover
-    {assume xa: "x \<in> C" and ya: "y \<in> C"
-      have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}
-    ultimately have "orthogonal x y" using xC yC by blast}
-  then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast
+  { fix y assume yC: "y \<in> C"
+    hence Cy: "C = insert y (C - {y})" by blast
+    have fth: "finite (C - {y})" using C by simp
+    have "orthogonal ?a y"
+      unfolding orthogonal_def
+      unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
+      unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
+      apply (clarsimp simp add: inner_commute[of y a])
+      apply (rule setsum_0')
+      apply clarsimp
+      apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
+      using `y \<in> C` by auto }
+  with `pairwise orthogonal C` have CPO: "pairwise orthogonal ?C"
+    by (rule pairwise_orthogonal_insert)
   from fC cC SC CPO have "?P (insert a B) ?C" by blast
   then show ?case by blast
 qed
@@ -2166,7 +1860,7 @@
         apply (subst B') using fB fth
         unfolding setsum_clauses(2)[OF fth]
         apply simp unfolding inner_simps
-        apply (clarsimp simp add: inner_add dot_lsum)
+        apply (clarsimp simp add: inner_add inner_setsum_left)
         apply (rule setsum_0', rule ballI)
         unfolding inner_commute
         by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
@@ -3017,7 +2711,23 @@
 apply simp
 done
 
-subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
+subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
+
+class ordered_euclidean_space = ord + euclidean_space +
+  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
+  and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
+
+lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
+  unfolding eucl_less[where 'a='a] by auto
+
+lemma euclidean_trans[trans]:
+  fixes x y z :: "'a::ordered_euclidean_space"
+  shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+  and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+  and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+  unfolding eucl_less[where 'a='a] eucl_le[where 'a='a]
+  by (fast intro: less_trans, fast intro: le_less_trans,
+    fast intro: order_trans)
 
 lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
 
@@ -3036,8 +2746,6 @@
   shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
   unfolding basis_complex_def by auto
 
-subsection {* Products Spaces *}
-
 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
   (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
   unfolding dimension_prod_def by (rule add_commute)
@@ -3051,5 +2759,4 @@
 instance proof qed (auto simp: less_prod_def less_eq_prod_def)
 end
 
-
 end
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Norm_Arith.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -0,0 +1,124 @@
+(*  Title:      HOL/Multivariate_Analysis/Norm_Arith.thy
+    Author:     Amine Chaieb, University of Cambridge
+*)
+
+header {* General linear decision procedure for normed spaces *}
+
+theory Norm_Arith
+imports "~~/src/HOL/Library/Sum_of_Squares"
+uses ("normarith.ML")
+begin
+
+lemma norm_cmul_rule_thm:
+  fixes x :: "'a::real_normed_vector"
+  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+  unfolding norm_scaleR
+  apply (erule mult_left_mono)
+  apply simp
+  done
+
+  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+lemma norm_add_rule_thm:
+  fixes x1 x2 :: "'a::real_normed_vector"
+  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+  by (rule order_trans [OF norm_triangle_ineq add_mono])
+
+lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+  by (simp add: field_simps)
+
+lemma pth_1:
+  fixes x :: "'a::real_normed_vector"
+  shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+  fixes x :: "'a::real_normed_vector"
+  shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+  fixes x :: "'a::real_normed_vector"
+  shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+  by (simp add: scaleR_right_distrib)
+
+lemma pth_7:
+  fixes x :: "'a::real_normed_vector"
+  shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+  by (simp add: scaleR_left_distrib)
+
+lemma pth_9:
+  fixes x :: "'a::real_normed_vector" shows
+  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+  by (simp_all add: algebra_simps)
+
+lemma pth_a:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+  by (simp_all add: algebra_simps)
+
+lemma pth_c:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+  by (simp_all add: algebra_simps)
+
+lemma pth_d:
+  fixes x :: "'a::real_normed_vector"
+  shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+  fixes x :: "'a::real_normed_vector"
+  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+  by atomize auto
+
+lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+
+lemma norm_pths:
+  fixes x :: "'a::real_normed_vector" shows
+  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+  using norm_ge_zero[of "x - y"] by auto
+
+use "normarith.ML"
+
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+*} "prove simple linear statements about vector norms"
+
+text{* Hence more metric properties. *}
+
+lemma dist_triangle_add:
+  fixes x y x' y' :: "'a::real_normed_vector"
+  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+  by norm
+
+lemma dist_triangle_add_half:
+  fixes x x' y y' :: "'a::real_normed_vector"
+  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+  by norm
+
+end
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -92,7 +92,7 @@
 lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
   have *:"\<And>g. path g \<Longrightarrow> path(reversepath g)" unfolding path_def reversepath_def
     apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
-    apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
+    apply(intro continuous_on_intros)
     apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
   show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
 
@@ -108,8 +108,9 @@
     by auto
   thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
     apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
-    apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
-    apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
+    apply (intro continuous_on_intros) defer
+    apply (intro continuous_on_intros)
+    apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
     apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
     apply(rule) defer apply rule proof-
     fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
@@ -132,10 +133,10 @@
     done
   show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
     show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
-      unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
+      unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply (intro continuous_on_intros)
       unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
     show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
-      apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
+      apply(rule continuous_on_compose) apply (intro continuous_on_intros)
       unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
       by (auto simp add: mult_ac) qed qed
 
diff -r f7259c9064ea -r 002b43117115 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 26 10:38:29 2011 -0700
@@ -7,7 +7,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
 begin
 
 (* to be moved elsewhere *)
@@ -20,7 +20,7 @@
   apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
   apply(rule member_le_setL2) by auto
 
-subsection {* General notion of a topologies as values *}
+subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
 typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -555,37 +555,61 @@
 
 subsection {* Interior of a Set *}
 
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+  assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+  shows "x \<in> interior S"
+  using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+  assumes "x \<in> interior S"
+  obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+  using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+  by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+  by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+  by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+  by (intro equalityI interior_subset interior_maximal subset_refl)
 
 lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
-  apply (simp add: set_eq_iff interior_def)
-  apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
-  apply (simp add: interior_def)
-  apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T  \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
-  by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
-  apply (simp add: interior_def)
-  by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+  by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
   by (metis interior_maximal interior_subset subset_trans)
 
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
-  apply (rule equalityI, simp)
-  apply (metis Int_lower1 Int_lower2 subset_interior)
-  by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+  using open_empty by (rule interior_open)
+
+lemma interior_UNIV [simp]: "interior UNIV = UNIV"
+  using open_UNIV by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+  using open_interior by (rule interior_open)
+
+lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+  by (auto simp add: interior_def)
+
+lemma interior_unique:
+  assumes "T \<subseteq> S" and "open T"
+  assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+  shows "interior S = T"
+  by (intro equalityI assms interior_subset open_interior interior_maximal)
+
+lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
+    Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+  using open_contains_ball_eq [where S="interior S"]
+  by (simp add: open_subset_interior)
 
 lemma interior_limit_point [intro]:
   fixes x :: "'a::perfect_space"
@@ -599,21 +623,20 @@
 
 lemma interior_closed_Un_empty_interior:
   assumes cS: "closed S" and iT: "interior T = {}"
-  shows "interior(S \<union> T) = interior S"
+  shows "interior (S \<union> T) = interior S"
 proof
-  show "interior S \<subseteq> interior (S\<union>T)"
-    by (rule subset_interior, blast)
+  show "interior S \<subseteq> interior (S \<union> T)"
+    by (rule interior_mono, rule Un_upper1)
 next
   show "interior (S \<union> T) \<subseteq> interior S"
   proof
     fix x assume "x \<in> interior (S \<union> T)"
-    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
-      unfolding interior_def by fast
+    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
     show "x \<in> interior S"
     proof (rule ccontr)
       assume "x \<notin> interior S"
       with `x \<in> R` `open R` obtain y where "y \<in> R - S"
-        unfolding interior_def set_eq_iff by fast
+        unfolding interior_def by fast
       from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
       from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
       from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +651,16 @@
     by (intro Sigma_mono interior_subset)
   show "open (interior A \<times> interior B)"
     by (intro open_Times open_interior)
-  show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
-    apply (simp add: open_prod_def, clarify)
-    apply (drule (1) bspec, clarify, rename_tac C D)
-    apply (simp add: interior_def, rule conjI)
-    apply (rule_tac x=C in exI, clarsimp)
-    apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
-    apply (rule_tac x=D in exI, clarsimp)
-    apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
-    done
+  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+  proof (safe)
+    fix x y assume "(x, y) \<in> T"
+    then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+      using `open T` unfolding open_prod_def by fast
+    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+      using `T \<subseteq> A \<times> B` by auto
+    thus "x \<in> interior A" and "y \<in> interior B"
+      by (auto intro: interiorI)
+  qed
 qed
 
 
@@ -644,119 +668,50 @@
 
 definition "closure S = S \<union> {x | x. x islimpt S}"
 
+lemma interior_closure: "interior S = - (closure (- S))"
+  unfolding interior_def closure_def islimpt_def by auto
+
 lemma closure_interior: "closure S = - interior (- S)"
-proof-
-  { fix x
-    have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
-    proof
-      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
-      assume "?lhs"
-      hence *:"\<not> ?exT x"
-        unfolding interior_def
-        by simp
-      { assume "\<not> ?rhs"
-        hence False using *
-          unfolding closure_def islimpt_def
-          by blast
-      }
-      thus "?rhs"
-        by blast
-    next
-      assume "?rhs" thus "?lhs"
-        unfolding closure_def interior_def islimpt_def
-        by blast
-    qed
-  }
-  thus ?thesis
-    by blast
-qed
-
-lemma interior_closure: "interior S = - (closure (- S))"
-proof-
-  { fix x
-    have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
-      unfolding interior_def closure_def islimpt_def
-      by auto
-  }
-  thus ?thesis
-    by blast
-qed
+  unfolding interior_closure by simp
 
 lemma closed_closure[simp, intro]: "closed (closure S)"
-proof-
-  have "closed (- interior (-S))" by blast
-  thus ?thesis using closure_interior[of S] by simp
-qed
+  unfolding closure_interior by (simp add: closed_Compl)
+
+lemma closure_subset: "S \<subseteq> closure S"
+  unfolding closure_def by simp
 
 lemma closure_hull: "closure S = closed hull S"
-proof-
-  have "S \<subseteq> closure S"
-    unfolding closure_def
-    by blast
-  moreover
-  have "closed (closure S)"
-    using closed_closure[of S]
-    by assumption
-  moreover
-  { fix t
-    assume *:"S \<subseteq> t" "closed t"
-    { fix x
-      assume "x islimpt S"
-      hence "x islimpt t" using *(1)
-        using islimpt_subset[of x, of S, of t]
-        by blast
-    }
-    with * have "closure S \<subseteq> t"
-      unfolding closure_def
-      using closed_limpt[of t]
-      by auto
-  }
-  ultimately show ?thesis
-    using hull_unique[of S, of "closure S", of closed]
-    by simp
-qed
+  unfolding hull_def closure_interior interior_def by auto
 
 lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
-  unfolding closure_hull
-  using hull_eq[of closed, OF  closed_Inter, of S]
-  by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
-  using closure_eq[of S]
-  by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
-  unfolding closure_hull
-  using hull_hull[of closed S]
-  by assumption
-
-lemma closure_subset: "S \<subseteq> closure S"
-  unfolding closure_hull
-  using hull_subset[of S closed]
-  by assumption
-
-lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
-  unfolding closure_hull
-  using hull_mono[of S T closed]
-  by assumption
-
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow>  closed T \<Longrightarrow> closure S \<subseteq> T"
-  using hull_minimal[of S T closed]
-  unfolding closure_hull
-  by simp
-
-lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
-  using hull_unique[of S T closed]
-  unfolding closure_hull
-  by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
-  using closed_empty closure_closed[of "{}"]
-  by simp
-
-lemma closure_univ[simp]: "closure UNIV = UNIV"
-  using closure_closed[of UNIV]
-  by simp
+  unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+  unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
+  unfolding closure_hull by (rule hull_hull)
+
+lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
+  unfolding closure_hull by (rule hull_mono)
+
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
+  unfolding closure_hull by (rule hull_minimal)
+
+lemma closure_unique:
+  assumes "S \<subseteq> T" and "closed T"
+  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+  shows "closure S = T"
+  using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
+  using closed_empty by (rule closure_closed)
+
+lemma closure_UNIV [simp]: "closure UNIV = UNIV"
+  using closed_UNIV by (rule closure_closed)
+
+lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+  unfolding closure_interior by simp
 
 lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
   using closure_empty closure_subset[of S]
@@ -797,26 +752,19 @@
     by blast
 qed
 
-lemma closure_complement: "closure(- S) = - interior(S)"
-proof-
-  have "S = - (- S)"
-    by auto
-  thus ?thesis
-    unfolding closure_interior
-    by auto
-qed
-
-lemma interior_complement: "interior(- S) = - closure(S)"
-  unfolding closure_interior
-  by blast
+lemma closure_complement: "closure (- S) = - interior S"
+  unfolding closure_interior by simp
+
+lemma interior_complement: "interior (- S) = - closure S"
+  unfolding closure_interior by simp
 
 lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
   show "A \<times> B \<subseteq> closure A \<times> closure B"
     by (intro Sigma_mono closure_subset)
   show "closed (closure A \<times> closure B)"
     by (intro closed_Times closed_closure)
-  show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+  fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
     apply (simp add: closed_def open_prod_def, clarify)
     apply (rule ccontr)
     apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1090,8 +1038,7 @@
   assumes "x \<in> interior S"
   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
 proof-
-  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
-    unfolding interior_def by fast
+  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   { assume "?lhs"
     then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
       unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2783,8 +2730,8 @@
   fixes x :: "'a::t1_space"
   shows "closure (insert x s) = insert x (closure s)"
 apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
 apply (simp add: closure_minimal)
 done
 
@@ -3351,10 +3298,9 @@
   unfolding continuous_on by (metis subset_eq Lim_within_subset)
 
 lemma continuous_on_interior:
-  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)
+  shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+  by (erule interiorE, drule (1) continuous_on_subset,
+    simp add: continuous_on_eq_continuous_at)
 
 lemma continuous_on_eq:
   "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3363,56 +3309,41 @@
 
 text {* Characterization of various kinds of continuity in terms of sequences. *}
 
-(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
 lemma continuous_within_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous (at a within s) f \<longleftrightarrow>
                 (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
                      --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
-    fix e::real assume "e>0"
-    from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
-    from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
-    hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
-      apply(rule_tac  x=N in exI) using N d  apply auto using x(1)
-      apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
-      apply(erule_tac x="x n" in ballE)  apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
+  { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
+    fix T::"'b set" assume "open T" and "f a \<in> T"
+    with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
+      unfolding continuous_within tendsto_def eventually_within by auto
+    have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
+      using x(2) `d>0` by simp
+    hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
+    proof (rule eventually_elim1)
+      fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+        using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+    qed
   }
-  thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
+  thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
 next
-  assume ?rhs
-  { fix e::real assume "e>0"
-    assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
-    hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
-    then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
-      using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
-    { fix d::real assume "d>0"
-      hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
-      then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
-      { fix n::nat assume n:"n\<ge>N"
-        hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
-        moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
-        ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
-      }
-      hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
-    }
-    hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
-    hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e"  using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
-    hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
-  }
-  thus ?lhs  unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
+  assume ?rhs thus ?lhs
+    unfolding continuous_within tendsto_def [where l="f a"]
+    by (simp add: sequentially_imp_eventually_within)
 qed
 
 lemma continuous_at_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  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]
+  unfolding within_UNIV by auto
 
 lemma continuous_on_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_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")
@@ -3527,16 +3458,10 @@
 
 text{* Same thing for setwise continuity. *}
 
-lemma continuous_on_const:
- "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
   unfolding continuous_on_def by (auto intro: tendsto_intros)
 
-lemma continuous_on_cmul:
-  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:
+lemma continuous_on_minus:
   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_def by (auto intro: tendsto_intros)
@@ -3547,12 +3472,46 @@
            \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
   unfolding continuous_on_def by (auto intro: tendsto_intros)
 
-lemma continuous_on_sub:
+lemma continuous_on_diff:
   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_def by (auto intro: tendsto_intros)
 
+lemma (in bounded_linear) continuous_on:
+  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+  unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) continuous_on:
+  "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
+  unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma continuous_on_scaleR:
+  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "continuous_on s f" and "continuous_on s g"
+  shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
+  using bounded_bilinear_scaleR assms
+  by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_mult:
+  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
+  assumes "continuous_on s f" and "continuous_on s g"
+  shows "continuous_on s (\<lambda>x. f x * g x)"
+  using bounded_bilinear_mult assms
+  by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_inner:
+  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
+  assumes "continuous_on s f" and "continuous_on s g"
+  shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
+  using bounded_bilinear_inner assms
+  by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_euclidean_component:
+  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
+  using bounded_linear_euclidean_component
+  by (rule bounded_linear.continuous_on)
+
 text{* Same thing for uniform continuity, using sequential formulations. *}
 
 lemma uniformly_continuous_on_const:
@@ -3796,13 +3755,20 @@
 lemma interior_image_subset:
   assumes "\<forall>x. continuous (at x) f" "inj f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
-  apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s" 
-  hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
-  thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
-    apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
-  proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
-    thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+  fix x assume "x \<in> interior (f ` s)"
+  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+  hence "x \<in> f ` s" by auto
+  then obtain y where y: "y \<in> s" "x = f y" by auto
+  have "open (vimage f T)"
+    using assms(1) `open T` by (rule continuous_open_vimage)
+  moreover have "y \<in> vimage f T"
+    using `x = f y` `x \<in> T` by simp
+  moreover have "vimage f T \<subseteq> s"
+    using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+  ultimately have "y \<in> interior s" ..
+  with `x = f y` show "x \<in> f ` interior s" ..
+qed
 
 text {* Equality of continuous functions on closure and related results. *}
 
@@ -3989,28 +3955,10 @@
 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
-
-lemma continuous_on_mul_real:
-  fixes f :: "'a::metric_space \<Rightarrow> real"
-  fixes g :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s g
-             ==> continuous_on s (\<lambda>x. f x * g x)"
-  using continuous_on_mul[of s f g] unfolding real_scaleR_def .
-
 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 continuous_on_mul continuous_on_vmul continuous_on_mul_real
+  continuous_on_id continuous_on_compose continuous_on_minus
+  continuous_on_diff continuous_on_scaleR continuous_on_mult
+  continuous_on_inner continuous_on_euclidean_component
   uniformly_continuous_on_add uniformly_continuous_on_const
   uniformly_continuous_on_id uniformly_continuous_on_compose
   uniformly_continuous_on_cmul uniformly_continuous_on_neg
@@ -4870,13 +4818,15 @@
   finally show "closed {a .. b}" .
 qed
 
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+  fixes a b :: "'a::ordered_euclidean_space"
+  shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
 proof(rule subset_antisym)
-  show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+  show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+    by (rule interior_maximal)
 next
-  { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
-    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+  { fix x assume "x \<in> interior {a..b}"
+    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
     { fix i assume i:"i<DIM('a)"
       have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4891,7 +4841,7 @@
       hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
         unfolding basis_component using `e>0` i by auto  }
     hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
-  thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+  thus "?L \<subseteq> ?R" ..
 qed
 
 lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"
@@ -5149,21 +5099,12 @@
   finally show ?thesis .
 qed
 
-lemma Lim_inner:
-  assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
-  by (intro tendsto_intros assms)
-
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
 
 lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
   unfolding euclidean_component_def by (rule continuous_at_inner)
 
-lemma continuous_on_inner:
-  fixes s :: "'a::real_inner set"
-  shows "continuous_on s (inner a)"
-  unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
   by (simp add: closed_Collect_le)
 
@@ -5440,8 +5381,7 @@
   unfolding homeomorphic_minimal
   apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
   apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
-  using assms apply auto
-  using continuous_on_cmul[OF continuous_on_id] by auto
+  using assms by (auto simp add: continuous_on_intros)
 
 lemma homeomorphic_translation:
   fixes s :: "'a::real_normed_vector set"
@@ -5763,15 +5703,13 @@
   { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
     hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
       unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
-      apply(auto simp add: pth_3[symmetric] 
-        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"]) 
+      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
       by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
   } moreover
   { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
     hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
       unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
-      apply(auto simp add: pth_3[symmetric]
-        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
       by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
   }
   ultimately show ?thesis using False by auto
@@ -6040,19 +5978,4 @@
 
 declare tendsto_const [intro] (* FIXME: move *)
 
-text {* Legacy theorem names *}
-
-lemmas Lim_ident_at = LIM_ident
-lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
-lemmas Lim_neg = tendsto_minus
-lemmas Lim_add = tendsto_add
-lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = tendsto_scaleR
-lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
-lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
-lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = tendsto_euclidean_component
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
 end