src/HOL/Analysis/Polytope.thy
changeset 68833 fde093888c16
parent 68074 8d50467f7555
child 69260 0a9688695a1b
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Tue Aug 28 13:28:39 2018 +0100
     1.3 @@ -6,18 +6,18 @@
     1.4  imports Cartesian_Euclidean_Space
     1.5  begin
     1.6  
     1.7 -subsection \<open>Faces of a (usually convex) set\<close>
     1.8 -
     1.9 -definition face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
    1.10 +subsection%important \<open>Faces of a (usually convex) set\<close>
    1.11 +
    1.12 +definition%important face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
    1.13    where
    1.14    "T face_of S \<longleftrightarrow>
    1.15          T \<subseteq> S \<and> convex T \<and>
    1.16          (\<forall>a \<in> S. \<forall>b \<in> S. \<forall>x \<in> T. x \<in> open_segment a b \<longrightarrow> a \<in> T \<and> b \<in> T)"
    1.17  
    1.18 -lemma face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
    1.19 +lemma%unimportant face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
    1.20    unfolding face_of_def by blast
    1.21  
    1.22 -lemma face_of_translation_eq [simp]:
    1.23 +lemma%unimportant face_of_translation_eq [simp]:
    1.24      "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
    1.25  proof -
    1.26    have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
    1.27 @@ -32,52 +32,52 @@
    1.28      done
    1.29  qed
    1.30  
    1.31 -lemma face_of_linear_image:
    1.32 +lemma%unimportant face_of_linear_image:
    1.33    assumes "linear f" "inj f"
    1.34      shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
    1.35  by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
    1.36  
    1.37 -lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
    1.38 +lemma%unimportant face_of_refl: "convex S \<Longrightarrow> S face_of S"
    1.39    by (auto simp: face_of_def)
    1.40  
    1.41 -lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
    1.42 +lemma%unimportant face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
    1.43    by (auto simp: face_of_def)
    1.44  
    1.45 -lemma empty_face_of [iff]: "{} face_of S"
    1.46 +lemma%unimportant empty_face_of [iff]: "{} face_of S"
    1.47    by (simp add: face_of_def)
    1.48  
    1.49 -lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
    1.50 +lemma%unimportant face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
    1.51    by (meson empty_face_of face_of_def subset_empty)
    1.52  
    1.53 -lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
    1.54 +lemma%unimportant face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
    1.55    unfolding face_of_def by (safe; blast)
    1.56  
    1.57 -lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
    1.58 +lemma%unimportant face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
    1.59    unfolding face_of_def by (safe; blast)
    1.60  
    1.61 -lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
    1.62 +lemma%unimportant face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
    1.63    unfolding face_of_def by (safe; blast)
    1.64  
    1.65 -lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
    1.66 +lemma%unimportant face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
    1.67    unfolding face_of_def by (blast intro: convex_Int)
    1.68  
    1.69 -lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
    1.70 +lemma%unimportant face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
    1.71    unfolding face_of_def by (blast intro: convex_Int)
    1.72  
    1.73 -lemma face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
    1.74 +lemma%unimportant face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
    1.75    unfolding face_of_def by (blast intro: convex_Inter)
    1.76  
    1.77 -lemma face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
    1.78 +lemma%unimportant face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
    1.79    unfolding face_of_def by (blast intro: convex_Int)
    1.80  
    1.81 -lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
    1.82 +lemma%unimportant face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
    1.83    unfolding face_of_def by blast
    1.84  
    1.85 -lemma face_of_imp_eq_affine_Int:
    1.86 +lemma%important face_of_imp_eq_affine_Int:
    1.87    fixes S :: "'a::euclidean_space set"
    1.88    assumes S: "convex S"  and T: "T face_of S"
    1.89    shows "T = (affine hull T) \<inter> S"
    1.90 -proof -
    1.91 +proof%unimportant -
    1.92    have "convex T" using T by (simp add: face_of_def)
    1.93    have *: False if x: "x \<in> affine hull T" and "x \<in> S" "x \<notin> T" and y: "y \<in> rel_interior T" for x y
    1.94    proof -
    1.95 @@ -114,15 +114,15 @@
    1.96      done
    1.97  qed
    1.98  
    1.99 -lemma face_of_imp_closed:
   1.100 +lemma%unimportant face_of_imp_closed:
   1.101       fixes S :: "'a::euclidean_space set"
   1.102       assumes "convex S" "closed S" "T face_of S" shows "closed T"
   1.103    by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
   1.104  
   1.105 -lemma face_of_Int_supporting_hyperplane_le_strong:
   1.106 +lemma%important face_of_Int_supporting_hyperplane_le_strong:
   1.107      assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
   1.108        shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
   1.109 -proof -
   1.110 +proof%unimportant -
   1.111    have *: "a \<bullet> u = a \<bullet> x" if "x \<in> open_segment u v" "u \<in> S" "v \<in> S" and b: "b = a \<bullet> x"
   1.112            for u v x
   1.113    proof (rule antisym)
   1.114 @@ -145,33 +145,33 @@
   1.115      using "*" open_segment_commute by blast
   1.116  qed
   1.117  
   1.118 -lemma face_of_Int_supporting_hyperplane_ge_strong:
   1.119 +lemma%unimportant face_of_Int_supporting_hyperplane_ge_strong:
   1.120     "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
   1.121      \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   1.122    using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
   1.123  
   1.124 -lemma face_of_Int_supporting_hyperplane_le:
   1.125 +lemma%unimportant face_of_Int_supporting_hyperplane_le:
   1.126      "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   1.127    by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
   1.128  
   1.129 -lemma face_of_Int_supporting_hyperplane_ge:
   1.130 +lemma%unimportant face_of_Int_supporting_hyperplane_ge:
   1.131      "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   1.132    by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
   1.133  
   1.134 -lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
   1.135 +lemma%unimportant face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
   1.136    using face_of_def by blast
   1.137  
   1.138 -lemma face_of_imp_compact:
   1.139 +lemma%unimportant face_of_imp_compact:
   1.140      fixes S :: "'a::euclidean_space set"
   1.141      shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
   1.142    by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
   1.143  
   1.144 -lemma face_of_Int_subface:
   1.145 +lemma%unimportant face_of_Int_subface:
   1.146       "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
   1.147        \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
   1.148    by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
   1.149  
   1.150 -lemma subset_of_face_of:
   1.151 +lemma%unimportant subset_of_face_of:
   1.152      fixes S :: "'a::real_normed_vector set"
   1.153      assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
   1.154        shows "u \<subseteq> T"
   1.155 @@ -213,7 +213,7 @@
   1.156    qed
   1.157  qed
   1.158  
   1.159 -lemma face_of_eq:
   1.160 +lemma%unimportant face_of_eq:
   1.161      fixes S :: "'a::real_normed_vector set"
   1.162      assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
   1.163        shows "T = u"
   1.164 @@ -221,13 +221,13 @@
   1.165    apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
   1.166    by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
   1.167  
   1.168 -lemma face_of_disjoint_rel_interior:
   1.169 +lemma%unimportant face_of_disjoint_rel_interior:
   1.170        fixes S :: "'a::real_normed_vector set"
   1.171        assumes "T face_of S" "T \<noteq> S"
   1.172          shows "T \<inter> rel_interior S = {}"
   1.173    by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
   1.174  
   1.175 -lemma face_of_disjoint_interior:
   1.176 +lemma%unimportant face_of_disjoint_interior:
   1.177        fixes S :: "'a::real_normed_vector set"
   1.178        assumes "T face_of S" "T \<noteq> S"
   1.179          shows "T \<inter> interior S = {}"
   1.180 @@ -238,19 +238,19 @@
   1.181      by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
   1.182  qed
   1.183  
   1.184 -lemma face_of_subset_rel_boundary:
   1.185 +lemma%unimportant face_of_subset_rel_boundary:
   1.186    fixes S :: "'a::real_normed_vector set"
   1.187    assumes "T face_of S" "T \<noteq> S"
   1.188      shows "T \<subseteq> (S - rel_interior S)"
   1.189  by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
   1.190  
   1.191 -lemma face_of_subset_rel_frontier:
   1.192 +lemma%unimportant face_of_subset_rel_frontier:
   1.193      fixes S :: "'a::real_normed_vector set"
   1.194      assumes "T face_of S" "T \<noteq> S"
   1.195        shows "T \<subseteq> rel_frontier S"
   1.196    using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
   1.197  
   1.198 -lemma face_of_aff_dim_lt:
   1.199 +lemma%unimportant face_of_aff_dim_lt:
   1.200    fixes S :: "'a::euclidean_space set"
   1.201    assumes "convex S" "T face_of S" "T \<noteq> S"
   1.202      shows "aff_dim T < aff_dim S"
   1.203 @@ -268,7 +268,7 @@
   1.204      by simp
   1.205  qed
   1.206  
   1.207 -lemma subset_of_face_of_affine_hull:
   1.208 +lemma%unimportant subset_of_face_of_affine_hull:
   1.209      fixes S :: "'a::euclidean_space set"
   1.210    assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "~disjnt (affine hull T) (rel_interior U)"
   1.211    shows "U \<subseteq> T"
   1.212 @@ -277,13 +277,13 @@
   1.213    using rel_interior_subset [of U] dis
   1.214    using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
   1.215  
   1.216 -lemma affine_hull_face_of_disjoint_rel_interior:
   1.217 +lemma%unimportant affine_hull_face_of_disjoint_rel_interior:
   1.218      fixes S :: "'a::euclidean_space set"
   1.219    assumes "convex S" "F face_of S" "F \<noteq> S"
   1.220    shows "affine hull F \<inter> rel_interior S = {}"
   1.221    by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
   1.222  
   1.223 -lemma affine_diff_divide:
   1.224 +lemma%unimportant affine_diff_divide:
   1.225      assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
   1.226        shows "(x - y) /\<^sub>R k \<in> S"
   1.227  proof -
   1.228 @@ -294,10 +294,10 @@
   1.229      using \<open>affine S\<close> xy by (auto simp: affine_alt)
   1.230  qed
   1.231  
   1.232 -lemma face_of_convex_hulls:
   1.233 +lemma%important face_of_convex_hulls:
   1.234        assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
   1.235        shows  "(convex hull T) face_of (convex hull S)"
   1.236 -proof -
   1.237 +proof%unimportant -
   1.238    have fin: "finite T" "finite (S - T)" using assms
   1.239      by (auto simp: finite_subset)
   1.240    have *: "x \<in> convex hull T"
   1.241 @@ -391,16 +391,16 @@
   1.242      using open_segment_commute by (auto simp: face_of_def intro: *)
   1.243  qed
   1.244  
   1.245 -proposition face_of_convex_hull_insert:
   1.246 +proposition%important face_of_convex_hull_insert:
   1.247     "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
   1.248    apply (rule face_of_trans, blast)
   1.249    apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
   1.250    done
   1.251  
   1.252 -proposition face_of_affine_trivial:
   1.253 +proposition%important face_of_affine_trivial:
   1.254      assumes "affine S" "T face_of S"
   1.255      shows "T = {} \<or> T = S"
   1.256 -proof (rule ccontr, clarsimp)
   1.257 +proof%unimportant (rule ccontr, clarsimp)
   1.258    assume "T \<noteq> {}" "T \<noteq> S"
   1.259    then obtain a where "a \<in> T" by auto
   1.260    then have "a \<in> S"
   1.261 @@ -430,16 +430,16 @@
   1.262  qed
   1.263  
   1.264  
   1.265 -lemma face_of_affine_eq:
   1.266 +lemma%unimportant face_of_affine_eq:
   1.267     "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
   1.268  using affine_imp_convex face_of_affine_trivial face_of_refl by auto
   1.269  
   1.270  
   1.271 -lemma Inter_faces_finite_altbound:
   1.272 +lemma%important Inter_faces_finite_altbound:
   1.273      fixes T :: "'a::euclidean_space set set"
   1.274      assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
   1.275      shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
   1.276 -proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
   1.277 +proof%unimportant (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
   1.278    case True
   1.279    then obtain c where c:
   1.280         "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
   1.281 @@ -499,17 +499,17 @@
   1.282      by blast
   1.283  qed
   1.284  
   1.285 -lemma faces_of_translation:
   1.286 +lemma%unimportant faces_of_translation:
   1.287     "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
   1.288  apply (rule subset_antisym, clarify)
   1.289  apply (auto simp: image_iff)
   1.290  apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
   1.291  done
   1.292  
   1.293 -proposition face_of_Times:
   1.294 +proposition%important face_of_Times:
   1.295    assumes "F face_of S" and "F' face_of S'"
   1.296      shows "(F \<times> F') face_of (S \<times> S')"
   1.297 -proof -
   1.298 +proof%unimportant -
   1.299    have "F \<times> F' \<subseteq> S \<times> S'"
   1.300      using assms [unfolded face_of_def] by blast
   1.301    moreover
   1.302 @@ -531,11 +531,11 @@
   1.303      unfolding face_of_def by blast
   1.304  qed
   1.305  
   1.306 -corollary face_of_Times_decomp:
   1.307 +corollary%important face_of_Times_decomp:
   1.308      fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   1.309      shows "c face_of (S \<times> S') \<longleftrightarrow> (\<exists>F F'. F face_of S \<and> F' face_of S' \<and> c = F \<times> F')"
   1.310       (is "?lhs = ?rhs")
   1.311 -proof
   1.312 +proof%unimportant
   1.313    assume c: ?lhs
   1.314    show ?rhs
   1.315    proof (cases "c = {}")
   1.316 @@ -582,13 +582,13 @@
   1.317    assume ?rhs with face_of_Times show ?lhs by auto
   1.318  qed
   1.319  
   1.320 -lemma face_of_Times_eq:
   1.321 +lemma%unimportant face_of_Times_eq:
   1.322      fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   1.323      shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
   1.324             F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
   1.325  by (auto simp: face_of_Times_decomp times_eq_iff)
   1.326  
   1.327 -lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
   1.328 +lemma%unimportant hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
   1.329  proof -
   1.330    have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   1.331      by auto
   1.332 @@ -596,7 +596,7 @@
   1.333    show ?thesis by auto
   1.334  qed
   1.335  
   1.336 -lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
   1.337 +lemma%unimportant hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
   1.338  proof -
   1.339    have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   1.340      by auto
   1.341 @@ -604,12 +604,12 @@
   1.342    show ?thesis by auto
   1.343  qed
   1.344  
   1.345 -lemma face_of_halfspace_le:
   1.346 +lemma%important face_of_halfspace_le:
   1.347    fixes a :: "'n::euclidean_space"
   1.348    shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
   1.349           F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
   1.350       (is "?lhs = ?rhs")
   1.351 -proof (cases "a = 0")
   1.352 +proof%unimportant (cases "a = 0")
   1.353    case True then show ?thesis
   1.354      using face_of_affine_eq affine_UNIV by auto
   1.355  next
   1.356 @@ -635,37 +635,37 @@
   1.357    qed
   1.358  qed
   1.359  
   1.360 -lemma face_of_halfspace_ge:
   1.361 +lemma%unimportant face_of_halfspace_ge:
   1.362    fixes a :: "'n::euclidean_space"
   1.363    shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
   1.364           F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
   1.365  using face_of_halfspace_le [of F "-a" "-b"] by simp
   1.366  
   1.367 -subsection\<open>Exposed faces\<close>
   1.368 +subsection%important\<open>Exposed faces\<close>
   1.369  
   1.370  text\<open>That is, faces that are intersection with supporting hyperplane\<close>
   1.371  
   1.372 -definition exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   1.373 +definition%important exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   1.374                                 (infixr "(exposed'_face'_of)" 50)
   1.375    where "T exposed_face_of S \<longleftrightarrow>
   1.376           T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
   1.377  
   1.378 -lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
   1.379 +lemma%unimportant empty_exposed_face_of [iff]: "{} exposed_face_of S"
   1.380    apply (simp add: exposed_face_of_def)
   1.381    apply (rule_tac x=0 in exI)
   1.382    apply (rule_tac x=1 in exI, force)
   1.383    done
   1.384  
   1.385 -lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   1.386 +lemma%unimportant exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   1.387    apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
   1.388    apply (rule_tac x=0 in exI)+
   1.389    apply force
   1.390    done
   1.391  
   1.392 -lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   1.393 +lemma%unimportant exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   1.394    by simp
   1.395  
   1.396 -lemma exposed_face_of:
   1.397 +lemma%unimportant exposed_face_of:
   1.398      "T exposed_face_of S \<longleftrightarrow>
   1.399       T face_of S \<and>
   1.400       (T = {} \<or> T = S \<or>
   1.401 @@ -688,19 +688,19 @@
   1.402    qed
   1.403  qed
   1.404  
   1.405 -lemma exposed_face_of_Int_supporting_hyperplane_le:
   1.406 +lemma%unimportant exposed_face_of_Int_supporting_hyperplane_le:
   1.407     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   1.408  by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
   1.409  
   1.410 -lemma exposed_face_of_Int_supporting_hyperplane_ge:
   1.411 +lemma%unimportant exposed_face_of_Int_supporting_hyperplane_ge:
   1.412     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   1.413  using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
   1.414  
   1.415 -proposition exposed_face_of_Int:
   1.416 +proposition%important exposed_face_of_Int:
   1.417    assumes "T exposed_face_of S"
   1.418        and "u exposed_face_of S"
   1.419      shows "(T \<inter> u) exposed_face_of S"
   1.420 -proof -
   1.421 +proof%unimportant -
   1.422    obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
   1.423                 and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
   1.424                 and teq: "T = S \<inter> {x. a \<bullet> x = b}"
   1.425 @@ -722,12 +722,12 @@
   1.426      done
   1.427  qed
   1.428  
   1.429 -proposition exposed_face_of_Inter:
   1.430 +proposition%important exposed_face_of_Inter:
   1.431      fixes P :: "'a::euclidean_space set set"
   1.432    assumes "P \<noteq> {}"
   1.433        and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
   1.434      shows "\<Inter>P exposed_face_of S"
   1.435 -proof -
   1.436 +proof%unimportant -
   1.437    obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
   1.438      using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
   1.439      by force
   1.440 @@ -749,14 +749,14 @@
   1.441    qed
   1.442  qed
   1.443  
   1.444 -proposition exposed_face_of_sums:
   1.445 +proposition%important exposed_face_of_sums:
   1.446    assumes "convex S" and "convex T"
   1.447        and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
   1.448            (is "F exposed_face_of ?ST")
   1.449    obtains k l
   1.450      where "k exposed_face_of S" "l exposed_face_of T"
   1.451            "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
   1.452 -proof (cases "F = {}")
   1.453 +proof%unimportant (cases "F = {}")
   1.454    case True then show ?thesis
   1.455      using that by blast
   1.456  next
   1.457 @@ -805,14 +805,14 @@
   1.458    qed
   1.459  qed
   1.460  
   1.461 -lemma exposed_face_of_parallel:
   1.462 +lemma%important exposed_face_of_parallel:
   1.463     "T exposed_face_of S \<longleftrightarrow>
   1.464           T face_of S \<and>
   1.465           (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
   1.466                  (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
   1.467                  (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
   1.468    (is "?lhs = ?rhs")
   1.469 -proof
   1.470 +proof%unimportant
   1.471    assume ?lhs then show ?rhs
   1.472    proof (clarsimp simp: exposed_face_of_def)
   1.473      fix a b
   1.474 @@ -874,40 +874,40 @@
   1.475      unfolding exposed_face_of_def by blast
   1.476  qed
   1.477  
   1.478 -subsection\<open>Extreme points of a set: its singleton faces\<close>
   1.479 -
   1.480 -definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   1.481 +subsection%important\<open>Extreme points of a set: its singleton faces\<close>
   1.482 +
   1.483 +definition%important extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   1.484                                 (infixr "(extreme'_point'_of)" 50)
   1.485    where "x extreme_point_of S \<longleftrightarrow>
   1.486           x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
   1.487  
   1.488 -lemma extreme_point_of_stillconvex:
   1.489 +lemma%unimportant extreme_point_of_stillconvex:
   1.490     "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
   1.491    by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
   1.492  
   1.493 -lemma face_of_singleton:
   1.494 +lemma%unimportant face_of_singleton:
   1.495     "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
   1.496  by (fastforce simp add: extreme_point_of_def face_of_def)
   1.497  
   1.498 -lemma extreme_point_not_in_REL_INTERIOR:
   1.499 +lemma%unimportant extreme_point_not_in_REL_INTERIOR:
   1.500      fixes S :: "'a::real_normed_vector set"
   1.501      shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
   1.502  apply (simp add: face_of_singleton [symmetric])
   1.503  apply (blast dest: face_of_disjoint_rel_interior)
   1.504  done
   1.505  
   1.506 -lemma extreme_point_not_in_interior:
   1.507 +lemma%important extreme_point_not_in_interior:
   1.508      fixes S :: "'a::{real_normed_vector, perfect_space} set"
   1.509      shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
   1.510  apply (case_tac "S = {x}")
   1.511  apply (simp add: empty_interior_finite)
   1.512  by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
   1.513  
   1.514 -lemma extreme_point_of_face:
   1.515 +lemma%unimportant extreme_point_of_face:
   1.516       "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
   1.517    by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
   1.518  
   1.519 -lemma extreme_point_of_convex_hull:
   1.520 +lemma%unimportant extreme_point_of_convex_hull:
   1.521     "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
   1.522  apply (simp add: extreme_point_of_stillconvex)
   1.523  using hull_minimal [of S "(convex hull S) - {x}" convex]
   1.524 @@ -915,52 +915,52 @@
   1.525  apply blast
   1.526  done
   1.527  
   1.528 -lemma extreme_points_of_convex_hull:
   1.529 +lemma%important extreme_points_of_convex_hull:
   1.530     "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
   1.531 -using extreme_point_of_convex_hull by auto
   1.532 -
   1.533 -lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   1.534 +using%unimportant extreme_point_of_convex_hull by auto
   1.535 +
   1.536 +lemma%unimportant extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   1.537    by (simp add: extreme_point_of_def)
   1.538  
   1.539 -lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   1.540 +lemma%unimportant extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   1.541    using extreme_point_of_stillconvex by auto
   1.542  
   1.543 -lemma extreme_point_of_translation_eq:
   1.544 +lemma%unimportant extreme_point_of_translation_eq:
   1.545     "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
   1.546  by (auto simp: extreme_point_of_def)
   1.547  
   1.548 -lemma extreme_points_of_translation:
   1.549 +lemma%important extreme_points_of_translation:
   1.550     "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
   1.551      (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
   1.552 -using extreme_point_of_translation_eq
   1.553 -by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
   1.554 -
   1.555 -lemma extreme_point_of_Int:
   1.556 +using%unimportant extreme_point_of_translation_eq
   1.557 +by%unimportant auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
   1.558 +
   1.559 +lemma%unimportant extreme_point_of_Int:
   1.560     "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
   1.561  by (simp add: extreme_point_of_def)
   1.562  
   1.563 -lemma extreme_point_of_Int_supporting_hyperplane_le:
   1.564 +lemma%important extreme_point_of_Int_supporting_hyperplane_le:
   1.565     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   1.566  apply (simp add: face_of_singleton [symmetric])
   1.567  by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
   1.568  
   1.569 -lemma extreme_point_of_Int_supporting_hyperplane_ge:
   1.570 +lemma%unimportant extreme_point_of_Int_supporting_hyperplane_ge:
   1.571     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   1.572  apply (simp add: face_of_singleton [symmetric])
   1.573  by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
   1.574  
   1.575 -lemma exposed_point_of_Int_supporting_hyperplane_le:
   1.576 +lemma%unimportant exposed_point_of_Int_supporting_hyperplane_le:
   1.577     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   1.578  apply (simp add: exposed_face_of_def face_of_singleton)
   1.579  apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
   1.580  done
   1.581  
   1.582 -lemma exposed_point_of_Int_supporting_hyperplane_ge:
   1.583 +lemma%unimportant exposed_point_of_Int_supporting_hyperplane_ge:
   1.584      "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   1.585  using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
   1.586  by simp
   1.587  
   1.588 -lemma extreme_point_of_convex_hull_insert:
   1.589 +lemma%unimportant extreme_point_of_convex_hull_insert:
   1.590     "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
   1.591  apply (case_tac "a \<in> S")
   1.592  apply (simp add: hull_inc)
   1.593 @@ -968,40 +968,40 @@
   1.594  apply (auto simp: face_of_singleton hull_same)
   1.595  done
   1.596  
   1.597 -subsection\<open>Facets\<close>
   1.598 -
   1.599 -definition facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   1.600 +subsection%important\<open>Facets\<close>
   1.601 +
   1.602 +definition%important facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   1.603                      (infixr "(facet'_of)" 50)
   1.604    where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
   1.605  
   1.606 -lemma facet_of_empty [simp]: "~ S facet_of {}"
   1.607 +lemma%unimportant facet_of_empty [simp]: "~ S facet_of {}"
   1.608    by (simp add: facet_of_def)
   1.609  
   1.610 -lemma facet_of_irrefl [simp]: "~ S facet_of S "
   1.611 +lemma%unimportant facet_of_irrefl [simp]: "~ S facet_of S "
   1.612    by (simp add: facet_of_def)
   1.613  
   1.614 -lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   1.615 +lemma%unimportant facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   1.616    by (simp add: facet_of_def)
   1.617  
   1.618 -lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   1.619 +lemma%unimportant facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   1.620    by (simp add: face_of_imp_subset facet_of_def)
   1.621  
   1.622 -lemma hyperplane_facet_of_halfspace_le:
   1.623 +lemma%unimportant hyperplane_facet_of_halfspace_le:
   1.624     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
   1.625  unfolding facet_of_def hyperplane_eq_empty
   1.626  by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
   1.627             DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
   1.628  
   1.629 -lemma hyperplane_facet_of_halfspace_ge:
   1.630 +lemma%unimportant hyperplane_facet_of_halfspace_ge:
   1.631      "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
   1.632  unfolding facet_of_def hyperplane_eq_empty
   1.633  by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
   1.634             DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
   1.635  
   1.636 -lemma facet_of_halfspace_le:
   1.637 +lemma%important facet_of_halfspace_le:
   1.638      "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   1.639      (is "?lhs = ?rhs")
   1.640 -proof
   1.641 +proof%unimportant
   1.642    assume c: ?lhs
   1.643    with c facet_of_irrefl show ?rhs
   1.644      by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
   1.645 @@ -1010,26 +1010,26 @@
   1.646      by (simp add: hyperplane_facet_of_halfspace_le)
   1.647  qed
   1.648  
   1.649 -lemma facet_of_halfspace_ge:
   1.650 +lemma%unimportant facet_of_halfspace_ge:
   1.651      "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   1.652  using facet_of_halfspace_le [of F "-a" "-b"] by simp
   1.653  
   1.654 -subsection \<open>Edges: faces of affine dimension 1\<close>
   1.655 -
   1.656 -definition edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   1.657 +subsection%important \<open>Edges: faces of affine dimension 1\<close>
   1.658 +
   1.659 +definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   1.660    where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
   1.661  
   1.662 -lemma edge_of_imp_subset:
   1.663 +lemma%unimportant edge_of_imp_subset:
   1.664     "S edge_of T \<Longrightarrow> S \<subseteq> T"
   1.665  by (simp add: edge_of_def face_of_imp_subset)
   1.666  
   1.667 -subsection\<open>Existence of extreme points\<close>
   1.668 -
   1.669 -lemma different_norm_3_collinear_points:
   1.670 +subsection%important\<open>Existence of extreme points\<close>
   1.671 +
   1.672 +lemma%important different_norm_3_collinear_points:
   1.673    fixes a :: "'a::euclidean_space"
   1.674    assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
   1.675    shows False
   1.676 -proof -
   1.677 +proof%unimportant -
   1.678    obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
   1.679               and "a \<noteq> b"
   1.680               and u01: "0 < u" "u < 1"
   1.681 @@ -1050,11 +1050,11 @@
   1.682      using \<open>a \<noteq> b\<close> by force
   1.683  qed
   1.684  
   1.685 -proposition extreme_point_exists_convex:
   1.686 +proposition%important extreme_point_exists_convex:
   1.687    fixes S :: "'a::euclidean_space set"
   1.688    assumes "compact S" "convex S" "S \<noteq> {}"
   1.689    obtains x where "x extreme_point_of S"
   1.690 -proof -
   1.691 +proof%unimportant -
   1.692    obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
   1.693      using distance_attains_sup [of S 0] assms by auto
   1.694    have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
   1.695 @@ -1099,13 +1099,13 @@
   1.696      done
   1.697  qed
   1.698  
   1.699 -subsection\<open>Krein-Milman, the weaker form\<close>
   1.700 -
   1.701 -proposition Krein_Milman:
   1.702 +subsection%important\<open>Krein-Milman, the weaker form\<close>
   1.703 +
   1.704 +proposition%important Krein_Milman:
   1.705    fixes S :: "'a::euclidean_space set"
   1.706    assumes "compact S" "convex S"
   1.707      shows "S = closure(convex hull {x. x extreme_point_of S})"
   1.708 -proof (cases "S = {}")
   1.709 +proof%unimportant (cases "S = {}")
   1.710    case True then show ?thesis   by simp
   1.711  next
   1.712    case False
   1.713 @@ -1155,12 +1155,12 @@
   1.714  
   1.715  text\<open>Now the sharper form.\<close>
   1.716  
   1.717 -lemma Krein_Milman_Minkowski_aux:
   1.718 +lemma%important Krein_Milman_Minkowski_aux:
   1.719    fixes S :: "'a::euclidean_space set"
   1.720    assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
   1.721      shows "0 \<in> convex hull {x. x extreme_point_of S}"
   1.722  using n S
   1.723 -proof (induction n arbitrary: S rule: less_induct)
   1.724 +proof%unimportant (induction n arbitrary: S rule: less_induct)
   1.725    case (less n S) show ?case
   1.726    proof (cases "0 \<in> rel_interior S")
   1.727      case True with Krein_Milman show ?thesis
   1.728 @@ -1197,11 +1197,11 @@
   1.729  qed
   1.730  
   1.731  
   1.732 -theorem Krein_Milman_Minkowski:
   1.733 +theorem%important Krein_Milman_Minkowski:
   1.734    fixes S :: "'a::euclidean_space set"
   1.735    assumes "compact S" "convex S"
   1.736      shows "S = convex hull {x. x extreme_point_of S}"
   1.737 -proof
   1.738 +proof%unimportant
   1.739    show "S \<subseteq> convex hull {x. x extreme_point_of S}"
   1.740    proof
   1.741      fix a assume [simp]: "a \<in> S"
   1.742 @@ -1225,17 +1225,17 @@
   1.743  qed
   1.744  
   1.745  
   1.746 -subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
   1.747 -
   1.748 -lemma Krein_Milman_polytope:
   1.749 +subsection%important\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
   1.750 +
   1.751 +lemma%important Krein_Milman_polytope:
   1.752    fixes S :: "'a::euclidean_space set"
   1.753    shows
   1.754     "finite S
   1.755         \<Longrightarrow> convex hull S =
   1.756             convex hull {x. x extreme_point_of (convex hull S)}"
   1.757 -by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
   1.758 -
   1.759 -lemma extreme_points_of_convex_hull_eq:
   1.760 +by%unimportant (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
   1.761 +
   1.762 +lemma%unimportant extreme_points_of_convex_hull_eq:
   1.763    fixes S :: "'a::euclidean_space set"
   1.764    shows
   1.765     "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
   1.766 @@ -1243,18 +1243,18 @@
   1.767  by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
   1.768  
   1.769  
   1.770 -lemma extreme_point_of_convex_hull_eq:
   1.771 +lemma%unimportant extreme_point_of_convex_hull_eq:
   1.772    fixes S :: "'a::euclidean_space set"
   1.773    shows
   1.774     "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
   1.775      \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
   1.776  using extreme_points_of_convex_hull_eq by auto
   1.777  
   1.778 -lemma extreme_point_of_convex_hull_convex_independent:
   1.779 +lemma%important extreme_point_of_convex_hull_convex_independent:
   1.780    fixes S :: "'a::euclidean_space set"
   1.781    assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
   1.782    shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
   1.783 -proof -
   1.784 +proof%unimportant -
   1.785    have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
   1.786    proof -
   1.787      obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
   1.788 @@ -1265,7 +1265,7 @@
   1.789      by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
   1.790  qed
   1.791  
   1.792 -lemma extreme_point_of_convex_hull_affine_independent:
   1.793 +lemma%unimportant extreme_point_of_convex_hull_affine_independent:
   1.794    fixes S :: "'a::euclidean_space set"
   1.795    shows
   1.796     "~ affine_dependent S
   1.797 @@ -1273,7 +1273,7 @@
   1.798  by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
   1.799  
   1.800  text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
   1.801 -lemma extreme_point_of_convex_hull_2:
   1.802 +lemma%unimportant extreme_point_of_convex_hull_2:
   1.803    fixes x :: "'a::euclidean_space"
   1.804    shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
   1.805  proof -
   1.806 @@ -1283,13 +1283,13 @@
   1.807      by simp
   1.808  qed
   1.809  
   1.810 -lemma extreme_point_of_segment:
   1.811 +lemma%unimportant extreme_point_of_segment:
   1.812    fixes x :: "'a::euclidean_space"
   1.813    shows
   1.814     "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
   1.815  by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
   1.816  
   1.817 -lemma face_of_convex_hull_subset:
   1.818 +lemma%unimportant face_of_convex_hull_subset:
   1.819    fixes S :: "'a::euclidean_space set"
   1.820    assumes "compact S" and T: "T face_of (convex hull S)"
   1.821    obtains s' where "s' \<subseteq> S" "T = convex hull s'"
   1.822 @@ -1298,11 +1298,11 @@
   1.823  by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
   1.824  
   1.825  
   1.826 -lemma face_of_convex_hull_aux:
   1.827 +lemma%important face_of_convex_hull_aux:
   1.828    assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
   1.829      and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
   1.830    shows "p \<in> S"
   1.831 -proof -
   1.832 +proof%unimportant -
   1.833    have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
   1.834      by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
   1.835    moreover have "affine hull {a,b,c} \<subseteq> S"
   1.836 @@ -1317,14 +1317,14 @@
   1.837    ultimately show ?thesis by force
   1.838  qed
   1.839  
   1.840 -proposition face_of_convex_hull_insert_eq:
   1.841 +proposition%important face_of_convex_hull_insert_eq:
   1.842    fixes a :: "'a :: euclidean_space"
   1.843    assumes "finite S" and a: "a \<notin> affine hull S"
   1.844    shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
   1.845            F face_of (convex hull S) \<or>
   1.846            (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
   1.847           (is "F face_of ?CAS \<longleftrightarrow> _")
   1.848 -proof safe
   1.849 +proof%unimportant safe
   1.850    assume F: "F face_of ?CAS"
   1.851      and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
   1.852    obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
   1.853 @@ -1465,18 +1465,18 @@
   1.854    qed
   1.855  qed
   1.856  
   1.857 -lemma face_of_convex_hull_insert2:
   1.858 +lemma%unimportant face_of_convex_hull_insert2:
   1.859    fixes a :: "'a :: euclidean_space"
   1.860    assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
   1.861    shows "convex hull (insert a F) face_of convex hull (insert a S)"
   1.862    by (metis F face_of_convex_hull_insert_eq [OF S a])
   1.863  
   1.864 -proposition face_of_convex_hull_affine_independent:
   1.865 +proposition%important face_of_convex_hull_affine_independent:
   1.866    fixes S :: "'a::euclidean_space set"
   1.867    assumes "~ affine_dependent S"
   1.868      shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
   1.869            (is "?lhs = ?rhs")
   1.870 -proof
   1.871 +proof%unimportant
   1.872    assume ?lhs
   1.873    then show ?rhs
   1.874      by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
   1.875 @@ -1493,7 +1493,7 @@
   1.876      by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
   1.877  qed
   1.878  
   1.879 -lemma facet_of_convex_hull_affine_independent:
   1.880 +lemma%unimportant facet_of_convex_hull_affine_independent:
   1.881    fixes S :: "'a::euclidean_space set"
   1.882    assumes "~ affine_dependent S"
   1.883      shows "T facet_of (convex hull S) \<longleftrightarrow>
   1.884 @@ -1540,7 +1540,7 @@
   1.885      done
   1.886  qed
   1.887  
   1.888 -lemma facet_of_convex_hull_affine_independent_alt:
   1.889 +lemma%unimportant facet_of_convex_hull_affine_independent_alt:
   1.890    fixes S :: "'a::euclidean_space set"
   1.891    shows
   1.892     "~affine_dependent S
   1.893 @@ -1551,7 +1551,7 @@
   1.894  apply (metis Diff_cancel Int_empty_right Int_insert_right_if1  aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty  not_less_eq_eq numeral_2_eq_2)
   1.895  done
   1.896  
   1.897 -lemma segment_face_of:
   1.898 +lemma%unimportant segment_face_of:
   1.899    assumes "(closed_segment a b) face_of S"
   1.900    shows "a extreme_point_of S" "b extreme_point_of S"
   1.901  proof -
   1.902 @@ -1571,12 +1571,12 @@
   1.903  qed
   1.904  
   1.905  
   1.906 -lemma Krein_Milman_frontier:
   1.907 +lemma%important Krein_Milman_frontier:
   1.908    fixes S :: "'a::euclidean_space set"
   1.909    assumes "convex S" "compact S"
   1.910      shows "S = convex hull (frontier S)"
   1.911            (is "?lhs = ?rhs")
   1.912 -proof
   1.913 +proof%unimportant
   1.914    have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
   1.915      using Krein_Milman_Minkowski assms by blast
   1.916    also have "... \<subseteq> ?rhs"
   1.917 @@ -1593,36 +1593,36 @@
   1.918    finally show "?rhs \<subseteq> ?lhs" .
   1.919  qed
   1.920  
   1.921 -subsection\<open>Polytopes\<close>
   1.922 -
   1.923 -definition polytope where
   1.924 +subsection%important\<open>Polytopes\<close>
   1.925 +
   1.926 +definition%important polytope where
   1.927   "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
   1.928  
   1.929 -lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
   1.930 +lemma%unimportant polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
   1.931  apply (simp add: polytope_def, safe)
   1.932  apply (metis convex_hull_translation finite_imageI translation_galois)
   1.933  by (metis convex_hull_translation finite_imageI)
   1.934  
   1.935 -lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
   1.936 +lemma%unimportant polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
   1.937    unfolding polytope_def using convex_hull_linear_image by blast
   1.938  
   1.939 -lemma polytope_empty: "polytope {}"
   1.940 +lemma%unimportant polytope_empty: "polytope {}"
   1.941    using convex_hull_empty polytope_def by blast
   1.942  
   1.943 -lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
   1.944 +lemma%unimportant polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
   1.945    using polytope_def by auto
   1.946  
   1.947 -lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
   1.948 +lemma%unimportant polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
   1.949    unfolding polytope_def
   1.950    by (metis finite_cartesian_product convex_hull_Times)
   1.951  
   1.952 -lemma face_of_polytope_polytope:
   1.953 +lemma%unimportant face_of_polytope_polytope:
   1.954    fixes S :: "'a::euclidean_space set"
   1.955    shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
   1.956  unfolding polytope_def
   1.957  by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
   1.958  
   1.959 -lemma finite_polytope_faces:
   1.960 +lemma%unimportant finite_polytope_faces:
   1.961    fixes S :: "'a::euclidean_space set"
   1.962    assumes "polytope S"
   1.963    shows "finite {F. F face_of S}"
   1.964 @@ -1637,48 +1637,48 @@
   1.965      by (blast intro: finite_subset)
   1.966  qed
   1.967  
   1.968 -lemma finite_polytope_facets:
   1.969 +lemma%unimportant finite_polytope_facets:
   1.970    assumes "polytope S"
   1.971    shows "finite {T. T facet_of S}"
   1.972  by (simp add: assms facet_of_def finite_polytope_faces)
   1.973  
   1.974 -lemma polytope_scaling:
   1.975 +lemma%unimportant polytope_scaling:
   1.976    assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
   1.977  by (simp add: assms polytope_linear_image)
   1.978  
   1.979 -lemma polytope_imp_compact:
   1.980 +lemma%unimportant polytope_imp_compact:
   1.981    fixes S :: "'a::real_normed_vector set"
   1.982    shows "polytope S \<Longrightarrow> compact S"
   1.983  by (metis finite_imp_compact_convex_hull polytope_def)
   1.984  
   1.985 -lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
   1.986 +lemma%unimportant polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
   1.987    by (metis convex_convex_hull polytope_def)
   1.988  
   1.989 -lemma polytope_imp_closed:
   1.990 +lemma%unimportant polytope_imp_closed:
   1.991    fixes S :: "'a::real_normed_vector set"
   1.992    shows "polytope S \<Longrightarrow> closed S"
   1.993  by (simp add: compact_imp_closed polytope_imp_compact)
   1.994  
   1.995 -lemma polytope_imp_bounded:
   1.996 +lemma%unimportant polytope_imp_bounded:
   1.997    fixes S :: "'a::real_normed_vector set"
   1.998    shows "polytope S \<Longrightarrow> bounded S"
   1.999  by (simp add: compact_imp_bounded polytope_imp_compact)
  1.1000  
  1.1001 -lemma polytope_interval: "polytope(cbox a b)"
  1.1002 +lemma%unimportant polytope_interval: "polytope(cbox a b)"
  1.1003    unfolding polytope_def by (meson closed_interval_as_convex_hull)
  1.1004  
  1.1005 -lemma polytope_sing: "polytope {a}"
  1.1006 +lemma%unimportant polytope_sing: "polytope {a}"
  1.1007    using polytope_def by force
  1.1008  
  1.1009 -lemma face_of_polytope_insert:
  1.1010 +lemma%unimportant face_of_polytope_insert:
  1.1011       "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
  1.1012    by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
  1.1013  
  1.1014 -lemma face_of_polytope_insert2:
  1.1015 +lemma%important face_of_polytope_insert2:
  1.1016    fixes a :: "'a :: euclidean_space"
  1.1017    assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
  1.1018    shows "convex hull (insert a F) face_of convex hull (insert a S)"
  1.1019 -proof -
  1.1020 +proof%unimportant -
  1.1021    obtain V where "finite V" "S = convex hull V"
  1.1022      using assms by (auto simp: polytope_def)
  1.1023    then have "convex hull (insert a F) face_of convex hull (insert a V)"
  1.1024 @@ -1688,31 +1688,31 @@
  1.1025  qed
  1.1026  
  1.1027  
  1.1028 -subsection\<open>Polyhedra\<close>
  1.1029 -
  1.1030 -definition polyhedron where
  1.1031 +subsection%important\<open>Polyhedra\<close>
  1.1032 +
  1.1033 +definition%important polyhedron where
  1.1034   "polyhedron S \<equiv>
  1.1035          \<exists>F. finite F \<and>
  1.1036              S = \<Inter> F \<and>
  1.1037              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
  1.1038  
  1.1039 -lemma polyhedron_Int [intro,simp]:
  1.1040 +lemma%unimportant polyhedron_Int [intro,simp]:
  1.1041     "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
  1.1042    apply (simp add: polyhedron_def, clarify)
  1.1043    apply (rename_tac F G)
  1.1044    apply (rule_tac x="F \<union> G" in exI, auto)
  1.1045    done
  1.1046  
  1.1047 -lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
  1.1048 +lemma%unimportant polyhedron_UNIV [iff]: "polyhedron UNIV"
  1.1049    unfolding polyhedron_def
  1.1050    by (rule_tac x="{}" in exI) auto
  1.1051  
  1.1052 -lemma polyhedron_Inter [intro,simp]:
  1.1053 +lemma%unimportant polyhedron_Inter [intro,simp]:
  1.1054     "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
  1.1055  by (induction F rule: finite_induct) auto
  1.1056  
  1.1057  
  1.1058 -lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
  1.1059 +lemma%unimportant polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
  1.1060  proof -
  1.1061    have "\<exists>a. a \<noteq> 0 \<and>
  1.1062               (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
  1.1063 @@ -1731,7 +1731,7 @@
  1.1064      done
  1.1065  qed
  1.1066  
  1.1067 -lemma polyhedron_halfspace_le:
  1.1068 +lemma%unimportant polyhedron_halfspace_le:
  1.1069    fixes a :: "'a :: euclidean_space"
  1.1070    shows "polyhedron {x. a \<bullet> x \<le> b}"
  1.1071  proof (cases "a = 0")
  1.1072 @@ -1743,53 +1743,53 @@
  1.1073      by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
  1.1074  qed
  1.1075  
  1.1076 -lemma polyhedron_halfspace_ge:
  1.1077 +lemma%unimportant polyhedron_halfspace_ge:
  1.1078    fixes a :: "'a :: euclidean_space"
  1.1079    shows "polyhedron {x. a \<bullet> x \<ge> b}"
  1.1080  using polyhedron_halfspace_le [of "-a" "-b"] by simp
  1.1081  
  1.1082 -lemma polyhedron_hyperplane:
  1.1083 +lemma%important polyhedron_hyperplane:
  1.1084    fixes a :: "'a :: euclidean_space"
  1.1085    shows "polyhedron {x. a \<bullet> x = b}"
  1.1086 -proof -
  1.1087 +proof%unimportant -
  1.1088    have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
  1.1089      by force
  1.1090    then show ?thesis
  1.1091      by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
  1.1092  qed
  1.1093  
  1.1094 -lemma affine_imp_polyhedron:
  1.1095 +lemma%unimportant affine_imp_polyhedron:
  1.1096    fixes S :: "'a :: euclidean_space set"
  1.1097    shows "affine S \<Longrightarrow> polyhedron S"
  1.1098  by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
  1.1099  
  1.1100 -lemma polyhedron_imp_closed:
  1.1101 +lemma%unimportant polyhedron_imp_closed:
  1.1102    fixes S :: "'a :: euclidean_space set"
  1.1103    shows "polyhedron S \<Longrightarrow> closed S"
  1.1104  apply (simp add: polyhedron_def)
  1.1105  using closed_halfspace_le by fastforce
  1.1106  
  1.1107 -lemma polyhedron_imp_convex:
  1.1108 +lemma%unimportant polyhedron_imp_convex:
  1.1109    fixes S :: "'a :: euclidean_space set"
  1.1110    shows "polyhedron S \<Longrightarrow> convex S"
  1.1111  apply (simp add: polyhedron_def)
  1.1112  using convex_Inter convex_halfspace_le by fastforce
  1.1113  
  1.1114 -lemma polyhedron_affine_hull:
  1.1115 +lemma%unimportant polyhedron_affine_hull:
  1.1116    fixes S :: "'a :: euclidean_space set"
  1.1117    shows "polyhedron(affine hull S)"
  1.1118  by (simp add: affine_imp_polyhedron)
  1.1119  
  1.1120  
  1.1121 -subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
  1.1122 -
  1.1123 -lemma polyhedron_Int_affine:
  1.1124 +subsection%important\<open>Canonical polyhedron representation making facial structure explicit\<close>
  1.1125 +
  1.1126 +lemma%important polyhedron_Int_affine:
  1.1127    fixes S :: "'a :: euclidean_space set"
  1.1128    shows "polyhedron S \<longleftrightarrow>
  1.1129             (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1.1130                  (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
  1.1131          (is "?lhs = ?rhs")
  1.1132 -proof
  1.1133 +proof%unimportant
  1.1134    assume ?lhs then show ?rhs
  1.1135      apply (simp add: polyhedron_def)
  1.1136      apply (erule ex_forward)
  1.1137 @@ -1803,13 +1803,13 @@
  1.1138      done
  1.1139  qed
  1.1140  
  1.1141 -proposition rel_interior_polyhedron_explicit:
  1.1142 +proposition%important rel_interior_polyhedron_explicit:
  1.1143    assumes "finite F"
  1.1144        and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1145        and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1.1146        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1.1147      shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
  1.1148 -proof -
  1.1149 +proof%unimportant -
  1.1150    have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
  1.1151      by (meson IntE mem_rel_interior)
  1.1152    moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
  1.1153 @@ -1877,7 +1877,7 @@
  1.1154  qed
  1.1155  
  1.1156  
  1.1157 -lemma polyhedron_Int_affine_parallel:
  1.1158 +lemma%important polyhedron_Int_affine_parallel:
  1.1159    fixes S :: "'a :: euclidean_space set"
  1.1160    shows "polyhedron S \<longleftrightarrow>
  1.1161           (\<exists>F. finite F \<and>
  1.1162 @@ -1885,7 +1885,7 @@
  1.1163                (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1.1164                               (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
  1.1165      (is "?lhs = ?rhs")
  1.1166 -proof
  1.1167 +proof%unimportant
  1.1168    assume ?lhs
  1.1169    then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
  1.1170                    and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1.1171 @@ -1931,7 +1931,7 @@
  1.1172  qed
  1.1173  
  1.1174  
  1.1175 -proposition polyhedron_Int_affine_parallel_minimal:
  1.1176 +proposition%important polyhedron_Int_affine_parallel_minimal:
  1.1177    fixes S :: "'a :: euclidean_space set"
  1.1178    shows "polyhedron S \<longleftrightarrow>
  1.1179           (\<exists>F. finite F \<and>
  1.1180 @@ -1940,7 +1940,7 @@
  1.1181                               (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
  1.1182                (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
  1.1183      (is "?lhs = ?rhs")
  1.1184 -proof
  1.1185 +proof%unimportant
  1.1186    assume ?lhs
  1.1187    then obtain f0
  1.1188             where f0: "finite f0"
  1.1189 @@ -1976,7 +1976,7 @@
  1.1190  qed
  1.1191  
  1.1192  
  1.1193 -lemma polyhedron_Int_affine_minimal:
  1.1194 +lemma%unimportant polyhedron_Int_affine_minimal:
  1.1195    fixes S :: "'a :: euclidean_space set"
  1.1196    shows "polyhedron S \<longleftrightarrow>
  1.1197           (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1.1198 @@ -1987,13 +1987,13 @@
  1.1199  apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
  1.1200  done
  1.1201  
  1.1202 -proposition facet_of_polyhedron_explicit:
  1.1203 +proposition%important facet_of_polyhedron_explicit:
  1.1204    assumes "finite F"
  1.1205        and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1206        and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1.1207        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1.1208      shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
  1.1209 -proof (cases "S = {}")
  1.1210 +proof%unimportant (cases "S = {}")
  1.1211    case True with psub show ?thesis by force
  1.1212  next
  1.1213    case False
  1.1214 @@ -2198,7 +2198,7 @@
  1.1215  qed
  1.1216  
  1.1217  
  1.1218 -lemma face_of_polyhedron_subset_explicit:
  1.1219 +lemma%important face_of_polyhedron_subset_explicit:
  1.1220    fixes S :: "'a :: euclidean_space set"
  1.1221    assumes "finite F"
  1.1222        and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1223 @@ -2206,7 +2206,7 @@
  1.1224        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1.1225        and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  1.1226     obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
  1.1227 -proof -
  1.1228 +proof%unimportant -
  1.1229    have "c \<subseteq> S" using \<open>c face_of S\<close>
  1.1230      by (simp add: face_of_imp_subset)
  1.1231    have "polyhedron S"
  1.1232 @@ -2245,7 +2245,7 @@
  1.1233  qed
  1.1234  
  1.1235  text\<open>Initial part of proof duplicates that above\<close>
  1.1236 -proposition face_of_polyhedron_explicit:
  1.1237 +proposition%important face_of_polyhedron_explicit:
  1.1238    fixes S :: "'a :: euclidean_space set"
  1.1239    assumes "finite F"
  1.1240        and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1241 @@ -2253,7 +2253,7 @@
  1.1242        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1.1243        and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  1.1244      shows "c = \<Inter>{S \<inter> {x. a h \<bullet> x = b h} | h. h \<in> F \<and> c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}"
  1.1245 -proof -
  1.1246 +proof%unimportant -
  1.1247    let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
  1.1248    have "c \<subseteq> S" using \<open>c face_of S\<close>
  1.1249      by (simp add: face_of_imp_subset)
  1.1250 @@ -2359,10 +2359,10 @@
  1.1251  
  1.1252  subsection\<open>More general corollaries from the explicit representation\<close>
  1.1253  
  1.1254 -corollary facet_of_polyhedron:
  1.1255 +corollary%important facet_of_polyhedron:
  1.1256    assumes "polyhedron S" and "c facet_of S"
  1.1257    obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
  1.1258 -proof -
  1.1259 +proof%unimportant -
  1.1260    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1261               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1.1262               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  1.1263 @@ -2379,10 +2379,10 @@
  1.1264      by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
  1.1265  qed
  1.1266  
  1.1267 -corollary face_of_polyhedron:
  1.1268 +corollary%important face_of_polyhedron:
  1.1269    assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  1.1270      shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
  1.1271 -proof -
  1.1272 +proof%unimportant -
  1.1273    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1274               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1.1275               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  1.1276 @@ -2395,14 +2395,14 @@
  1.1277      done
  1.1278  qed
  1.1279  
  1.1280 -lemma face_of_polyhedron_subset_facet:
  1.1281 +lemma%unimportant face_of_polyhedron_subset_facet:
  1.1282    assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  1.1283    obtains F where "F facet_of S" "c \<subseteq> F"
  1.1284  using face_of_polyhedron assms
  1.1285  by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
  1.1286  
  1.1287  
  1.1288 -lemma exposed_face_of_polyhedron:
  1.1289 +lemma%unimportant exposed_face_of_polyhedron:
  1.1290    assumes "polyhedron S"
  1.1291      shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
  1.1292  proof
  1.1293 @@ -2430,12 +2430,12 @@
  1.1294    qed
  1.1295  qed
  1.1296  
  1.1297 -lemma face_of_polyhedron_polyhedron:
  1.1298 +lemma%unimportant face_of_polyhedron_polyhedron:
  1.1299    fixes S :: "'a :: euclidean_space set"
  1.1300    assumes "polyhedron S" "c face_of S" shows "polyhedron c"
  1.1301  by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex)
  1.1302  
  1.1303 -lemma finite_polyhedron_faces:
  1.1304 +lemma%unimportant finite_polyhedron_faces:
  1.1305    fixes S :: "'a :: euclidean_space set"
  1.1306    assumes "polyhedron S"
  1.1307      shows "finite {F. F face_of S}"
  1.1308 @@ -2459,29 +2459,29 @@
  1.1309      by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
  1.1310  qed
  1.1311  
  1.1312 -lemma finite_polyhedron_exposed_faces:
  1.1313 +lemma%unimportant finite_polyhedron_exposed_faces:
  1.1314     "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
  1.1315  using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
  1.1316  
  1.1317 -lemma finite_polyhedron_extreme_points:
  1.1318 +lemma%unimportant finite_polyhedron_extreme_points:
  1.1319    fixes S :: "'a :: euclidean_space set"
  1.1320    shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
  1.1321  apply (simp add: face_of_singleton [symmetric])
  1.1322  apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
  1.1323  done
  1.1324  
  1.1325 -lemma finite_polyhedron_facets:
  1.1326 +lemma%unimportant finite_polyhedron_facets:
  1.1327    fixes S :: "'a :: euclidean_space set"
  1.1328    shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
  1.1329  unfolding facet_of_def
  1.1330  by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
  1.1331  
  1.1332  
  1.1333 -proposition rel_interior_of_polyhedron:
  1.1334 +proposition%important rel_interior_of_polyhedron:
  1.1335    fixes S :: "'a :: euclidean_space set"
  1.1336    assumes "polyhedron S"
  1.1337      shows "rel_interior S = S - \<Union>{F. F facet_of S}"
  1.1338 -proof -
  1.1339 +proof%unimportant -
  1.1340    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  1.1341               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1.1342               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  1.1343 @@ -2521,19 +2521,19 @@
  1.1344      by (force simp: rel)
  1.1345  qed
  1.1346  
  1.1347 -lemma rel_boundary_of_polyhedron:
  1.1348 +lemma%unimportant rel_boundary_of_polyhedron:
  1.1349    fixes S :: "'a :: euclidean_space set"
  1.1350    assumes "polyhedron S"
  1.1351      shows "S - rel_interior S = \<Union> {F. F facet_of S}"
  1.1352  using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
  1.1353  
  1.1354 -lemma rel_frontier_of_polyhedron:
  1.1355 +lemma%unimportant rel_frontier_of_polyhedron:
  1.1356    fixes S :: "'a :: euclidean_space set"
  1.1357    assumes "polyhedron S"
  1.1358      shows "rel_frontier S = \<Union> {F. F facet_of S}"
  1.1359  by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
  1.1360  
  1.1361 -lemma rel_frontier_of_polyhedron_alt:
  1.1362 +lemma%unimportant rel_frontier_of_polyhedron_alt:
  1.1363    fixes S :: "'a :: euclidean_space set"
  1.1364    assumes "polyhedron S"
  1.1365      shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
  1.1366 @@ -2544,11 +2544,11 @@
  1.1367  
  1.1368  text\<open>A characterization of polyhedra as having finitely many faces\<close>
  1.1369  
  1.1370 -proposition polyhedron_eq_finite_exposed_faces:
  1.1371 +proposition%important polyhedron_eq_finite_exposed_faces:
  1.1372    fixes S :: "'a :: euclidean_space set"
  1.1373    shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
  1.1374           (is "?lhs = ?rhs")
  1.1375 -proof
  1.1376 +proof%unimportant
  1.1377    assume ?lhs
  1.1378    then show ?rhs
  1.1379      by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
  1.1380 @@ -2635,11 +2635,11 @@
  1.1381    qed
  1.1382  qed
  1.1383  
  1.1384 -corollary polyhedron_eq_finite_faces:
  1.1385 +corollary%important polyhedron_eq_finite_faces:
  1.1386    fixes S :: "'a :: euclidean_space set"
  1.1387    shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
  1.1388           (is "?lhs = ?rhs")
  1.1389 -proof
  1.1390 +proof%unimportant
  1.1391    assume ?lhs
  1.1392    then show ?rhs
  1.1393      by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
  1.1394 @@ -2649,7 +2649,7 @@
  1.1395      by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
  1.1396  qed
  1.1397  
  1.1398 -lemma polyhedron_linear_image_eq:
  1.1399 +lemma%unimportant polyhedron_linear_image_eq:
  1.1400    fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
  1.1401    assumes "linear h" "bij h"
  1.1402      shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
  1.1403 @@ -2669,19 +2669,19 @@
  1.1404      done
  1.1405  qed
  1.1406  
  1.1407 -lemma polyhedron_negations:
  1.1408 +lemma%unimportant polyhedron_negations:
  1.1409    fixes S :: "'a :: euclidean_space set"
  1.1410    shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
  1.1411    by (subst polyhedron_linear_image_eq)
  1.1412      (auto simp: bij_uminus intro!: linear_uminus)
  1.1413  
  1.1414 -subsection\<open>Relation between polytopes and polyhedra\<close>
  1.1415 -
  1.1416 -lemma polytope_eq_bounded_polyhedron:
  1.1417 +subsection%important\<open>Relation between polytopes and polyhedra\<close>
  1.1418 +
  1.1419 +lemma%important polytope_eq_bounded_polyhedron:
  1.1420    fixes S :: "'a :: euclidean_space set"
  1.1421    shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
  1.1422           (is "?lhs = ?rhs")
  1.1423 -proof
  1.1424 +proof%unimportant
  1.1425    assume ?lhs
  1.1426    then show ?rhs
  1.1427      by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
  1.1428 @@ -2694,28 +2694,28 @@
  1.1429      done
  1.1430  qed
  1.1431  
  1.1432 -lemma polytope_Int:
  1.1433 +lemma%unimportant polytope_Int:
  1.1434    fixes S :: "'a :: euclidean_space set"
  1.1435    shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  1.1436  by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
  1.1437  
  1.1438  
  1.1439 -lemma polytope_Int_polyhedron:
  1.1440 +lemma%important polytope_Int_polyhedron:
  1.1441    fixes S :: "'a :: euclidean_space set"
  1.1442    shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  1.1443 -by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  1.1444 -
  1.1445 -lemma polyhedron_Int_polytope:
  1.1446 +by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  1.1447 +
  1.1448 +lemma%important polyhedron_Int_polytope:
  1.1449    fixes S :: "'a :: euclidean_space set"
  1.1450    shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  1.1451 -by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  1.1452 -
  1.1453 -lemma polytope_imp_polyhedron:
  1.1454 +by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  1.1455 +
  1.1456 +lemma%important polytope_imp_polyhedron:
  1.1457    fixes S :: "'a :: euclidean_space set"
  1.1458    shows "polytope S \<Longrightarrow> polyhedron S"
  1.1459 -by (simp add: polytope_eq_bounded_polyhedron)
  1.1460 -
  1.1461 -lemma polytope_facet_exists:
  1.1462 +by%unimportant (simp add: polytope_eq_bounded_polyhedron)
  1.1463 +
  1.1464 +lemma%unimportant polytope_facet_exists:
  1.1465    fixes p :: "'a :: euclidean_space set"
  1.1466    assumes "polytope p" "0 < aff_dim p"
  1.1467    obtains F where "F facet_of p"
  1.1468 @@ -2732,16 +2732,16 @@
  1.1469         all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
  1.1470  qed
  1.1471  
  1.1472 -lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
  1.1473 +lemma%unimportant polyhedron_interval [iff]: "polyhedron(cbox a b)"
  1.1474  by (metis polytope_imp_polyhedron polytope_interval)
  1.1475  
  1.1476 -lemma polyhedron_convex_hull:
  1.1477 +lemma%unimportant polyhedron_convex_hull:
  1.1478    fixes S :: "'a :: euclidean_space set"
  1.1479    shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
  1.1480  by (simp add: polytope_convex_hull polytope_imp_polyhedron)
  1.1481  
  1.1482  
  1.1483 -subsection\<open>Relative and absolute frontier of a polytope\<close>
  1.1484 +subsection%important\<open>Relative and absolute frontier of a polytope\<close>
  1.1485  
  1.1486  lemma rel_boundary_of_convex_hull:
  1.1487      fixes S :: "'a::euclidean_space set"
  1.1488 @@ -3194,9 +3194,9 @@
  1.1489    qed (use C in auto)
  1.1490  qed
  1.1491  
  1.1492 -subsection\<open>Simplicial complexes and triangulations\<close>
  1.1493 -
  1.1494 -definition simplicial_complex where
  1.1495 +subsection%important \<open>Simplicial complexes and triangulations\<close>
  1.1496 +
  1.1497 +definition%important simplicial_complex where
  1.1498   "simplicial_complex \<C> \<equiv>
  1.1499          finite \<C> \<and>
  1.1500          (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
  1.1501 @@ -3204,7 +3204,7 @@
  1.1502          (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
  1.1503                  \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
  1.1504  
  1.1505 -definition triangulation where
  1.1506 +definition%important triangulation where
  1.1507   "triangulation \<T> \<equiv>
  1.1508          finite \<T> \<and>
  1.1509          (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
  1.1510 @@ -3212,9 +3212,9 @@
  1.1511                  \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
  1.1512  
  1.1513  
  1.1514 -subsection\<open>Refining a cell complex to a simplicial complex\<close>
  1.1515 -
  1.1516 -lemma convex_hull_insert_Int_eq:
  1.1517 +subsection%important\<open>Refining a cell complex to a simplicial complex\<close>
  1.1518 +
  1.1519 +lemma%important convex_hull_insert_Int_eq:
  1.1520    fixes z :: "'a :: euclidean_space"
  1.1521    assumes z: "z \<in> rel_interior S"
  1.1522        and T: "T \<subseteq> rel_frontier S"
  1.1523 @@ -3222,7 +3222,7 @@
  1.1524        and "convex S" "convex T" "convex U"
  1.1525    shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
  1.1526      (is "?lhs = ?rhs")
  1.1527 -proof
  1.1528 +proof%unimportant
  1.1529    show "?lhs \<subseteq> ?rhs"
  1.1530    proof (cases "T={} \<or> U={}")
  1.1531      case True then show ?thesis by auto
  1.1532 @@ -3294,7 +3294,7 @@
  1.1533      by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
  1.1534  qed
  1.1535  
  1.1536 -lemma simplicial_subdivision_aux:
  1.1537 +lemma%important simplicial_subdivision_aux:
  1.1538    assumes "finite \<M>"
  1.1539        and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1540        and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
  1.1541 @@ -3306,7 +3306,7 @@
  1.1542                  (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
  1.1543                  (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
  1.1544    using assms
  1.1545 -proof (induction n arbitrary: \<M> rule: less_induct)
  1.1546 +proof%unimportant (induction n arbitrary: \<M> rule: less_induct)
  1.1547    case (less n)
  1.1548    then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1549        and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
  1.1550 @@ -3756,7 +3756,7 @@
  1.1551  qed
  1.1552  
  1.1553  
  1.1554 -lemma simplicial_subdivision_of_cell_complex_lowdim:
  1.1555 +lemma%important simplicial_subdivision_of_cell_complex_lowdim:
  1.1556    assumes "finite \<M>"
  1.1557        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1558        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
  1.1559 @@ -3765,7 +3765,7 @@
  1.1560                    "\<Union>\<T> = \<Union>\<M>"
  1.1561                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  1.1562                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  1.1563 -proof (cases "d \<ge> 0")
  1.1564 +proof%unimportant (cases "d \<ge> 0")
  1.1565    case True
  1.1566    then obtain n where n: "d = of_nat n"
  1.1567      using zero_le_imp_eq_int by blast
  1.1568 @@ -3822,7 +3822,7 @@
  1.1569    qed auto
  1.1570  qed
  1.1571  
  1.1572 -proposition simplicial_subdivision_of_cell_complex:
  1.1573 +proposition%important simplicial_subdivision_of_cell_complex:
  1.1574    assumes "finite \<M>"
  1.1575        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1576        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
  1.1577 @@ -3830,9 +3830,9 @@
  1.1578                    "\<Union>\<T> = \<Union>\<M>"
  1.1579                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  1.1580                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  1.1581 -  by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
  1.1582 -
  1.1583 -corollary fine_simplicial_subdivision_of_cell_complex:
  1.1584 +  by%unimportant (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
  1.1585 +
  1.1586 +corollary%important fine_simplicial_subdivision_of_cell_complex:
  1.1587    assumes "0 < e" "finite \<M>"
  1.1588        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1589        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
  1.1590 @@ -3841,7 +3841,7 @@
  1.1591                    "\<Union>\<T> = \<Union>\<M>"
  1.1592                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  1.1593                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  1.1594 -proof -
  1.1595 +proof%unimportant -
  1.1596    obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
  1.1597                and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
  1.1598                 and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  1.1599 @@ -3880,13 +3880,13 @@
  1.1600    qed
  1.1601  qed
  1.1602  
  1.1603 -subsection\<open>Some results on cell division with full-dimensional cells only\<close>
  1.1604 -
  1.1605 -lemma convex_Union_fulldim_cells:
  1.1606 +subsection%important\<open>Some results on cell division with full-dimensional cells only\<close>
  1.1607 +
  1.1608 +lemma%important convex_Union_fulldim_cells:
  1.1609    assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
  1.1610        and eq: "\<Union>\<S> = U"and  "convex U"
  1.1611   shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
  1.1612 -proof -
  1.1613 +proof%unimportant -
  1.1614    have "closed U"
  1.1615      using \<open>finite \<S>\<close> clo eq by blast
  1.1616    have "?lhs \<subseteq> U"
  1.1617 @@ -3935,7 +3935,7 @@
  1.1618    ultimately show ?thesis by blast
  1.1619  qed
  1.1620  
  1.1621 -proposition fine_triangular_subdivision_of_cell_complex:
  1.1622 +proposition%important fine_triangular_subdivision_of_cell_complex:
  1.1623    assumes "0 < e" "finite \<M>"
  1.1624        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  1.1625        and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
  1.1626 @@ -3944,7 +3944,7 @@
  1.1627                   "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
  1.1628                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
  1.1629                   "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
  1.1630 -proof -
  1.1631 +proof%unimportant -
  1.1632    obtain \<T> where "simplicial_complex \<T>"
  1.1633               and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
  1.1634               and "\<Union>\<T> = \<Union>\<M>"