src/HOL/Analysis/Convex_Euclidean_Space.thy
 changeset 68607 67bb59e49834 parent 68527 2f4e2aab190a child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
1.3 @@ -2005,9 +2005,9 @@
1.4    shows "c *\<^sub>R x \<in> cone hull S"
1.5    by (metis assms cone_cone_hull hull_inc mem_cone)
1.6
1.7 -proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
1.8 +proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
1.9    (is "?lhs = ?rhs")
1.10 -proof%unimportant -
1.11 +proof -
1.12    {
1.13      fix x
1.14      assume "x \<in> ?rhs"
1.15 @@ -2089,7 +2089,7 @@
1.16     "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
1.17  by (meson Diff_subset affine_dependent_subset)
1.18
1.19 -proposition%important affine_dependent_explicit:
1.20 +proposition affine_dependent_explicit:
1.21    "affine_dependent p \<longleftrightarrow>
1.22      (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
1.23  proof -
1.24 @@ -2524,7 +2524,7 @@
1.25
1.26  subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
1.27
1.28 -proposition%important convex_hull_indexed:
1.29 +proposition convex_hull_indexed:
1.30    fixes S :: "'a::real_vector set"
1.31    shows "convex hull S =
1.32      {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
1.33 @@ -4020,11 +4020,11 @@
1.34      by (auto simp: convex_hull_explicit)
1.35  qed
1.36
1.37 -theorem%important caratheodory:
1.38 +theorem caratheodory:
1.39    "convex hull p =
1.40      {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
1.41        card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
1.42 -proof%unimportant safe
1.43 +proof safe
1.44    fix x
1.45    assume "x \<in> convex hull p"
1.46    then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
1.47 @@ -5871,10 +5871,10 @@
1.48      done
1.49  qed
1.50
1.53    assumes "affine_dependent c"
1.54    obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
1.55 -proof%unimportant -
1.56 +proof -
1.57    from assms[unfolded affine_dependent_explicit]
1.58    obtain s u where
1.59        "finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
1.60 @@ -5965,12 +5965,12 @@
1.61    qed
1.62  qed
1.63
1.64 -theorem%important helly:
1.65 +theorem helly:
1.66    fixes f :: "'a::euclidean_space set set"
1.67    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
1.68      and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
1.69    shows "\<Inter>f \<noteq> {}"
1.70 -  apply%unimportant (rule helly_induct)
1.71 +  apply (rule helly_induct)
1.72    using assms
1.73    apply auto
1.74    done
```