src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 63075 60a42a4166af
parent 63072 eb5d493a9e03
child 63077 844725394a37
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
     1.3 @@ -2136,7 +2136,6 @@
     1.4  lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
     1.5    by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
     1.6  
     1.7 -
     1.8  lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
     1.9    unfolding affine_dependent_def dependent_def
    1.10    using affine_hull_subset_span by auto
    1.11 @@ -2669,6 +2668,13 @@
    1.12    shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
    1.13  by (simp add: span_mono subspace_dim_equal subspace_span)
    1.14  
    1.15 +lemma dim_eq_full:
    1.16 +    fixes S :: "'a :: euclidean_space set"
    1.17 +    shows "dim S = DIM('a) \<longleftrightarrow> span S = UNIV"
    1.18 +apply (rule iffI)
    1.19 + apply (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV)
    1.20 +by (metis dim_UNIV dim_span)
    1.21 +
    1.22  lemma span_substd_basis:
    1.23    assumes d: "d \<subseteq> Basis"
    1.24    shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
    1.25 @@ -2741,7 +2747,7 @@
    1.26  lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
    1.27    by (simp add: aff_dim_empty [symmetric])
    1.28  
    1.29 -lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
    1.30 +lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
    1.31    unfolding aff_dim_def using hull_hull[of _ S] by auto
    1.32  
    1.33  lemma aff_dim_affine_hull2:
    1.34 @@ -3672,7 +3678,7 @@
    1.35    have "aff_dim S \<le> aff_dim (closure S)"
    1.36      using aff_dim_subset closure_subset by auto
    1.37    moreover have "aff_dim (closure S) \<le> aff_dim (affine hull S)"
    1.38 -    using aff_dim_subset closure_affine_hull by auto
    1.39 +    using aff_dim_subset closure_affine_hull by blast
    1.40    moreover have "aff_dim (affine hull S) = aff_dim S"
    1.41      using aff_dim_affine_hull by auto
    1.42    ultimately show ?thesis by auto
    1.43 @@ -4578,7 +4584,7 @@
    1.44    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)"
    1.45  proof -
    1.46    obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
    1.47 -    by (metis distance_attains_inf[OF assms(2-3)]) 
    1.48 +    by (metis distance_attains_inf[OF assms(2-3)])
    1.49    show ?thesis
    1.50      apply (rule_tac x="y - z" in exI)
    1.51      apply (rule_tac x="inner (y - z) y" in exI)
    1.52 @@ -6751,7 +6757,11 @@
    1.53  
    1.54  lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
    1.55    using open_segment_def by auto
    1.56 -  
    1.57 +
    1.58 +lemma convex_contains_open_segment:
    1.59 +  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
    1.60 +  by (simp add: convex_contains_segment closed_segment_eq_open)
    1.61 +
    1.62  lemma closed_segment_eq_real_ivl:
    1.63    fixes a b::real
    1.64    shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
    1.65 @@ -7759,7 +7769,7 @@
    1.66          then have "x /\<^sub>R (2 * real (card d)) \<in> span d"
    1.67            using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto
    1.68        }
    1.69 -      then show "\<forall>x\<in>d. x /\<^sub>R (2 * real (card d)) \<in> span d"
    1.70 +      then show "\<And>x. x\<in>d \<Longrightarrow> x /\<^sub>R (2 * real (card d)) \<in> span d"
    1.71          by auto
    1.72      qed
    1.73      then show "?a \<bullet> i = 0 "
    1.74 @@ -8124,8 +8134,8 @@
    1.75  proof -
    1.76    have "rel_interior S \<noteq> {}"
    1.77      by (simp add: assms rel_interior_eq_empty)
    1.78 -  then obtain a where a: "a \<in> rel_interior S"  by blast 
    1.79 -  with ST have "a \<in> T"  by blast 
    1.80 +  then obtain a where a: "a \<in> rel_interior S"  by blast
    1.81 +  with ST have "a \<in> T"  by blast
    1.82    have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
    1.83      apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    1.84      using assms by blast
    1.85 @@ -11013,8 +11023,7 @@
    1.86      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
    1.87                  del: One_nat_def)
    1.88      apply (rule ex_cong)
    1.89 -    using span_0
    1.90 -    apply (force simp: \<open>c = 0\<close>)
    1.91 +    apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq)
    1.92      done
    1.93    next
    1.94      case False
    1.95 @@ -11048,7 +11057,7 @@
    1.96    qed
    1.97  qed
    1.98  
    1.99 -corollary aff_dim_hyperplane:
   1.100 +corollary aff_dim_hyperplane [simp]:
   1.101    fixes a :: "'a::euclidean_space"
   1.102    shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
   1.103  by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
   1.104 @@ -11379,17 +11388,17 @@
   1.105  
   1.106  subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
   1.107  
   1.108 -lemma 
   1.109 +lemma
   1.110    fixes s :: "'a::euclidean_space set"
   1.111 -  assumes "~ (affine_dependent(s \<union> t))" 
   1.112 +  assumes "~ (affine_dependent(s \<union> t))"
   1.113      shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)
   1.114        and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A)
   1.115  proof -
   1.116    have [simp]: "finite s" "finite t"
   1.117      using aff_independent_finite assms by blast+
   1.118 -    have "setsum u (s \<inter> t) = 1 \<and> 
   1.119 -          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)" 
   1.120 -      if [simp]:  "setsum u s = 1" 
   1.121 +    have "setsum u (s \<inter> t) = 1 \<and>
   1.122 +          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
   1.123 +      if [simp]:  "setsum u s = 1"
   1.124                   "setsum v t = 1"
   1.125           and eq: "(\<Sum>x\<in>t. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)" for u v
   1.126      proof -
   1.127 @@ -11408,7 +11417,7 @@
   1.128      then have u [simp]: "\<And>x. x \<in> s \<Longrightarrow> u x = (if x \<in> t then v x else 0)"
   1.129        by (simp add: f_def) presburger
   1.130      have "setsum u (s \<inter> t) = setsum u s"
   1.131 -      by (simp add: setsum.inter_restrict) 
   1.132 +      by (simp add: setsum.inter_restrict)
   1.133      then have "setsum u (s \<inter> t) = 1"
   1.134        using that by linarith
   1.135      moreover have "(\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
   1.136 @@ -11423,7 +11432,7 @@
   1.137  
   1.138  proposition affine_hull_Int:
   1.139    fixes s :: "'a::euclidean_space set"
   1.140 -  assumes "~ (affine_dependent(s \<union> t))" 
   1.141 +  assumes "~ (affine_dependent(s \<union> t))"
   1.142      shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
   1.143  apply (rule subset_antisym)
   1.144  apply (simp add: hull_mono)
   1.145 @@ -11431,20 +11440,20 @@
   1.146  
   1.147  proposition convex_hull_Int:
   1.148    fixes s :: "'a::euclidean_space set"
   1.149 -  assumes "~ (affine_dependent(s \<union> t))" 
   1.150 +  assumes "~ (affine_dependent(s \<union> t))"
   1.151      shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
   1.152  apply (rule subset_antisym)
   1.153  apply (simp add: hull_mono)
   1.154  by (simp add: convex_hull_Int_subset assms)
   1.155  
   1.156 -proposition 
   1.157 +proposition
   1.158    fixes s :: "'a::euclidean_space set set"
   1.159 -  assumes "~ (affine_dependent (\<Union>s))" 
   1.160 +  assumes "~ (affine_dependent (\<Union>s))"
   1.161      shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
   1.162        and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
   1.163  proof -
   1.164    have "finite s"
   1.165 -    using aff_independent_finite assms finite_UnionD by blast  
   1.166 +    using aff_independent_finite assms finite_UnionD by blast
   1.167    then have "?A \<and> ?C" using assms
   1.168    proof (induction s rule: finite_induct)
   1.169      case empty then show ?case by auto
   1.170 @@ -11515,11 +11524,11 @@
   1.171      have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
   1.172        by (rule affine_independent_subset [OF indc]) auto
   1.173      have affeq: "affine hull s = (\<Inter>x\<in>(\<lambda>a. c - {a}) ` (c - b). affine hull x)"
   1.174 -      using \<open>b \<subseteq> c\<close> False 
   1.175 +      using \<open>b \<subseteq> c\<close> False
   1.176        apply (subst affine_hull_Inter [OF ind, symmetric])
   1.177        apply (simp add: eq double_diff)
   1.178        done
   1.179 -    have *: "1 + aff_dim (c - {t}) = int (DIM('a))" 
   1.180 +    have *: "1 + aff_dim (c - {t}) = int (DIM('a))"
   1.181              if t: "t \<in> c" for t
   1.182      proof -
   1.183        have "insert t c = c"
   1.184 @@ -11537,4 +11546,592 @@
   1.185    qed
   1.186  qed
   1.187  
   1.188 +subsection\<open>Misc results about span\<close>
   1.189 +
   1.190 +lemma eq_span_insert_eq:
   1.191 +  assumes "(x - y) \<in> span S"
   1.192 +    shows "span(insert x S) = span(insert y S)"
   1.193 +proof -
   1.194 +  have *: "span(insert x S) \<subseteq> span(insert y S)" if "(x - y) \<in> span S" for x y
   1.195 +  proof -
   1.196 +    have 1: "(r *\<^sub>R x - r *\<^sub>R y) \<in> span S" for r
   1.197 +      by (metis real_vector.scale_right_diff_distrib span_mul that)
   1.198 +    have 2: "(z - k *\<^sub>R y) - k *\<^sub>R (x - y) = z - k *\<^sub>R x" for  z k
   1.199 +      by (simp add: real_vector.scale_right_diff_distrib)
   1.200 +  show ?thesis
   1.201 +    apply (clarsimp simp add: span_breakdown_eq)
   1.202 +    by (metis 1 2 diff_add_cancel real_vector.scale_right_diff_distrib span_add_eq)
   1.203 +  qed
   1.204 +  show ?thesis
   1.205 +    apply (intro subset_antisym * assms)
   1.206 +    using assms subspace_neg subspace_span minus_diff_eq by force
   1.207 +qed
   1.208 +
   1.209 +lemma dim_psubset:
   1.210 +    fixes S :: "'a :: euclidean_space set"
   1.211 +    shows "span S \<subset> span T \<Longrightarrow> dim S < dim T"
   1.212 +by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
   1.213 +
   1.214 +
   1.215 +lemma basis_subspace_exists:
   1.216 +  fixes S :: "'a::euclidean_space set"
   1.217 +  shows
   1.218 +   "subspace S
   1.219 +        \<Longrightarrow> \<exists>b. finite b \<and> b \<subseteq> S \<and>
   1.220 +                independent b \<and> span b = S \<and> card b = dim S"
   1.221 +by (metis span_subspace basis_exists independent_imp_finite)
   1.222 +
   1.223 +lemma affine_hyperplane_sums_eq_UNIV_0:
   1.224 +  fixes S :: "'a :: euclidean_space set"
   1.225 +  assumes "affine S"
   1.226 +     and "0 \<in> S" and "w \<in> S"
   1.227 +     and "a \<bullet> w \<noteq> 0"
   1.228 +   shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
   1.229 +proof -
   1.230 +  have "subspace S"
   1.231 +    by (simp add: assms subspace_affine)
   1.232 +  have span1: "span {y. a \<bullet> y = 0} \<subseteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
   1.233 +    apply (rule span_mono)
   1.234 +    using \<open>0 \<in> S\<close> add.left_neutral by force
   1.235 +  have "w \<notin> span {y. a \<bullet> y = 0}"
   1.236 +    using \<open>a \<bullet> w \<noteq> 0\<close> span_induct subspace_hyperplane by auto
   1.237 +  moreover have "w \<in> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
   1.238 +    using \<open>w \<in> S\<close>
   1.239 +    by (metis (mono_tags, lifting) inner_zero_right mem_Collect_eq pth_d span_superset)
   1.240 +  ultimately have span2: "span {y. a \<bullet> y = 0} \<noteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
   1.241 +    by blast
   1.242 +  have "a \<noteq> 0" using assms inner_zero_left by blast
   1.243 +  then have "DIM('a) - 1 = dim {y. a \<bullet> y = 0}"
   1.244 +    by (simp add: dim_hyperplane)
   1.245 +  also have "... < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
   1.246 +    using span1 span2 by (blast intro: dim_psubset)
   1.247 +  finally have DIM_lt: "DIM('a) - 1 < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}" .
   1.248 +  have subs: "subspace {x + y| x y. x \<in> S \<and> a \<bullet> y = 0}"
   1.249 +    using subspace_sums [OF \<open>subspace S\<close> subspace_hyperplane] by simp
   1.250 +  moreover have "span {x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
   1.251 +    apply (rule dim_eq_full [THEN iffD1])
   1.252 +    apply (rule antisym [OF dim_subset_UNIV])
   1.253 +    using DIM_lt apply simp
   1.254 +    done
   1.255 +  ultimately show ?thesis
   1.256 +    by (simp add: subs) (metis (lifting) span_eq subs)
   1.257 +qed
   1.258 +
   1.259 +proposition affine_hyperplane_sums_eq_UNIV:
   1.260 +  fixes S :: "'a :: euclidean_space set"
   1.261 +  assumes "affine S"
   1.262 +      and "S \<inter> {v. a \<bullet> v = b} \<noteq> {}"
   1.263 +      and "S - {v. a \<bullet> v = b} \<noteq> {}"
   1.264 +    shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
   1.265 +proof (cases "a = 0")
   1.266 +  case True with assms show ?thesis
   1.267 +    by (auto simp: if_splits)
   1.268 +next
   1.269 +  case False
   1.270 +  obtain c where "c \<in> S" and c: "a \<bullet> c = b"
   1.271 +    using assms by force
   1.272 +  with affine_diffs_subspace [OF \<open>affine S\<close>]
   1.273 +  have "subspace (op + (- c) ` S)" by blast
   1.274 +  then have aff: "affine (op + (- c) ` S)"
   1.275 +    by (simp add: subspace_imp_affine)
   1.276 +  have 0: "0 \<in> op + (- c) ` S"
   1.277 +    by (simp add: \<open>c \<in> S\<close>)
   1.278 +  obtain d where "d \<in> S" and "a \<bullet> d \<noteq> b" and dc: "d-c \<in> op + (- c) ` S"
   1.279 +    using assms by auto
   1.280 +  then have adc: "a \<bullet> (d - c) \<noteq> 0"
   1.281 +    by (simp add: c inner_diff_right)
   1.282 +  let ?U = "op + (c+c) ` {x + y |x y. x \<in> op + (- c) ` S \<and> a \<bullet> y = 0}"
   1.283 +  have "u + v \<in> op + (c + c) ` {x + v |x v. x \<in> op + (- c) ` S \<and> a \<bullet> v = 0}"
   1.284 +              if "u \<in> S" "b = a \<bullet> v" for u v
   1.285 +    apply (rule_tac x="u+v-c-c" in image_eqI)
   1.286 +    apply (simp_all add: algebra_simps)
   1.287 +    apply (rule_tac x="u-c" in exI)
   1.288 +    apply (rule_tac x="v-c" in exI)
   1.289 +    apply (simp add: algebra_simps that c)
   1.290 +    done
   1.291 +  moreover have "\<lbrakk>a \<bullet> v = 0; u \<in> S\<rbrakk>
   1.292 +       \<Longrightarrow> \<exists>x ya. v + (u + c) = x + ya \<and> x \<in> S \<and> a \<bullet> ya = b" for v u
   1.293 +    by (metis add.left_commute c inner_right_distrib pth_d)
   1.294 +  ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U"
   1.295 +    by (fastforce simp: algebra_simps)
   1.296 +  also have "... = op + (c+c) ` UNIV"
   1.297 +    by (simp add: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc])
   1.298 +  also have "... = UNIV"
   1.299 +    by (simp add: translation_UNIV)
   1.300 +  finally show ?thesis .
   1.301 +qed
   1.302 +
   1.303 +proposition dim_sums_Int:
   1.304 +    fixes S :: "'a :: euclidean_space set"
   1.305 +  assumes "subspace S" "subspace T"
   1.306 +  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T"
   1.307 +proof -
   1.308 +  obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
   1.309 +             and indB: "independent B"
   1.310 +             and cardB: "card B = dim (S \<inter> T)"
   1.311 +    using basis_exists by blast
   1.312 +  then obtain C D where "B \<subseteq> C" "C \<subseteq> S" "independent C" "S \<subseteq> span C"
   1.313 +                    and "B \<subseteq> D" "D \<subseteq> T" "independent D" "T \<subseteq> span D"
   1.314 +    using maximal_independent_subset_extend
   1.315 +    by (metis Int_subset_iff \<open>B \<subseteq> S \<inter> T\<close> indB)
   1.316 +  then have "finite B" "finite C" "finite D"
   1.317 +    by (simp_all add: independent_imp_finite indB independent_bound)
   1.318 +  have Beq: "B = C \<inter> D"
   1.319 +    apply (rule sym)
   1.320 +    apply (rule spanning_subset_independent)
   1.321 +    using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast
   1.322 +    apply (meson \<open>independent C\<close> independent_mono inf.cobounded1)
   1.323 +    using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto
   1.324 +    done
   1.325 +  then have Deq: "D = B \<union> (D - C)"
   1.326 +    by blast
   1.327 +  have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}"
   1.328 +    apply safe
   1.329 +    apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_0 span_minimal)
   1.330 +    apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_0 span_minimal)
   1.331 +    done
   1.332 +  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"
   1.333 +                 and v: "v \<in> C \<union> (D-C)" for a v
   1.334 +  proof -
   1.335 +    have eq: "(\<Sum>v\<in>D - C. a v *\<^sub>R v) = - (\<Sum>v\<in>C. a v *\<^sub>R v)"
   1.336 +      using that add_eq_0_iff by blast
   1.337 +    have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> S"
   1.338 +      apply (subst eq)
   1.339 +      apply (rule subspace_neg [OF \<open>subspace S\<close>])
   1.340 +      apply (rule subspace_setsum [OF \<open>subspace S\<close>])
   1.341 +      by (meson subsetCE subspace_mul \<open>C \<subseteq> S\<close> \<open>subspace S\<close>)
   1.342 +    moreover have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> T"
   1.343 +      apply (rule subspace_setsum [OF \<open>subspace T\<close>])
   1.344 +      by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
   1.345 +    ultimately have "(\<Sum>v \<in> D-C. a v *\<^sub>R v) \<in> span B"
   1.346 +      using B by blast
   1.347 +    then obtain e where e: "(\<Sum>v\<in>B. e v *\<^sub>R v) = (\<Sum>v \<in> D-C. a v *\<^sub>R v)"
   1.348 +      using span_finite [OF \<open>finite B\<close>] by blast
   1.349 +    have "\<And>c v. \<lbrakk>(\<Sum>v\<in>C. c v *\<^sub>R v) = 0; v \<in> C\<rbrakk> \<Longrightarrow> c v = 0"
   1.350 +      using independent_explicit \<open>independent C\<close> by blast
   1.351 +    def cc \<equiv> "(\<lambda>x. if x \<in> B then a x + e x else a x)"
   1.352 +    have [simp]: "C \<inter> B = B" "D \<inter> B = B" "C \<inter> - B = C-D" "B \<inter> (D - C) = {}"
   1.353 +      using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+
   1.354 +    have f2: "(\<Sum>v\<in>C \<inter> D. e v *\<^sub>R v) = (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
   1.355 +      using Beq e by presburger
   1.356 +    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)"
   1.357 +      using \<open>finite C\<close> \<open>finite D\<close> setsum.union_diff2 by blast
   1.358 +    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)"
   1.359 +      by (meson Diff_disjoint \<open>finite C\<close> \<open>finite D\<close> finite_Diff setsum.union_disjoint)
   1.360 +    have "(\<Sum>v\<in>C. cc v *\<^sub>R v) = 0"
   1.361 +      using 0 f2 f3 f4
   1.362 +      apply (simp add: cc_def Beq if_smult \<open>finite C\<close> setsum.If_cases algebra_simps setsum.distrib)
   1.363 +      apply (simp add: add.commute add.left_commute diff_eq)
   1.364 +      done
   1.365 +    then have "\<And>v. v \<in> C \<Longrightarrow> cc v = 0"
   1.366 +      using independent_explicit \<open>independent C\<close> by blast
   1.367 +    then have C0: "\<And>v. v \<in> C - B \<Longrightarrow> a v = 0"
   1.368 +      by (simp add: cc_def Beq) meson
   1.369 +    then have [simp]: "(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0"
   1.370 +      by simp
   1.371 +    have "(\<Sum>x\<in>C. a x *\<^sub>R x) = (\<Sum>x\<in>B. a x *\<^sub>R x)"
   1.372 +    proof -
   1.373 +      have "C - D = C - B"
   1.374 +        using Beq by blast
   1.375 +      then show ?thesis
   1.376 +        using Beq \<open>(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0\<close> f3 f4 by auto
   1.377 +    qed
   1.378 +    with 0 have Dcc0: "(\<Sum>v\<in>D. a v *\<^sub>R v) = 0"
   1.379 +      apply (subst Deq)
   1.380 +      by (simp add: \<open>finite B\<close> \<open>finite D\<close> setsum_Un)
   1.381 +    then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0"
   1.382 +      using independent_explicit \<open>independent D\<close> by blast
   1.383 +    show ?thesis
   1.384 +      using v C0 D0 Beq by blast
   1.385 +  qed
   1.386 +  then have "independent (C \<union> (D - C))"
   1.387 +    by (simp add: independent_explicit \<open>finite C\<close> \<open>finite D\<close> setsum_Un del: Un_Diff_cancel)
   1.388 +  then have indCUD: "independent (C \<union> D)" by simp
   1.389 +  have "dim (S \<inter> T) = card B"
   1.390 +    by (rule dim_unique [OF B indB refl])
   1.391 +  moreover have "dim S = card C"
   1.392 +    by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
   1.393 +  moreover have "dim T = card D"
   1.394 +    by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
   1.395 +  moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)"
   1.396 +    apply (rule dim_unique [OF CUD _ indCUD refl], clarify)
   1.397 +    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)
   1.398 +    done
   1.399 +  ultimately show ?thesis
   1.400 +    using \<open>B = C \<inter> D\<close> [symmetric]
   1.401 +    by (simp add:  \<open>independent C\<close> \<open>independent D\<close> card_Un_Int independent_finite)
   1.402 +qed
   1.403 +
   1.404 +
   1.405 +lemma aff_dim_sums_Int_0:
   1.406 +  assumes "affine S"
   1.407 +      and "affine T"
   1.408 +      and "0 \<in> S" "0 \<in> T"
   1.409 +    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)"
   1.410 +proof -
   1.411 +  have "0 \<in> {x + y |x y. x \<in> S \<and> y \<in> T}"
   1.412 +    using assms by force
   1.413 +  then have 0: "0 \<in> affine hull {x + y |x y. x \<in> S \<and> y \<in> T}"
   1.414 +    by (metis (lifting) hull_inc)
   1.415 +  have sub: "subspace S"  "subspace T"
   1.416 +    using assms by (auto simp: subspace_affine)
   1.417 +  show ?thesis
   1.418 +    using dim_sums_Int [OF sub] by (simp add: aff_dim_zero assms 0 hull_inc)
   1.419 +qed
   1.420 +
   1.421 +proposition aff_dim_sums_Int:
   1.422 +  assumes "affine S"
   1.423 +      and "affine T"
   1.424 +      and "S \<inter> T \<noteq> {}"
   1.425 +    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)"
   1.426 +proof -
   1.427 +  obtain a where a: "a \<in> S" "a \<in> T" using assms by force
   1.428 +  have aff: "affine (op+ (-a) ` S)"  "affine (op+ (-a) ` T)"
   1.429 +    using assms by (auto simp: affine_translation [symmetric])
   1.430 +  have zero: "0 \<in> (op+ (-a) ` S)"  "0 \<in> (op+ (-a) ` T)"
   1.431 +    using a assms by auto
   1.432 +  have [simp]: "{x + y |x y. x \<in> op + (- a) ` S \<and> y \<in> op + (- a) ` T} =
   1.433 +        op + (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}"
   1.434 +    by (force simp: algebra_simps scaleR_2)
   1.435 +  have [simp]: "op + (- a) ` S \<inter> op + (- a) ` T = op + (- a) ` (S \<inter> T)"
   1.436 +    by auto
   1.437 +  show ?thesis
   1.438 +    using aff_dim_sums_Int_0 [OF aff zero]
   1.439 +    by (auto simp: aff_dim_translation_eq)
   1.440 +qed
   1.441 +
   1.442 +lemma aff_dim_affine_Int_hyperplane:
   1.443 +  fixes a :: "'a::euclidean_space"
   1.444 +  assumes "affine S"
   1.445 +    shows "aff_dim(S \<inter> {x. a \<bullet> x = b}) =
   1.446 +             (if S \<inter> {v. a \<bullet> v = b} = {} then - 1
   1.447 +              else if S \<subseteq> {v. a \<bullet> v = b} then aff_dim S
   1.448 +              else aff_dim S - 1)"
   1.449 +proof (cases "a = 0")
   1.450 +  case True with assms show ?thesis
   1.451 +    by auto
   1.452 +next
   1.453 +  case False
   1.454 +  then have "aff_dim (S \<inter> {x. a \<bullet> x = b}) = aff_dim S - 1"
   1.455 +            if "x \<in> S" "a \<bullet> x \<noteq> b" and non: "S \<inter> {v. a \<bullet> v = b} \<noteq> {}" for x
   1.456 +  proof -
   1.457 +    have [simp]: "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
   1.458 +      using affine_hyperplane_sums_eq_UNIV [OF assms non] that  by blast
   1.459 +    show ?thesis
   1.460 +      using aff_dim_sums_Int [OF assms affine_hyperplane non]
   1.461 +      by (simp add: of_nat_diff False)
   1.462 +  qed
   1.463 +  then show ?thesis
   1.464 +    by (metis (mono_tags, lifting) inf.orderE aff_dim_empty_eq mem_Collect_eq subsetI)
   1.465 +qed
   1.466 +
   1.467 +lemma aff_dim_lt_full:
   1.468 +  fixes S :: "'a::euclidean_space set"
   1.469 +  shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
   1.470 +by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
   1.471 +
   1.472 +subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
   1.473 +
   1.474 +lemma span_delete_0 [simp]: "span(S - {0}) = span S"
   1.475 +proof
   1.476 +  show "span (S - {0}) \<subseteq> span S"
   1.477 +    by (blast intro!: span_mono)
   1.478 +next
   1.479 +  have "span S \<subseteq> span(insert 0 (S - {0}))"
   1.480 +    by (blast intro!: span_mono)
   1.481 +  also have "... \<subseteq> span(S - {0})"
   1.482 +    using span_insert_0 by blast
   1.483 +  finally show "span S \<subseteq> span (S - {0})" .
   1.484 +qed
   1.485 +
   1.486 +lemma span_image_scale:
   1.487 +  assumes "finite S" and nz: "\<And>x. x \<in> S \<Longrightarrow> c x \<noteq> 0"
   1.488 +    shows "span ((\<lambda>x. c x *\<^sub>R x) ` S) = span S"
   1.489 +using assms
   1.490 +proof (induction S arbitrary: c)
   1.491 +  case (empty c) show ?case by simp
   1.492 +next
   1.493 +  case (insert x F c)
   1.494 +  show ?case
   1.495 +  proof (intro set_eqI iffI)
   1.496 +    fix y
   1.497 +      assume "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
   1.498 +      then show "y \<in> span (insert x F)"
   1.499 +        using insert by (force simp: span_breakdown_eq)
   1.500 +  next
   1.501 +    fix y
   1.502 +      assume "y \<in> span (insert x F)"
   1.503 +      then show "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
   1.504 +        using insert
   1.505 +        apply (clarsimp simp: span_breakdown_eq)
   1.506 +        apply (rule_tac x="k / c x" in exI)
   1.507 +        by simp
   1.508 +  qed
   1.509 +qed
   1.510 +
   1.511 +lemma pairwise_orthogonal_independent:
   1.512 +  assumes "pairwise orthogonal S" and "0 \<notin> S"
   1.513 +    shows "independent S"
   1.514 +proof -
   1.515 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.516 +    using assms by (simp add: pairwise_def orthogonal_def)
   1.517 +  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
   1.518 +  proof -
   1.519 +    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
   1.520 +      using a by (force simp: span_explicit)
   1.521 +    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
   1.522 +      by simp
   1.523 +    also have "... = 0"
   1.524 +      apply (simp add: inner_setsum_right)
   1.525 +      apply (rule comm_monoid_add_class.setsum.neutral)
   1.526 +      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
   1.527 +    finally show ?thesis
   1.528 +      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
   1.529 +  qed
   1.530 +  then show ?thesis
   1.531 +    by (force simp: dependent_def)
   1.532 +qed
   1.533 +
   1.534 +lemma pairwise_orthogonal_imp_finite:
   1.535 +  fixes S :: "'a::euclidean_space set"
   1.536 +  assumes "pairwise orthogonal S"
   1.537 +    shows "finite S"
   1.538 +proof -
   1.539 +  have "independent (S - {0})"
   1.540 +    apply (rule pairwise_orthogonal_independent)
   1.541 +     apply (metis Diff_iff assms pairwise_def)
   1.542 +    by blast
   1.543 +  then show ?thesis
   1.544 +    by (meson independent_imp_finite infinite_remove)
   1.545 +qed
   1.546 +
   1.547 +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
   1.548 +  by (simp add: subspace_def orthogonal_clauses)
   1.549 +
   1.550 +lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
   1.551 +  by (simp add: subspace_def orthogonal_clauses)
   1.552 +
   1.553 +lemma orthogonal_to_span:
   1.554 +  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
   1.555 +    shows "orthogonal x a"
   1.556 +apply (rule CollectD, rule span_induct [OF a subspace_orthogonal_to_vector])
   1.557 +apply (simp add: x)
   1.558 +done
   1.559 +
   1.560 +proposition Gram_Schmidt_step:
   1.561 +  fixes S :: "'a::euclidean_space set"
   1.562 +  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
   1.563 +    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
   1.564 +proof -
   1.565 +  have "finite S"
   1.566 +    by (simp add: S pairwise_orthogonal_imp_finite)
   1.567 +  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
   1.568 +       if "x \<in> S" for x
   1.569 +  proof -
   1.570 +    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
   1.571 +      by (simp add: \<open>finite S\<close> inner_commute setsum.delta that)
   1.572 +    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
   1.573 +      apply (rule setsum.cong [OF refl], simp)
   1.574 +      by (meson S orthogonal_def pairwise_def that)
   1.575 +   finally show ?thesis
   1.576 +     by (simp add: orthogonal_def algebra_simps inner_setsum_left)
   1.577 +  qed
   1.578 +  then show ?thesis
   1.579 +    using orthogonal_to_span orthogonal_commute x by blast
   1.580 +qed
   1.581 +
   1.582 +
   1.583 +lemma orthogonal_extension_aux:
   1.584 +  fixes S :: "'a::euclidean_space set"
   1.585 +  assumes "finite T" "finite S" "pairwise orthogonal S"
   1.586 +    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
   1.587 +using assms
   1.588 +proof (induction arbitrary: S)
   1.589 +  case empty then show ?case
   1.590 +    by simp (metis sup_bot_right)
   1.591 +next
   1.592 +  case (insert a T)
   1.593 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.594 +    using insert by (simp add: pairwise_def orthogonal_def)
   1.595 +  def a' \<equiv> "a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
   1.596 +  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
   1.597 +             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
   1.598 +    apply (rule exE [OF insert.IH [of "insert a' S"]])
   1.599 +    apply (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute pairwise_orthogonal_insert span_clauses)
   1.600 +    done
   1.601 +  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
   1.602 +    apply (simp add: a'_def)
   1.603 +    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
   1.604 +    apply (force simp: orthogonal_def inner_commute span_inc [THEN subsetD])
   1.605 +    done
   1.606 +  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
   1.607 +    using spanU by simp
   1.608 +  also have "... = span (insert a (S \<union> T))"
   1.609 +    apply (rule eq_span_insert_eq)
   1.610 +    apply (simp add: a'_def span_neg span_setsum span_clauses(1) span_mul)
   1.611 +    done
   1.612 +  also have "... = span (S \<union> insert a T)"
   1.613 +    by simp
   1.614 +  finally show ?case
   1.615 +    apply (rule_tac x="insert a' U" in exI)
   1.616 +    using orthU apply auto
   1.617 +    done
   1.618 +qed
   1.619 +
   1.620 +
   1.621 +proposition orthogonal_extension:
   1.622 +  fixes S :: "'a::euclidean_space set"
   1.623 +  assumes S: "pairwise orthogonal S"
   1.624 +  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   1.625 +proof -
   1.626 +  obtain B where "finite B" "span B = span T"
   1.627 +    using basis_subspace_exists [of "span T"] subspace_span by auto
   1.628 +  with orthogonal_extension_aux [of B S]
   1.629 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
   1.630 +    using assms pairwise_orthogonal_imp_finite by auto
   1.631 +  show ?thesis
   1.632 +    apply (rule_tac U=U in that)
   1.633 +     apply (simp add: \<open>pairwise orthogonal (S \<union> U)\<close>)
   1.634 +    by (metis \<open>span (S \<union> U) = span (S \<union> B)\<close> \<open>span B = span T\<close> span_union)
   1.635 +qed
   1.636 +
   1.637 +corollary orthogonal_extension_strong:
   1.638 +  fixes S :: "'a::euclidean_space set"
   1.639 +  assumes S: "pairwise orthogonal S"
   1.640 +  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
   1.641 +                   "span (S \<union> U) = span (S \<union> T)"
   1.642 +proof -
   1.643 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   1.644 +    using orthogonal_extension assms by blast
   1.645 +  then show ?thesis
   1.646 +    apply (rule_tac U = "U - (insert 0 S)" in that)
   1.647 +      apply blast
   1.648 +     apply (force simp: pairwise_def)
   1.649 +    apply (metis (no_types, lifting) Un_Diff_cancel span_insert_0 span_union)
   1.650 +  done
   1.651 +qed
   1.652 +
   1.653 +subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
   1.654 +
   1.655 +text\<open>existence of orthonormal basis for a subspace.\<close>
   1.656 +
   1.657 +lemma orthogonal_spanningset_subspace:
   1.658 +  fixes S :: "'a :: euclidean_space set"
   1.659 +  assumes "subspace S"
   1.660 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   1.661 +proof -
   1.662 +  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
   1.663 +    using basis_exists by blast
   1.664 +  with orthogonal_extension [of "{}" B]
   1.665 +  show ?thesis
   1.666 +    by (metis Un_empty_left assms pairwise_empty span_inc span_subspace that)
   1.667 +qed
   1.668 +
   1.669 +lemma orthogonal_basis_subspace:
   1.670 +  fixes S :: "'a :: euclidean_space set"
   1.671 +  assumes "subspace S"
   1.672 +  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
   1.673 +                  "card B = dim S" "span B = S"
   1.674 +proof -
   1.675 +  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   1.676 +    using assms orthogonal_spanningset_subspace by blast
   1.677 +  then show ?thesis
   1.678 +    apply (rule_tac B = "B - {0}" in that)
   1.679 +    apply (auto simp: indep_card_eq_dim_span pairwise_subset Diff_subset pairwise_orthogonal_independent elim: pairwise_subset)
   1.680 +    done
   1.681 +qed
   1.682 +
   1.683 +proposition orthogonal_subspace_decomp_exists:
   1.684 +  fixes S :: "'a :: euclidean_space set"
   1.685 +  obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
   1.686 +proof -
   1.687 +  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
   1.688 +    using orthogonal_basis_subspace subspace_span by blast
   1.689 +  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
   1.690 +  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
   1.691 +    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close> orthogonal_commute that)
   1.692 +  show ?thesis
   1.693 +    apply (rule_tac y = "?a" and z = "x - ?a" in that)
   1.694 +      apply (meson \<open>T \<subseteq> span S\<close> span_mul span_setsum subsetCE)
   1.695 +     apply (fact orth, simp)
   1.696 +    done
   1.697 +qed
   1.698 +
   1.699 +lemma orthogonal_subspace_decomp_unique:
   1.700 +  fixes S :: "'a :: euclidean_space set"
   1.701 +  assumes "x + y = x' + y'"
   1.702 +      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
   1.703 +      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
   1.704 +  shows "x = x' \<and> y = y'"
   1.705 +proof -
   1.706 +  have "x + y - y' = x'"
   1.707 +    by (simp add: assms)
   1.708 +  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
   1.709 +    by (meson orth orthogonal_commute orthogonal_to_span)
   1.710 +  ultimately have "0 = x' - x"
   1.711 +    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
   1.712 +  with assms show ?thesis by auto
   1.713 +qed
   1.714 +
   1.715 +
   1.716 +text\<open> If we take a slice out of a set, we can do it perpendicularly,
   1.717 +  with the normal vector to the slice parallel to the affine hull.\<close>
   1.718 +
   1.719 +proposition affine_parallel_slice:
   1.720 +  fixes S :: "'a :: euclidean_space set"
   1.721 +  assumes "affine S"
   1.722 +      and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
   1.723 +      and "~ (S \<subseteq> {x. a \<bullet> x \<le> b})"
   1.724 +  obtains a' b' where "a' \<noteq> 0"
   1.725 +                   "S \<inter> {x. a' \<bullet> x \<le> b'} = S \<inter> {x. a \<bullet> x \<le> b}"
   1.726 +                   "S \<inter> {x. a' \<bullet> x = b'} = S \<inter> {x. a \<bullet> x = b}"
   1.727 +                   "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
   1.728 +proof (cases "S \<inter> {x. a \<bullet> x = b} = {}")
   1.729 +  case True
   1.730 +  then obtain u v where "u \<in> S" "v \<in> S" "a \<bullet> u \<le> b" "a \<bullet> v > b"
   1.731 +    using assms by (auto simp: not_le)
   1.732 +  def \<eta> \<equiv> "u + ((b - a \<bullet> u) / (a \<bullet> v - a \<bullet> u)) *\<^sub>R (v - u)"
   1.733 +  have "\<eta> \<in> S"
   1.734 +    by (simp add: \<eta>_def \<open>u \<in> S\<close> \<open>v \<in> S\<close> \<open>affine S\<close> mem_affine_3_minus)
   1.735 +  moreover have "a \<bullet> \<eta> = b"
   1.736 +    using \<open>a \<bullet> u \<le> b\<close> \<open>b < a \<bullet> v\<close>
   1.737 +    by (simp add: \<eta>_def algebra_simps) (simp add: field_simps)
   1.738 +  ultimately have False
   1.739 +    using True by force
   1.740 +  then show ?thesis ..
   1.741 +next
   1.742 +  case False
   1.743 +  then obtain z where "z \<in> S" and z: "a \<bullet> z = b"
   1.744 +    using assms by auto
   1.745 +  with affine_diffs_subspace [OF \<open>affine S\<close>]
   1.746 +  have sub: "subspace (op + (- z) ` S)" by blast
   1.747 +  then have aff: "affine (op + (- z) ` S)" and span: "span (op + (- z) ` S) = (op + (- z) ` S)"
   1.748 +    by (auto simp: subspace_imp_affine)
   1.749 +  obtain a' a'' where a': "a' \<in> span (op + (- z) ` S)" and a: "a = a' + a''"
   1.750 +                  and "\<And>w. w \<in> span (op + (- z) ` S) \<Longrightarrow> orthogonal a'' w"
   1.751 +      using orthogonal_subspace_decomp_exists [of "op + (- z) ` S" "a"] by metis
   1.752 +  then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0"
   1.753 +    by (simp add: imageI orthogonal_def span)
   1.754 +  then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z"
   1.755 +    by (simp add: a inner_diff_right)
   1.756 +  then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z"
   1.757 +    by (simp add: inner_diff_left z)
   1.758 +  have "\<And>w. w \<in> op + (- z) ` S \<Longrightarrow> (w + a') \<in> op + (- z) ` S"
   1.759 +    by (metis subspace_add a' span_eq sub)
   1.760 +  then have Sclo: "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
   1.761 +    by fastforce
   1.762 +  show ?thesis
   1.763 +  proof (cases "a' = 0")
   1.764 +    case True
   1.765 +    with a assms True a'' diff_zero less_irrefl show ?thesis
   1.766 +      by auto
   1.767 +  next
   1.768 +    case False
   1.769 +    show ?thesis
   1.770 +      apply (rule_tac a' = "a'" and b' = "a' \<bullet> z" in that)
   1.771 +      apply (auto simp: a ba'' inner_left_distrib False Sclo)
   1.772 +      done
   1.773 +  qed
   1.774 +qed
   1.775 +
   1.776  end