src/HOL/Analysis/Starlike.thy

 lemma aff_dim_halfspace_ge:
   fixes a :: "'a::euclidean_space"
   shows "aff_dim {x. a \<bullet> x \<ge> r} =
         (if a = 0 \<and> r > 0 then -1 else DIM('a))"
 using aff_dim_halfspace_le [of "-a" "-r"] by simp
-
-subsection\<open>Properties of special hyperplanes\<close>
-
-lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
-  by (simp add: subspace_def inner_right_distrib)
-
-lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
-  by (simp add: inner_commute inner_right_distrib subspace_def)
-
-lemma special_hyperplane_span:
-  fixes S :: "'n::euclidean_space set"
-  assumes "k \<in> Basis"
-  shows "{x. k \<bullet> x = 0} = span (Basis - {k})"
-proof -
-  have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x
-  proof -
-    have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)"
-      by (simp add: euclidean_representation)
-    also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)"
-      by (auto simp: sum.remove [of _ k] inner_commute assms that)
-    finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" .
-    then show ?thesis
-      by (simp add: span_finite)
-  qed
-  show ?thesis
-    apply (rule span_subspace [symmetric])
-    using assms
-    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
-    done
-qed
-
-lemma dim_special_hyperplane:
-  fixes k :: "'n::euclidean_space"
-  shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
-apply (simp add: special_hyperplane_span)
-apply (rule dim_unique [OF subset_refl])
-apply (auto simp: independent_substdbasis)
-apply (metis member_remove remove_def span_base)
-done
-
-proposition dim_hyperplane:
-  fixes a :: "'a::euclidean_space"
-  assumes "a \<noteq> 0"
-    shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1"
-proof -
-  have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}"
-    by (rule span_unique) (auto simp: subspace_hyperplane)
-  then obtain B where "independent B"
-              and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}"
-              and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B"
-              and card0: "(card B = dim {x. a \<bullet> x = 0})"
-              and ortho: "pairwise orthogonal B"
-    using orthogonal_basis_exists by metis
-  with assms have "a \<notin> span B"
-    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
-  then have ind: "independent (insert a B)"
-    by (simp add: \<open>independent B\<close> independent_insert)
-  have "finite B"
-    using \<open>independent B\<close> independent_bound by blast
-  have "UNIV \<subseteq> span (insert a B)"
-  proof fix y::'a
-    obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0"
-      apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that)
-      using assms
-      by (auto simp: algebra_simps)
-    show "y \<in> span (insert a B)"
-      by (metis (mono_tags, lifting) z Bsub span_eq_iff
-         add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB)
-  qed
-  then have dima: "DIM('a) = dim(insert a B)"
-    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
-  then show ?thesis
-    by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0
-        card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE
-        subspB)
-qed
-
-lemma lowdim_eq_hyperplane:
-  fixes S :: "'a::euclidean_space set"
-  assumes "dim S = DIM('a) - 1"
-  obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}"
-proof -
-  have dimS: "dim S < DIM('a)"
-    by (simp add: assms)
-  then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
-    using lowdim_subset_hyperplane [of S] by fastforce
-  show ?thesis
-    apply (rule that[OF b(1)])
-    apply (rule subspace_dim_equal)
-    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
-        subspace_span)
-qed
-
-lemma dim_eq_hyperplane:
-  fixes S :: "'n::euclidean_space set"
-  shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
-by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
 
 proposition aff_dim_eq_hyperplane:
   fixes S :: "'a::euclidean_space set"
   shows "aff_dim S = DIM('a) - 1 \<longleftrightarrow> (\<exists>a b. a \<noteq> 0 \<and> affine hull S = {x. a \<bullet> x = b})"
 proof (cases "S = {}")

 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 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_sum_right)
-      apply (rule comm_monoid_add_class.sum.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"
-  by (metis a orthogonal_clauses(1,2,4)
-      span_induct_alt x)
-
-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 sum.delta that)
-    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
-      apply (rule sum.cong [OF refl], simp)
-      by (meson S orthogonal_def pairwise_def that)
-   finally show ?thesis
-     by (simp add: orthogonal_def algebra_simps inner_sum_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)
-  define a' where "a' = 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)"
-    by (rule exE [OF insert.IH [of "insert a' S"]])
-      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
-        pairwise_orthogonal_insert span_clauses)
-  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_superset [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_sum span_base span_mul)
-    done
-  also have "... = span (S \<union> insert a T)"
-    by simp
-  finally show ?case
-    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
-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 metis
-  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
-  with \<open>span B = span T\<close> show ?thesis
-    by (rule_tac U=U in that) (auto simp: span_Un)
-qed
-
-corollary%unimportant 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 Un_Diff_cancel Un_insert_left span_redundant span_zero)
-    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_superset 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 pairwise_orthogonal_independent elim: pairwise_subset)
-    done
-qed
-
-proposition orthonormal_basis_subspace:
-  fixes S :: "'a :: euclidean_space set"
-  assumes "subspace S"
-  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
-              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
-              and "independent B" "card B = dim S" "span B = S"
-proof -
-  obtain B where "0 \<notin> B" "B \<subseteq> S"
-             and orth: "pairwise orthogonal B"
-             and "independent B" "card B = dim S" "span B = S"
-    by (blast intro: orthogonal_basis_subspace [OF assms])
-  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
-    using \<open>span B = S\<close> span_superset span_mul by fastforce
-  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
-    using orth by (force simp: pairwise_def orthogonal_clauses)
-  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
-    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
-  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
-    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
-  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
-  proof
-    fix x y
-    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
-    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
-      using 3 by blast
-    ultimately show "x = y"
-      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
-  qed
-  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
-    by (metis \<open>card B = dim S\<close> card_image)
-  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
-    by (metis "1" "4" "5" assms card_eq_dim independent_finite span_subspace)
-  show ?thesis
-    by (rule that [OF 1 2 3 4 5 6])
-qed
-
-
-proposition%unimportant orthogonal_to_subspace_exists_gen:
-  fixes S :: "'a :: euclidean_space set"
-  assumes "span S \<subset> span T"
-  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof -
-  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
-             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
-             and "independent B" "card B = dim S" "span B = span S"
-    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
-      (auto simp: dim_span)
-  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
-    by auto
-  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
-    by (blast intro: orthogonal_extension [OF orthB])
-  show thesis
-  proof (cases "C \<subseteq> insert 0 B")
-    case True
-    then have "C \<subseteq> span B"
-      using span_eq
-      by (metis span_insert_0 subset_trans)
-    moreover have "u \<in> span (B \<union> C)"
-      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
-    ultimately show ?thesis
-      using True \<open>u \<notin> span B\<close>
-      by (metis Un_insert_left span_insert_0 sup.orderE)
-  next
-    case False
-    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
-      by blast
-    then have "x \<in> span T"
-      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC
-          \<open>u \<in> span T\<close> insert_subset span_superset span_mono
-          span_span subsetCE subset_trans sup_bot.comm_neutral)
-    moreover have "orthogonal x y" if "y \<in> span B" for y
-      using that
-    proof (rule span_induct)
-      show "subspace {a. orthogonal x a}"
-        by (simp add: subspace_orthogonal_to_vector)
-      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
-        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
-    qed
-    ultimately show ?thesis
-      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
-  qed
-qed
-
-corollary%unimportant orthogonal_to_subspace_exists:
-  fixes S :: "'a :: euclidean_space set"
-  assumes "dim S < DIM('a)"
-  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof -
-have "span S \<subset> UNIV"
-  by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
-      mem_Collect_eq top.extremum_strict top.not_eq_extremum)
-  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
-    by (auto simp: span_UNIV)
-qed
-
-corollary%unimportant orthogonal_to_vector_exists:
-  fixes x :: "'a :: euclidean_space"
-  assumes "2 \<le> DIM('a)"
-  obtains y where "y \<noteq> 0" "orthogonal x y"
-proof -
-  have "dim {x} < DIM('a)"
-    using assms by auto
-  then show thesis
-    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
-qed
-
-proposition%unimportant orthogonal_subspace_decomp_exists:
-  fixes S :: "'a :: euclidean_space set"
-  obtains y z
-  where "y \<in> span S"
-    and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
-    and "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_scale span_sum 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
-
-lemma vector_in_orthogonal_spanningset:
-  fixes a :: "'a::euclidean_space"
-  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
-  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def
-      pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
-
-lemma vector_in_orthogonal_basis:
-  fixes a :: "'a::euclidean_space"
-  assumes "a \<noteq> 0"
-  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
-                  "span S = UNIV" "card S = DIM('a)"
-proof -
-  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
-    using vector_in_orthogonal_spanningset .
-  show thesis
-  proof
-    show "pairwise orthogonal (S - {0})"
-      using pairwise_mono S(2) by blast
-    show "independent (S - {0})"
-      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
-    show "finite (S - {0})"
-      using \<open>independent (S - {0})\<close> independent_finite by blast
-    show "card (S - {0}) = DIM('a)"
-      using span_delete_0 [of S] S
-      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
-  qed (use S \<open>a \<noteq> 0\<close> in auto)
-qed
-
-lemma vector_in_orthonormal_basis:
-  fixes a :: "'a::euclidean_space"
-  assumes "norm a = 1"
-  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
-    "independent S" "card S = DIM('a)" "span S = UNIV"
-proof -
-  have "a \<noteq> 0"
-    using assms by auto
-  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
-          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
-    by (metis vector_in_orthogonal_basis)
-  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
-  show thesis
-  proof
-    show "a \<in> ?S"
-      using \<open>a \<in> S\<close> assms image_iff by fastforce
-  next
-    show "pairwise orthogonal ?S"
-      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
-    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
-      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
-    then show "independent ?S"
-      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
-    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
-      unfolding inj_on_def
-      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
-    then show "card ?S = DIM('a)"
-      by (simp add: card_image S)
-    show "span ?S = UNIV"
-      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close>
-          field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale
-          zero_less_norm_iff)
-  qed
-qed
-
-proposition dim_orthogonal_sum:
-  fixes A :: "'a::euclidean_space set"
-  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
-    shows "dim(A \<union> B) = dim A + dim B"
-proof -
-  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
-    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
-  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
-    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
-  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
-    by simp
-  have "dim(A \<union> B) = dim (span (A \<union> B))"
-    by (simp add: dim_span)
-  also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
-    by (auto simp add: span_Un image_def)
-  also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
-    by (auto intro!: arg_cong [where f=dim])
-  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
-    by (auto simp: dest: 0)
-  also have "... = dim (span A) + dim (span B)"
-    by (rule dim_sums_Int) (auto simp: subspace_span)
-  also have "... = dim A + dim B"
-    by (simp add: dim_span)
-  finally show ?thesis .
-qed
-
-lemma dim_subspace_orthogonal_to_vectors:
-  fixes A :: "'a::euclidean_space set"
-  assumes "subspace A" "subspace B" "A \<subseteq> B"
-    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
-proof -
-  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
-  proof (rule arg_cong [where f=dim, OF subset_antisym])
-    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
-      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
-  next
-    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
-         if "x \<in> B" for x
-    proof -
-      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
-        using orthogonal_subspace_decomp_exists [of A x] that by auto
-      have "y \<in> span B"
-        using \<open>y \<in> span A\<close> assms(3) span_mono by blast
-      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
-        apply simp
-        using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq
-          span_eq_iff that by blast
-      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
-        by (meson span_superset subset_iff)
-      then show ?thesis
-        apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
-        using \<open>y \<in> span A\<close> add.commute by blast
-    qed
-    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
-      by (rule span_minimal)
-        (auto intro: * span_minimal simp: subspace_span)
-  qed
-  then show ?thesis
-    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
-        orthogonal_commute orthogonal_def)
-qed
-
 lemma aff_dim_openin:
   fixes S :: "'a::euclidean_space set"
   assumes ope: "openin (subtopology euclidean T) S" and "affine T" "S \<noteq> {}"
   shows "aff_dim S = aff_dim T"
 proof -