src/HOL/Analysis/Starlike.thy

 using halfspace_eq_empty_le [of "-a" "-b"]
 by simp
 
 subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
 
-proposition separation_closures:
+proposition%unimportant separation_closures:
   fixes S :: "'a::euclidean_space set"
   assumes "S \<inter> closure T = {}" "T \<inter> closure S = {}"
   obtains U V where "U \<inter> V = {}" "open U" "open V" "S \<subseteq> U" "T \<subseteq> V"
 proof (cases "S = {} \<or> T = {}")
   case True with that show ?thesis by auto

     by (simp add: clo closedin_closed_Int)
 qed
 
 subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
 
-proposition affine_hull_convex_Int_nonempty_interior:
+proposition%unimportant affine_hull_convex_Int_nonempty_interior:
   fixes S :: "'a::real_normed_vector set"
   assumes "convex S" "S \<inter> interior T \<noteq> {}"
     shows "affine hull (S \<inter> T) = affine hull S"
 proof
   show "affine hull (S \<inter> T) \<subseteq> affine hull S"

   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%unimportant\<open>Properties of special hyperplanes\<close>
+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 (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
 qed
 
 subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
 
-proposition separating_hyperplane_closed_point_inset:
+proposition%unimportant separating_hyperplane_closed_point_inset:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "closed S" "S \<noteq> {}" "z \<notin> S"
   obtains a b where "a \<in> S" "(a - z) \<bullet> z < b" "\<And>x. x \<in> S \<Longrightarrow> b < (a - z) \<bullet> x"
 proof -
   obtain y where "y \<in> S" and y: "\<And>u. u \<in> S \<Longrightarrow> dist z y \<le> dist z u"

   obtains a b where "a \<in> S" "a \<noteq> 0" "0 < b" "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x > b"
 using separating_hyperplane_closed_point_inset [OF assms]
 by simp (metis \<open>0 \<notin> S\<close>)
 
 
-proposition separating_hyperplane_set_0_inspan:
+proposition%unimportant separating_hyperplane_set_0_inspan:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "S \<noteq> {}" "0 \<notin> S"
   obtains a where "a \<in> span S" "a \<noteq> 0" "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> a \<bullet> x"
 proof -
   define k where [abs_def]: "k c = {x. 0 \<le> c \<bullet> x}" for c :: 'a

     using \<open>a \<in> span ((+) (- z) ` S)\<close> affine_hull_insert_span_gen apply blast
     apply (simp_all add: \<open>a \<noteq> 0\<close> szx)
     done
 qed
 
-proposition supporting_hyperplane_rel_boundary:
+proposition%unimportant supporting_hyperplane_rel_boundary:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
   obtains a where "a \<noteq> 0"
               and "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
               and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"

     then show ?A ?C
       by (auto simp: convex_hull_finite affine_hull_finite)
 qed
 
 
-proposition affine_hull_Int:
+proposition%unimportant affine_hull_Int:
   fixes s :: "'a::euclidean_space set"
   assumes "\<not> 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)
 by (simp add: affine_hull_Int_subset assms)
 
-proposition convex_hull_Int:
+proposition%unimportant convex_hull_Int:
   fixes s :: "'a::euclidean_space set"
   assumes "\<not> 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%unimportant
   fixes s :: "'a::euclidean_space set set"
   assumes "\<not> 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 -

   qed
   then show "?A" "?C"
     by auto
 qed
 
-proposition in_convex_hull_exchange_unique:
+proposition%unimportant in_convex_hull_exchange_unique:
   fixes S :: "'a::euclidean_space set"
   assumes naff: "\<not> affine_dependent S" and a: "a \<in> convex hull S"
       and S: "T \<subseteq> S" "T' \<subseteq> S"
       and x:  "x \<in> convex hull (insert a T)"
       and x': "x \<in> convex hull (insert a T')"

         by simp
     qed
   qed
 qed
 
-corollary convex_hull_exchange_Int:
+corollary%unimportant convex_hull_exchange_Int:
   fixes a  :: "'a::euclidean_space"
   assumes "\<not> affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
   shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
          convex hull (insert a (T \<inter> T'))"
 apply (rule subset_antisym)

     done
   ultimately show ?thesis
     by (simp add: subs) (metis (lifting) span_eq_iff subs)
 qed
 
-proposition affine_hyperplane_sums_eq_UNIV:
+proposition%unimportant 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"

     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 orthogonal_extension_strong:
+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 -

   show ?thesis
     by (rule that [OF 1 2 3 4 5 6])
 qed
 
 
-proposition orthogonal_to_subspace_exists_gen:
+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"

     ultimately show ?thesis
       using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
   qed
 qed
 
-corollary orthogonal_to_subspace_exists:
+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"

       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 orthogonal_to_vector_exists:
+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 orthogonal_subspace_decomp_exists:
+proposition%unimportant 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"
+  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"

     by (metis dim_less dim_subset inf.cobounded2 inf.orderE inf.strict_boundedE not_le)
   ultimately show ?thesis
     by force
 qed
 
-corollary dense_complement_affine:
+corollary%unimportant dense_complement_affine:
   fixes S :: "'a :: euclidean_space set"
   assumes less: "aff_dim T < aff_dim S" and "affine S" shows "closure(S - T) = S"
 proof (cases "S \<inter> T = {}")
   case True
   then show ?thesis

     by (simp add: dense_complement_subspace)
   then show ?thesis
     by (metis closure_translation translation_diff translation_invert)
 qed
 
-corollary dense_complement_openin_affine_hull:
+corollary%unimportant dense_complement_openin_affine_hull:
   fixes S :: "'a :: euclidean_space set"
   assumes less: "aff_dim T < aff_dim S"
       and ope: "openin (subtopology euclidean (affine hull S)) S"
     shows "closure(S - T) = closure S"
 proof -

     by (rule closure_openin_Int_closure [OF ope])
   then show ?thesis
     by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
 qed
 
-corollary dense_complement_convex:
+corollary%unimportant dense_complement_convex:
   fixes S :: "'a :: euclidean_space set"
   assumes "aff_dim T < aff_dim S" "convex S"
     shows "closure(S - T) = closure S"
 proof
   show "closure (S - T) \<subseteq> closure S"

     using \<open>convex S\<close> rel_interior_rel_open rel_open by blast
   then show "closure S \<subseteq> closure (S - T)"
     by (metis Diff_mono \<open>convex S\<close> closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
 qed
 
-corollary dense_complement_convex_closed:
+corollary%unimportant dense_complement_convex_closed:
   fixes S :: "'a :: euclidean_space set"
   assumes "aff_dim T < aff_dim S" "convex S" "closed S"
     shows "closure(S - T) = S"
   by (simp add: assms dense_complement_convex)
 

 subsection%unimportant\<open>Parallel slices, etc\<close>
 
 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:
+proposition%unimportant affine_parallel_slice:
   fixes S :: "'a :: euclidean_space set"
   assumes "affine S"
       and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
       and "\<not> (S \<subseteq> {x. a \<bullet> x \<le> b})"
   obtains a' b' where "a' \<noteq> 0"

     by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq)
   ultimately show ?thesis
     by (rule that)
 qed
 
-subsection\<open>Several Variants of Paracompactness\<close>
+subsection\<open>Paracompactness\<close>
 
 proposition paracompact:
   fixes S :: "'a :: euclidean_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   obtains \<C>' where "S \<subseteq> \<Union> \<C>'"

       apply (auto intro: that finite_subset [OF *])
       done
     qed
 qed
 
-corollary paracompact_closed:
+corollary%unimportant paracompact_closed:
   fixes S :: "'a :: euclidean_space set"
   assumes "closed S"
       and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and "S \<subseteq> \<Union>\<C>"
   obtains \<C>' where "S \<subseteq> \<Union>\<C>'"

     by (rule continuous_on_Un_local_open [OF opS opT])
 qed
   
 subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
 
-proposition in_convex_hull_exchange:
+proposition%unimportant in_convex_hull_exchange:
   fixes a :: "'a::euclidean_space"
   assumes a: "a \<in> convex hull S" and xS: "x \<in> convex hull S"
   obtains b where "b \<in> S" "x \<in> convex hull (insert a (S - {b}))"
 proof (cases "a \<in> S")
   case True

 qed
 
 
 subsection\<open>Orthogonal complement\<close>
 
-definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
+definition%important orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
   where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
 
-lemma subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
+proposition subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
   unfolding subspace_def orthogonal_comp_def orthogonal_def
   by (auto simp: inner_right_distrib)
 
 lemma orthogonal_comp_anti_mono:
   assumes "A \<subseteq> B"

     by (meson set_plus_elim)
   then show "x \<in> U"
     by (meson assms subsetCE subspace_add)
 qed
 
-lemma subspace_sum_orthogonal_comp:
+proposition subspace_sum_orthogonal_comp:
   fixes U :: "'a :: euclidean_space set"
   assumes "subspace U"
   shows "U + U\<^sup>\<bottom> = UNIV"
 proof -
   obtain B where "B \<subseteq> U"

   shows "f -` {0} =  (range (adjoint f))\<^sup>\<bottom>"
   apply (auto simp: orthogonal_comp_def orthogonal_def)
   apply (simp add: adjoint_works assms(1) inner_commute)
   by (metis adjoint_works all_zero_iff assms(1) inner_commute)
 
-subsection\<open> A non-injective linear function maps into a hyperplane.\<close>
+subsection%unimportant \<open>A non-injective linear function maps into a hyperplane.\<close>
 
 lemma linear_surj_adj_imp_inj:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes "linear f" "surj (adjoint f)"
   shows "inj f"

     using \<open>surj f\<close> adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force
   then show "inj (adjoint f)"
     by (simp add: \<open>surj f\<close> adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj)
 qed
 
-proposition linear_singular_into_hyperplane:
+lemma linear_singular_into_hyperplane:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "linear f"
   shows "\<not> inj f \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> (\<forall>x. a \<bullet> f x = 0))" (is "_ = ?rhs")
 proof
   assume "\<not>inj f"