# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1462810999 -3600
# Node ID 60a42a4166afc8e4ced41d141d44c205f821cf39
# Parent  eb5d493a9e03ed4e048f3bc3c6b667046335ba12
lemmas about dimension, hyperplanes, span, etc.

diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
@@ -9,7 +9,7 @@
 
 lemma delta_mult_idempotent:
   "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
-  by (cases "k=a") auto
+  by simp
 
 lemma setsum_UNIV_sum:
   fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
@@ -812,7 +812,6 @@
       have "x \<in> span (columns A)"
         unfolding y[symmetric]
         apply (rule span_setsum)
-        apply clarify
         unfolding scalar_mult_eq_scaleR
         apply (rule span_mul)
         apply (rule span_superset)
diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
@@ -2136,7 +2136,6 @@
 lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
   by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
 
-
 lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
   unfolding affine_dependent_def dependent_def
   using affine_hull_subset_span by auto
@@ -2669,6 +2668,13 @@
   shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
 by (simp add: span_mono subspace_dim_equal subspace_span)
 
+lemma dim_eq_full:
+    fixes S :: "'a :: euclidean_space set"
+    shows "dim S = DIM('a) \<longleftrightarrow> span S = UNIV"
+apply (rule iffI)
+ apply (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV)
+by (metis dim_UNIV dim_span)
+
 lemma span_substd_basis:
   assumes d: "d \<subseteq> Basis"
   shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
@@ -2741,7 +2747,7 @@
 lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
   by (simp add: aff_dim_empty [symmetric])
 
-lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
+lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
   unfolding aff_dim_def using hull_hull[of _ S] by auto
 
 lemma aff_dim_affine_hull2:
@@ -3672,7 +3678,7 @@
   have "aff_dim S \<le> aff_dim (closure S)"
     using aff_dim_subset closure_subset by auto
   moreover have "aff_dim (closure S) \<le> aff_dim (affine hull S)"
-    using aff_dim_subset closure_affine_hull by auto
+    using aff_dim_subset closure_affine_hull by blast
   moreover have "aff_dim (affine hull S) = aff_dim S"
     using aff_dim_affine_hull by auto
   ultimately show ?thesis by auto
@@ -4578,7 +4584,7 @@
   shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
 proof -
   obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
-    by (metis distance_attains_inf[OF assms(2-3)]) 
+    by (metis distance_attains_inf[OF assms(2-3)])
   show ?thesis
     apply (rule_tac x="y - z" in exI)
     apply (rule_tac x="inner (y - z) y" in exI)
@@ -6751,7 +6757,11 @@
 
 lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
   using open_segment_def by auto
-  
+
+lemma convex_contains_open_segment:
+  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
+  by (simp add: convex_contains_segment closed_segment_eq_open)
+
 lemma closed_segment_eq_real_ivl:
   fixes a b::real
   shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
@@ -7759,7 +7769,7 @@
         then have "x /\<^sub>R (2 * real (card d)) \<in> span d"
           using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto
       }
-      then show "\<forall>x\<in>d. x /\<^sub>R (2 * real (card d)) \<in> span d"
+      then show "\<And>x. x\<in>d \<Longrightarrow> x /\<^sub>R (2 * real (card d)) \<in> span d"
         by auto
     qed
     then show "?a \<bullet> i = 0 "
@@ -8124,8 +8134,8 @@
 proof -
   have "rel_interior S \<noteq> {}"
     by (simp add: assms rel_interior_eq_empty)
-  then obtain a where a: "a \<in> rel_interior S"  by blast 
-  with ST have "a \<in> T"  by blast 
+  then obtain a where a: "a \<in> rel_interior S"  by blast
+  with ST have "a \<in> T"  by blast
   have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
     apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
     using assms by blast
@@ -11013,8 +11023,7 @@
     apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane
                 del: One_nat_def)
     apply (rule ex_cong)
-    using span_0
-    apply (force simp: \<open>c = 0\<close>)
+    apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq)
     done
   next
     case False
@@ -11048,7 +11057,7 @@
   qed
 qed
 
-corollary aff_dim_hyperplane:
+corollary aff_dim_hyperplane [simp]:
   fixes a :: "'a::euclidean_space"
   shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
 by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
@@ -11379,17 +11388,17 @@
 
 subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
 
-lemma 
+lemma
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))" 
+  assumes "~ (affine_dependent(s \<union> t))"
     shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)
       and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A)
 proof -
   have [simp]: "finite s" "finite t"
     using aff_independent_finite assms by blast+
-    have "setsum u (s \<inter> t) = 1 \<and> 
-          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)" 
-      if [simp]:  "setsum u s = 1" 
+    have "setsum u (s \<inter> t) = 1 \<and>
+          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
+      if [simp]:  "setsum u s = 1"
                  "setsum v t = 1"
          and eq: "(\<Sum>x\<in>t. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)" for u v
     proof -
@@ -11408,7 +11417,7 @@
     then have u [simp]: "\<And>x. x \<in> s \<Longrightarrow> u x = (if x \<in> t then v x else 0)"
       by (simp add: f_def) presburger
     have "setsum u (s \<inter> t) = setsum u s"
-      by (simp add: setsum.inter_restrict) 
+      by (simp add: setsum.inter_restrict)
     then have "setsum u (s \<inter> t) = 1"
       using that by linarith
     moreover have "(\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
@@ -11423,7 +11432,7 @@
 
 proposition affine_hull_Int:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))" 
+  assumes "~ (affine_dependent(s \<union> t))"
     shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
@@ -11431,20 +11440,20 @@
 
 proposition convex_hull_Int:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))" 
+  assumes "~ (affine_dependent(s \<union> t))"
     shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
 by (simp add: convex_hull_Int_subset assms)
 
-proposition 
+proposition
   fixes s :: "'a::euclidean_space set set"
-  assumes "~ (affine_dependent (\<Union>s))" 
+  assumes "~ (affine_dependent (\<Union>s))"
     shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
       and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
 proof -
   have "finite s"
-    using aff_independent_finite assms finite_UnionD by blast  
+    using aff_independent_finite assms finite_UnionD by blast
   then have "?A \<and> ?C" using assms
   proof (induction s rule: finite_induct)
     case empty then show ?case by auto
@@ -11515,11 +11524,11 @@
     have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
       by (rule affine_independent_subset [OF indc]) auto
     have affeq: "affine hull s = (\<Inter>x\<in>(\<lambda>a. c - {a}) ` (c - b). affine hull x)"
-      using \<open>b \<subseteq> c\<close> False 
+      using \<open>b \<subseteq> c\<close> False
       apply (subst affine_hull_Inter [OF ind, symmetric])
       apply (simp add: eq double_diff)
       done
-    have *: "1 + aff_dim (c - {t}) = int (DIM('a))" 
+    have *: "1 + aff_dim (c - {t}) = int (DIM('a))"
             if t: "t \<in> c" for t
     proof -
       have "insert t c = c"
@@ -11537,4 +11546,592 @@
   qed
 qed
 
+subsection\<open>Misc results about span\<close>
+
+lemma eq_span_insert_eq:
+  assumes "(x - y) \<in> span S"
+    shows "span(insert x S) = span(insert y S)"
+proof -
+  have *: "span(insert x S) \<subseteq> span(insert y S)" if "(x - y) \<in> span S" for x y
+  proof -
+    have 1: "(r *\<^sub>R x - r *\<^sub>R y) \<in> span S" for r
+      by (metis real_vector.scale_right_diff_distrib span_mul that)
+    have 2: "(z - k *\<^sub>R y) - k *\<^sub>R (x - y) = z - k *\<^sub>R x" for  z k
+      by (simp add: real_vector.scale_right_diff_distrib)
+  show ?thesis
+    apply (clarsimp simp add: span_breakdown_eq)
+    by (metis 1 2 diff_add_cancel real_vector.scale_right_diff_distrib span_add_eq)
+  qed
+  show ?thesis
+    apply (intro subset_antisym * assms)
+    using assms subspace_neg subspace_span minus_diff_eq by force
+qed
+
+lemma dim_psubset:
+    fixes S :: "'a :: euclidean_space set"
+    shows "span S \<subset> span T \<Longrightarrow> dim S < dim T"
+by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
+
+
+lemma basis_subspace_exists:
+  fixes S :: "'a::euclidean_space set"
+  shows
+   "subspace S
+        \<Longrightarrow> \<exists>b. finite b \<and> b \<subseteq> S \<and>
+                independent b \<and> span b = S \<and> card b = dim S"
+by (metis span_subspace basis_exists independent_imp_finite)
+
+lemma affine_hyperplane_sums_eq_UNIV_0:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "affine S"
+     and "0 \<in> S" and "w \<in> S"
+     and "a \<bullet> w \<noteq> 0"
+   shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
+proof -
+  have "subspace S"
+    by (simp add: assms subspace_affine)
+  have span1: "span {y. a \<bullet> y = 0} \<subseteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
+    apply (rule span_mono)
+    using \<open>0 \<in> S\<close> add.left_neutral by force
+  have "w \<notin> span {y. a \<bullet> y = 0}"
+    using \<open>a \<bullet> w \<noteq> 0\<close> span_induct subspace_hyperplane by auto
+  moreover have "w \<in> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
+    using \<open>w \<in> S\<close>
+    by (metis (mono_tags, lifting) inner_zero_right mem_Collect_eq pth_d span_superset)
+  ultimately have span2: "span {y. a \<bullet> y = 0} \<noteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
+    by blast
+  have "a \<noteq> 0" using assms inner_zero_left by blast
+  then have "DIM('a) - 1 = dim {y. a \<bullet> y = 0}"
+    by (simp add: dim_hyperplane)
+  also have "... < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
+    using span1 span2 by (blast intro: dim_psubset)
+  finally have DIM_lt: "DIM('a) - 1 < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}" .
+  have subs: "subspace {x + y| x y. x \<in> S \<and> a \<bullet> y = 0}"
+    using subspace_sums [OF \<open>subspace S\<close> subspace_hyperplane] by simp
+  moreover have "span {x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
+    apply (rule dim_eq_full [THEN iffD1])
+    apply (rule antisym [OF dim_subset_UNIV])
+    using DIM_lt apply simp
+    done
+  ultimately show ?thesis
+    by (simp add: subs) (metis (lifting) span_eq subs)
+qed
+
+proposition affine_hyperplane_sums_eq_UNIV:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "affine S"
+      and "S \<inter> {v. a \<bullet> v = b} \<noteq> {}"
+      and "S - {v. a \<bullet> v = b} \<noteq> {}"
+    shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
+proof (cases "a = 0")
+  case True with assms show ?thesis
+    by (auto simp: if_splits)
+next
+  case False
+  obtain c where "c \<in> S" and c: "a \<bullet> c = b"
+    using assms by force
+  with affine_diffs_subspace [OF \<open>affine S\<close>]
+  have "subspace (op + (- c) ` S)" by blast
+  then have aff: "affine (op + (- c) ` S)"
+    by (simp add: subspace_imp_affine)
+  have 0: "0 \<in> op + (- c) ` S"
+    by (simp add: \<open>c \<in> S\<close>)
+  obtain d where "d \<in> S" and "a \<bullet> d \<noteq> b" and dc: "d-c \<in> op + (- c) ` S"
+    using assms by auto
+  then have adc: "a \<bullet> (d - c) \<noteq> 0"
+    by (simp add: c inner_diff_right)
+  let ?U = "op + (c+c) ` {x + y |x y. x \<in> op + (- c) ` S \<and> a \<bullet> y = 0}"
+  have "u + v \<in> op + (c + c) ` {x + v |x v. x \<in> op + (- c) ` S \<and> a \<bullet> v = 0}"
+              if "u \<in> S" "b = a \<bullet> v" for u v
+    apply (rule_tac x="u+v-c-c" in image_eqI)
+    apply (simp_all add: algebra_simps)
+    apply (rule_tac x="u-c" in exI)
+    apply (rule_tac x="v-c" in exI)
+    apply (simp add: algebra_simps that c)
+    done
+  moreover have "\<lbrakk>a \<bullet> v = 0; u \<in> S\<rbrakk>
+       \<Longrightarrow> \<exists>x ya. v + (u + c) = x + ya \<and> x \<in> S \<and> a \<bullet> ya = b" for v u
+    by (metis add.left_commute c inner_right_distrib pth_d)
+  ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U"
+    by (fastforce simp: algebra_simps)
+  also have "... = op + (c+c) ` UNIV"
+    by (simp add: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc])
+  also have "... = UNIV"
+    by (simp add: translation_UNIV)
+  finally show ?thesis .
+qed
+
+proposition dim_sums_Int:
+    fixes S :: "'a :: euclidean_space set"
+  assumes "subspace S" "subspace T"
+  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T"
+proof -
+  obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
+             and indB: "independent B"
+             and cardB: "card B = dim (S \<inter> T)"
+    using basis_exists by blast
+  then obtain C D where "B \<subseteq> C" "C \<subseteq> S" "independent C" "S \<subseteq> span C"
+                    and "B \<subseteq> D" "D \<subseteq> T" "independent D" "T \<subseteq> span D"
+    using maximal_independent_subset_extend
+    by (metis Int_subset_iff \<open>B \<subseteq> S \<inter> T\<close> indB)
+  then have "finite B" "finite C" "finite D"
+    by (simp_all add: independent_imp_finite indB independent_bound)
+  have Beq: "B = C \<inter> D"
+    apply (rule sym)
+    apply (rule spanning_subset_independent)
+    using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast
+    apply (meson \<open>independent C\<close> independent_mono inf.cobounded1)
+    using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto
+    done
+  then have Deq: "D = B \<union> (D - C)"
+    by blast
+  have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}"
+    apply safe
+    apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_0 span_minimal)
+    apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_0 span_minimal)
+    done
+  have "a v = 0" if 0: "(\<Sum>v\<in>C. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v) = 0"
+                 and v: "v \<in> C \<union> (D-C)" for a v
+  proof -
+    have eq: "(\<Sum>v\<in>D - C. a v *\<^sub>R v) = - (\<Sum>v\<in>C. a v *\<^sub>R v)"
+      using that add_eq_0_iff by blast
+    have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> S"
+      apply (subst eq)
+      apply (rule subspace_neg [OF \<open>subspace S\<close>])
+      apply (rule subspace_setsum [OF \<open>subspace S\<close>])
+      by (meson subsetCE subspace_mul \<open>C \<subseteq> S\<close> \<open>subspace S\<close>)
+    moreover have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> T"
+      apply (rule subspace_setsum [OF \<open>subspace T\<close>])
+      by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
+    ultimately have "(\<Sum>v \<in> D-C. a v *\<^sub>R v) \<in> span B"
+      using B by blast
+    then obtain e where e: "(\<Sum>v\<in>B. e v *\<^sub>R v) = (\<Sum>v \<in> D-C. a v *\<^sub>R v)"
+      using span_finite [OF \<open>finite B\<close>] by blast
+    have "\<And>c v. \<lbrakk>(\<Sum>v\<in>C. c v *\<^sub>R v) = 0; v \<in> C\<rbrakk> \<Longrightarrow> c v = 0"
+      using independent_explicit \<open>independent C\<close> by blast
+    def cc \<equiv> "(\<lambda>x. if x \<in> B then a x + e x else a x)"
+    have [simp]: "C \<inter> B = B" "D \<inter> B = B" "C \<inter> - B = C-D" "B \<inter> (D - C) = {}"
+      using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+
+    have f2: "(\<Sum>v\<in>C \<inter> D. e v *\<^sub>R v) = (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
+      using Beq e by presburger
+    have f3: "(\<Sum>v\<in>C \<union> D. a v *\<^sub>R v) = (\<Sum>v\<in>C - D. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v) + (\<Sum>v\<in>C \<inter> D. a v *\<^sub>R v)"
+      using \<open>finite C\<close> \<open>finite D\<close> setsum.union_diff2 by blast
+    have f4: "(\<Sum>v\<in>C \<union> (D - C). a v *\<^sub>R v) = (\<Sum>v\<in>C. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
+      by (meson Diff_disjoint \<open>finite C\<close> \<open>finite D\<close> finite_Diff setsum.union_disjoint)
+    have "(\<Sum>v\<in>C. cc v *\<^sub>R v) = 0"
+      using 0 f2 f3 f4
+      apply (simp add: cc_def Beq if_smult \<open>finite C\<close> setsum.If_cases algebra_simps setsum.distrib)
+      apply (simp add: add.commute add.left_commute diff_eq)
+      done
+    then have "\<And>v. v \<in> C \<Longrightarrow> cc v = 0"
+      using independent_explicit \<open>independent C\<close> by blast
+    then have C0: "\<And>v. v \<in> C - B \<Longrightarrow> a v = 0"
+      by (simp add: cc_def Beq) meson
+    then have [simp]: "(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0"
+      by simp
+    have "(\<Sum>x\<in>C. a x *\<^sub>R x) = (\<Sum>x\<in>B. a x *\<^sub>R x)"
+    proof -
+      have "C - D = C - B"
+        using Beq by blast
+      then show ?thesis
+        using Beq \<open>(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0\<close> f3 f4 by auto
+    qed
+    with 0 have Dcc0: "(\<Sum>v\<in>D. a v *\<^sub>R v) = 0"
+      apply (subst Deq)
+      by (simp add: \<open>finite B\<close> \<open>finite D\<close> setsum_Un)
+    then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0"
+      using independent_explicit \<open>independent D\<close> by blast
+    show ?thesis
+      using v C0 D0 Beq by blast
+  qed
+  then have "independent (C \<union> (D - C))"
+    by (simp add: independent_explicit \<open>finite C\<close> \<open>finite D\<close> setsum_Un del: Un_Diff_cancel)
+  then have indCUD: "independent (C \<union> D)" by simp
+  have "dim (S \<inter> T) = card B"
+    by (rule dim_unique [OF B indB refl])
+  moreover have "dim S = card C"
+    by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
+  moreover have "dim T = card D"
+    by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
+  moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)"
+    apply (rule dim_unique [OF CUD _ indCUD refl], clarify)
+    apply (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_inc span_minimal subsetCE subspace_span sup.bounded_iff)
+    done
+  ultimately show ?thesis
+    using \<open>B = C \<inter> D\<close> [symmetric]
+    by (simp add:  \<open>independent C\<close> \<open>independent D\<close> card_Un_Int independent_finite)
+qed
+
+
+lemma aff_dim_sums_Int_0:
+  assumes "affine S"
+      and "affine T"
+      and "0 \<in> S" "0 \<in> T"
+    shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)"
+proof -
+  have "0 \<in> {x + y |x y. x \<in> S \<and> y \<in> T}"
+    using assms by force
+  then have 0: "0 \<in> affine hull {x + y |x y. x \<in> S \<and> y \<in> T}"
+    by (metis (lifting) hull_inc)
+  have sub: "subspace S"  "subspace T"
+    using assms by (auto simp: subspace_affine)
+  show ?thesis
+    using dim_sums_Int [OF sub] by (simp add: aff_dim_zero assms 0 hull_inc)
+qed
+
+proposition aff_dim_sums_Int:
+  assumes "affine S"
+      and "affine T"
+      and "S \<inter> T \<noteq> {}"
+    shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)"
+proof -
+  obtain a where a: "a \<in> S" "a \<in> T" using assms by force
+  have aff: "affine (op+ (-a) ` S)"  "affine (op+ (-a) ` T)"
+    using assms by (auto simp: affine_translation [symmetric])
+  have zero: "0 \<in> (op+ (-a) ` S)"  "0 \<in> (op+ (-a) ` T)"
+    using a assms by auto
+  have [simp]: "{x + y |x y. x \<in> op + (- a) ` S \<and> y \<in> op + (- a) ` T} =
+        op + (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}"
+    by (force simp: algebra_simps scaleR_2)
+  have [simp]: "op + (- a) ` S \<inter> op + (- a) ` T = op + (- a) ` (S \<inter> T)"
+    by auto
+  show ?thesis
+    using aff_dim_sums_Int_0 [OF aff zero]
+    by (auto simp: aff_dim_translation_eq)
+qed
+
+lemma aff_dim_affine_Int_hyperplane:
+  fixes a :: "'a::euclidean_space"
+  assumes "affine S"
+    shows "aff_dim(S \<inter> {x. a \<bullet> x = b}) =
+             (if S \<inter> {v. a \<bullet> v = b} = {} then - 1
+              else if S \<subseteq> {v. a \<bullet> v = b} then aff_dim S
+              else aff_dim S - 1)"
+proof (cases "a = 0")
+  case True with assms show ?thesis
+    by auto
+next
+  case False
+  then have "aff_dim (S \<inter> {x. a \<bullet> x = b}) = aff_dim S - 1"
+            if "x \<in> S" "a \<bullet> x \<noteq> b" and non: "S \<inter> {v. a \<bullet> v = b} \<noteq> {}" for x
+  proof -
+    have [simp]: "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
+      using affine_hyperplane_sums_eq_UNIV [OF assms non] that  by blast
+    show ?thesis
+      using aff_dim_sums_Int [OF assms affine_hyperplane non]
+      by (simp add: of_nat_diff False)
+  qed
+  then show ?thesis
+    by (metis (mono_tags, lifting) inf.orderE aff_dim_empty_eq mem_Collect_eq subsetI)
+qed
+
+lemma aff_dim_lt_full:
+  fixes S :: "'a::euclidean_space set"
+  shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
+by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
+
+subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
+
+lemma span_delete_0 [simp]: "span(S - {0}) = span S"
+proof
+  show "span (S - {0}) \<subseteq> span S"
+    by (blast intro!: span_mono)
+next
+  have "span S \<subseteq> span(insert 0 (S - {0}))"
+    by (blast intro!: span_mono)
+  also have "... \<subseteq> span(S - {0})"
+    using span_insert_0 by blast
+  finally show "span S \<subseteq> span (S - {0})" .
+qed
+
+lemma span_image_scale:
+  assumes "finite S" and nz: "\<And>x. x \<in> S \<Longrightarrow> c x \<noteq> 0"
+    shows "span ((\<lambda>x. c x *\<^sub>R x) ` S) = span S"
+using assms
+proof (induction S arbitrary: c)
+  case (empty c) show ?case by simp
+next
+  case (insert x F c)
+  show ?case
+  proof (intro set_eqI iffI)
+    fix y
+      assume "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
+      then show "y \<in> span (insert x F)"
+        using insert by (force simp: span_breakdown_eq)
+  next
+    fix y
+      assume "y \<in> span (insert x F)"
+      then show "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
+        using insert
+        apply (clarsimp simp: span_breakdown_eq)
+        apply (rule_tac x="k / c x" in exI)
+        by simp
+  qed
+qed
+
+lemma pairwise_orthogonal_independent:
+  assumes "pairwise orthogonal S" and "0 \<notin> S"
+    shows "independent S"
+proof -
+  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    using assms by (simp add: pairwise_def orthogonal_def)
+  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
+  proof -
+    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
+      using a by (force simp: span_explicit)
+    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
+      by simp
+    also have "... = 0"
+      apply (simp add: inner_setsum_right)
+      apply (rule comm_monoid_add_class.setsum.neutral)
+      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
+    finally show ?thesis
+      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
+  qed
+  then show ?thesis
+    by (force simp: dependent_def)
+qed
+
+lemma pairwise_orthogonal_imp_finite:
+  fixes S :: "'a::euclidean_space set"
+  assumes "pairwise orthogonal S"
+    shows "finite S"
+proof -
+  have "independent (S - {0})"
+    apply (rule pairwise_orthogonal_independent)
+     apply (metis Diff_iff assms pairwise_def)
+    by blast
+  then show ?thesis
+    by (meson independent_imp_finite infinite_remove)
+qed
+
+lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
+  by (simp add: subspace_def orthogonal_clauses)
+
+lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
+  by (simp add: subspace_def orthogonal_clauses)
+
+lemma orthogonal_to_span:
+  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+    shows "orthogonal x a"
+apply (rule CollectD, rule span_induct [OF a subspace_orthogonal_to_vector])
+apply (simp add: x)
+done
+
+proposition Gram_Schmidt_step:
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
+    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
+proof -
+  have "finite S"
+    by (simp add: S pairwise_orthogonal_imp_finite)
+  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
+       if "x \<in> S" for x
+  proof -
+    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
+      by (simp add: \<open>finite S\<close> inner_commute setsum.delta that)
+    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
+      apply (rule setsum.cong [OF refl], simp)
+      by (meson S orthogonal_def pairwise_def that)
+   finally show ?thesis
+     by (simp add: orthogonal_def algebra_simps inner_setsum_left)
+  qed
+  then show ?thesis
+    using orthogonal_to_span orthogonal_commute x by blast
+qed
+
+
+lemma orthogonal_extension_aux:
+  fixes S :: "'a::euclidean_space set"
+  assumes "finite T" "finite S" "pairwise orthogonal S"
+    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
+using assms
+proof (induction arbitrary: S)
+  case empty then show ?case
+    by simp (metis sup_bot_right)
+next
+  case (insert a T)
+  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    using insert by (simp add: pairwise_def orthogonal_def)
+  def a' \<equiv> "a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
+  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
+             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
+    apply (rule exE [OF insert.IH [of "insert a' S"]])
+    apply (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute pairwise_orthogonal_insert span_clauses)
+    done
+  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
+    apply (simp add: a'_def)
+    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
+    apply (force simp: orthogonal_def inner_commute span_inc [THEN subsetD])
+    done
+  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
+    using spanU by simp
+  also have "... = span (insert a (S \<union> T))"
+    apply (rule eq_span_insert_eq)
+    apply (simp add: a'_def span_neg span_setsum span_clauses(1) span_mul)
+    done
+  also have "... = span (S \<union> insert a T)"
+    by simp
+  finally show ?case
+    apply (rule_tac x="insert a' U" in exI)
+    using orthU apply auto
+    done
+qed
+
+
+proposition orthogonal_extension:
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "pairwise orthogonal S"
+  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
+proof -
+  obtain B where "finite B" "span B = span T"
+    using basis_subspace_exists [of "span T"] subspace_span by auto
+  with orthogonal_extension_aux [of B S]
+  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
+    using assms pairwise_orthogonal_imp_finite by auto
+  show ?thesis
+    apply (rule_tac U=U in that)
+     apply (simp add: \<open>pairwise orthogonal (S \<union> U)\<close>)
+    by (metis \<open>span (S \<union> U) = span (S \<union> B)\<close> \<open>span B = span T\<close> span_union)
+qed
+
+corollary orthogonal_extension_strong:
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "pairwise orthogonal S"
+  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
+                   "span (S \<union> U) = span (S \<union> T)"
+proof -
+  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
+    using orthogonal_extension assms by blast
+  then show ?thesis
+    apply (rule_tac U = "U - (insert 0 S)" in that)
+      apply blast
+     apply (force simp: pairwise_def)
+    apply (metis (no_types, lifting) Un_Diff_cancel span_insert_0 span_union)
+  done
+qed
+
+subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
+
+text\<open>existence of orthonormal basis for a subspace.\<close>
+
+lemma orthogonal_spanningset_subspace:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "subspace S"
+  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
+proof -
+  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
+    using basis_exists by blast
+  with orthogonal_extension [of "{}" B]
+  show ?thesis
+    by (metis Un_empty_left assms pairwise_empty span_inc span_subspace that)
+qed
+
+lemma orthogonal_basis_subspace:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "subspace S"
+  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
+                  "card B = dim S" "span B = S"
+proof -
+  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
+    using assms orthogonal_spanningset_subspace by blast
+  then show ?thesis
+    apply (rule_tac B = "B - {0}" in that)
+    apply (auto simp: indep_card_eq_dim_span pairwise_subset Diff_subset pairwise_orthogonal_independent elim: pairwise_subset)
+    done
+qed
+
+proposition orthogonal_subspace_decomp_exists:
+  fixes S :: "'a :: euclidean_space set"
+  obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
+proof -
+  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
+    using orthogonal_basis_subspace subspace_span by blast
+  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
+  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
+    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close> orthogonal_commute that)
+  show ?thesis
+    apply (rule_tac y = "?a" and z = "x - ?a" in that)
+      apply (meson \<open>T \<subseteq> span S\<close> span_mul span_setsum subsetCE)
+     apply (fact orth, simp)
+    done
+qed
+
+lemma orthogonal_subspace_decomp_unique:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "x + y = x' + y'"
+      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
+      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
+  shows "x = x' \<and> y = y'"
+proof -
+  have "x + y - y' = x'"
+    by (simp add: assms)
+  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
+    by (meson orth orthogonal_commute orthogonal_to_span)
+  ultimately have "0 = x' - x"
+    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
+  with assms show ?thesis by auto
+qed
+
+
+text\<open> If we take a slice out of a set, we can do it perpendicularly,
+  with the normal vector to the slice parallel to the affine hull.\<close>
+
+proposition affine_parallel_slice:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "affine S"
+      and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
+      and "~ (S \<subseteq> {x. a \<bullet> x \<le> b})"
+  obtains a' b' where "a' \<noteq> 0"
+                   "S \<inter> {x. a' \<bullet> x \<le> b'} = S \<inter> {x. a \<bullet> x \<le> b}"
+                   "S \<inter> {x. a' \<bullet> x = b'} = S \<inter> {x. a \<bullet> x = b}"
+                   "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
+proof (cases "S \<inter> {x. a \<bullet> x = b} = {}")
+  case True
+  then obtain u v where "u \<in> S" "v \<in> S" "a \<bullet> u \<le> b" "a \<bullet> v > b"
+    using assms by (auto simp: not_le)
+  def \<eta> \<equiv> "u + ((b - a \<bullet> u) / (a \<bullet> v - a \<bullet> u)) *\<^sub>R (v - u)"
+  have "\<eta> \<in> S"
+    by (simp add: \<eta>_def \<open>u \<in> S\<close> \<open>v \<in> S\<close> \<open>affine S\<close> mem_affine_3_minus)
+  moreover have "a \<bullet> \<eta> = b"
+    using \<open>a \<bullet> u \<le> b\<close> \<open>b < a \<bullet> v\<close>
+    by (simp add: \<eta>_def algebra_simps) (simp add: field_simps)
+  ultimately have False
+    using True by force
+  then show ?thesis ..
+next
+  case False
+  then obtain z where "z \<in> S" and z: "a \<bullet> z = b"
+    using assms by auto
+  with affine_diffs_subspace [OF \<open>affine S\<close>]
+  have sub: "subspace (op + (- z) ` S)" by blast
+  then have aff: "affine (op + (- z) ` S)" and span: "span (op + (- z) ` S) = (op + (- z) ` S)"
+    by (auto simp: subspace_imp_affine)
+  obtain a' a'' where a': "a' \<in> span (op + (- z) ` S)" and a: "a = a' + a''"
+                  and "\<And>w. w \<in> span (op + (- z) ` S) \<Longrightarrow> orthogonal a'' w"
+      using orthogonal_subspace_decomp_exists [of "op + (- z) ` S" "a"] by metis
+  then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0"
+    by (simp add: imageI orthogonal_def span)
+  then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z"
+    by (simp add: a inner_diff_right)
+  then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z"
+    by (simp add: inner_diff_left z)
+  have "\<And>w. w \<in> op + (- z) ` S \<Longrightarrow> (w + a') \<in> op + (- z) ` S"
+    by (metis subspace_add a' span_eq sub)
+  then have Sclo: "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
+    by fastforce
+  show ?thesis
+  proof (cases "a' = 0")
+    case True
+    with a assms True a'' diff_zero less_irrefl show ?thesis
+      by auto
+  next
+    case False
+    show ?thesis
+      apply (rule_tac a' = "a'" and b' = "a' \<bullet> z" in that)
+      apply (auto simp: a ba'' inner_left_distrib False Sclo)
+      done
+  qed
+qed
+
 end
diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon May 09 17:23:19 2016 +0100
@@ -836,7 +836,6 @@
       unfolding thr0
       apply (rule span_setsum)
       apply simp
-      apply (rule ballI)
       apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
       apply (rule span_superset)
       apply auto
@@ -878,7 +877,6 @@
   have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
     apply (rule det_row_span)
     apply (rule span_setsum)
-    apply (rule ballI)
     apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
     apply (rule span_superset)
     apply auto
diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon May 09 17:23:19 2016 +0100
@@ -228,7 +228,7 @@
 
 lemma (in real_vector) subspace_setsum:
   assumes sA: "subspace A"
-    and f: "\<forall>x\<in>B. f x \<in> A"
+    and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
   shows "setsum f B \<in> A"
 proof (cases "finite B")
   case True
@@ -236,7 +236,7 @@
     using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
 qed (simp add: subspace_0 [OF sA])
 
-lemma subspace_trivial: "subspace {0}"
+lemma subspace_trivial [iff]: "subspace {0}"
   by (simp add: subspace_def)
 
 lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
@@ -245,7 +245,15 @@
 lemma subspace_Times: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<times> B)"
   unfolding subspace_def zero_prod_def by simp
 
-text \<open>Properties of span.\<close>
+lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
+apply (simp add: subspace_def)
+apply (intro conjI impI allI)
+  using add.right_neutral apply blast
+ apply clarify
+ apply (metis add.assoc add.left_commute)
+using scaleR_add_right by blast
+
+subsection \<open>Properties of span\<close>
 
 lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
   by (metis span_def hull_mono)
@@ -399,7 +407,7 @@
 lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
   by (metis span_clauses(1))
 
-lemma (in real_vector) span_0: "0 \<in> span S"
+lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
   by (metis subspace_span subspace_0)
 
 lemma span_inc: "S \<subseteq> span S"
@@ -414,7 +422,7 @@
   shows "dependent A"
   unfolding dependent_def
   using assms span_0
-  by auto
+  by blast
 
 lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
   by (metis subspace_add subspace_span)
@@ -428,7 +436,7 @@
 lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
   by (metis subspace_span subspace_sub)
 
-lemma (in real_vector) span_setsum: "\<forall>x\<in>A. f x \<in> span S \<Longrightarrow> setsum f A \<in> span S"
+lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
   by (rule subspace_setsum [OF subspace_span])
 
 lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
@@ -697,6 +705,24 @@
   ultimately show ?thesis by blast
 qed
 
+lemma dependent_finite:
+  assumes "finite S"
+    shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = 0)"
+           (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain T u v
+         where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *\<^sub>R v) = 0"
+    by (force simp: dependent_explicit)
+  with assms show ?rhs
+    apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
+    apply (auto simp: setsum.mono_neutral_right)
+    done
+next
+  assume ?rhs  with assms show ?lhs
+    by (fastforce simp add: dependent_explicit)
+qed
+
 lemma span_alt:
   "span B = {(\<Sum>x | f x \<noteq> 0. f x *\<^sub>R x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}"
   unfolding span_explicit
@@ -2007,6 +2033,16 @@
   shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
 using assms independent_bound by auto
 
+lemma independent_explicit:
+  fixes B :: "'a::euclidean_space set"
+  shows "independent B \<longleftrightarrow>
+         finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *\<^sub>R v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
+apply (cases "finite B")
+ apply (force simp: dependent_finite)
+using independent_bound
+apply auto
+done
+
 lemma dependent_biggerset:
   fixes S :: "'a::euclidean_space set"
   shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
@@ -2251,7 +2287,6 @@
       apply (rule span_add_eq)
       apply (rule span_mul)
       apply (rule span_setsum)
-      apply clarify
       apply (rule span_mul)
       apply (rule span_superset)
       apply assumption
@@ -2334,7 +2369,6 @@
   have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
     unfolding sSB
     apply (rule span_setsum)
-    apply clarsimp
     apply (rule span_mul)
     apply (rule span_superset)
     apply assumption
@@ -3095,8 +3129,8 @@
 
 lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
   unfolding norm_cauchy_schwarz_abs_eq
-  apply (cases "x=0", simp_all add: collinear_2)
-  apply (cases "y=0", simp_all add: collinear_2 insert_commute)
+  apply (cases "x=0", simp_all)
+  apply (cases "y=0", simp_all add: insert_commute)
   unfolding collinear_lemma
   apply simp
   apply (subgoal_tac "norm x \<noteq> 0")
diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
@@ -457,7 +457,7 @@
   by (rule openin_clauses)
 
 lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
-  using openin_clauses by blast 
+  using openin_clauses by blast
 
 lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
   using openin_Union[of "{S,T}" U] by auto
@@ -956,7 +956,7 @@
 apply (rule_tac x="e/2" in exI)
 apply force+
 done
-    
+
 lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
   unfolding mem_ball set_eq_iff
   apply (simp add: not_less)
@@ -1408,7 +1408,7 @@
 
 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
   by (simp add: box_ne_empty inner_Basis inner_setsum_left) (simp add: setsum.remove)
-  
+
 
 subsection\<open>Connectedness\<close>
 
@@ -2283,7 +2283,7 @@
   shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
   unfolding frontier_def closure_interior
   by (auto simp add: mem_interior subset_eq ball_def)
-                                               
+
 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
   by (metis frontier_def closure_closed Diff_subset)
 
@@ -3259,7 +3259,7 @@
 
 lemma interior_ball [simp]: "interior (ball x e) = ball x e"
   by (simp add: interior_open)
-  
+
 lemma frontier_ball [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
@@ -5051,17 +5051,27 @@
   using compact_eq_bounded_closed compact_frontier_bounded
   by blast
 
-corollary compact_sphere:
+corollary compact_sphere [simp]:
   fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
   shows "compact (sphere a r)"
 using compact_frontier [of "cball a r"] by simp
 
+corollary bounded_sphere [simp]:
+  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+  shows "bounded (sphere a r)"
+by (simp add: compact_imp_bounded)
+
+corollary closed_sphere  [simp]:
+  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+  shows "closed (sphere a r)"
+by (simp add: compact_imp_closed)
+
 lemma frontier_subset_compact:
   fixes s :: "'a::heine_borel set"
   shows "compact s \<Longrightarrow> frontier s \<subseteq> s"
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
-                 
+
 subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
 
 lemma summable_imp_bounded:
@@ -5997,23 +6007,23 @@
   proof
     fix x and e::real
     assume "0 < e" and x: "x \<in> closure S"
-    obtain \<delta>::real where "\<delta> > 0" 
+    obtain \<delta>::real where "\<delta> > 0"
                    and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
-      using R [of x "e/2"] \<open>0 < e\<close> x by auto 
+      using R [of x "e/2"] \<open>0 < e\<close> x by auto
     have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
     proof -
-      obtain \<delta>'::real where "\<delta>' > 0" 
+      obtain \<delta>'::real where "\<delta>' > 0"
                       and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
-        using R [of y "e/2"] \<open>0 < e\<close> y by auto 
+        using R [of y "e/2"] \<open>0 < e\<close> y by auto
       obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
         using closure_approachable y
         by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
       have "dist (f z) (f y) < e/2"
         apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>'\<close> by linarith 
+        using z \<open>0 < \<delta>'\<close> by linarith
       moreover have "dist (f z) (f x) < e/2"
         apply (rule \<delta> [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto 
+        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
       ultimately show ?thesis
         by (metis dist_commute dist_triangle_half_l less_imp_le)
     qed
@@ -6029,7 +6039,7 @@
     (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
    (is "?lhs = ?rhs")
 proof -
-  have "continuous_on (closure S) f \<longleftrightarrow> 
+  have "continuous_on (closure S) f \<longleftrightarrow>
            (\<forall>x \<in> closure S. continuous (at x within S) f)"
     by (force simp: continuous_on_closure Topology_Euclidean_Space.continuous_within_eps_delta)
   also have "... = ?rhs"
@@ -6046,35 +6056,35 @@
 proof (intro allI impI)
   fix e::real
   assume "0 < e"
-  then obtain d::real 
-    where "d>0" 
+  then obtain d::real
+    where "d>0"
       and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
     using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
   show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
   proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
     fix x y
     assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
-    obtain d1::real where "d1 > 0" 
+    obtain d1::real where "d1 > 0"
            and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
       using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
      obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
-        using closure_approachable [of x S] 
-        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral) 
-    obtain d2::real where "d2 > 0" 
+        using closure_approachable [of x S]
+        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
+    obtain d2::real where "d2 > 0"
            and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
       using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
      obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
-        using closure_approachable [of y S] 
+        using closure_approachable [of y S]
         by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
      have "dist x' x < d/3" using x' by auto
      moreover have "dist x y < d/3"
-       by (metis dist_commute dyx less_divide_eq_numeral1(1)) 
+       by (metis dist_commute dyx less_divide_eq_numeral1(1))
      moreover have "dist y y' < d/3"
-       by (metis (no_types) dist_commute min_less_iff_conj y') 
+       by (metis (no_types) dist_commute min_less_iff_conj y')
      ultimately have "dist x' y' < d/3 + d/3 + d/3"
        by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
-     then have "dist x' y' < d" by simp 
-     then have "dist (f x') (f y') < e/3" 
+     then have "dist x' y' < d" by simp
+     then have "dist (f x') (f y') < e/3"
        by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
      moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
        by (simp add: closure_def)
@@ -7974,6 +7984,10 @@
     (infixr "homeomorphic" 60)
   where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
 
+lemma homeomorphic_empty [iff]:
+     "S homeomorphic {} \<longleftrightarrow> S = {}" "{} homeomorphic S \<longleftrightarrow> S = {}"
+  by (auto simp add: homeomorphic_def homeomorphism_def)
+
 lemma homeomorphic_refl: "s homeomorphic s"
   unfolding homeomorphic_def homeomorphism_def
   using continuous_on_id