# HG changeset patch
# User wenzelm
# Date 1393188327 -3600
# Node ID abec82f4e3e92add19146a1c172431230f5c07d3
# Parent  de2668c504036afc79be3b7ccf8dfd042f5cb7ea
tuned proofs;

diff -r de2668c50403 -r abec82f4e3e9 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Feb 23 21:30:47 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Feb 23 21:45:27 2014 +0100
@@ -4806,8 +4806,10 @@
   assumes "finite c" "affine_dependent c"
   shows "\<exists>u. setsum u c = 0 \<and> (\<exists>v\<in>c. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) c = 0"
 proof -
-  from assms(2)[unfolded affine_dependent_explicit] guess s ..
-  then guess u ..
+  from assms(2)[unfolded affine_dependent_explicit]
+  obtain s u where
+      "finite s" "s \<subseteq> c" "setsum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
+    by blast
   then show ?thesis
     apply (rule_tac x="\<lambda>v. if v\<in>s then u v else 0" in exI)
     unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms(1), symmetric]
@@ -4931,10 +4933,15 @@
   assumes "affine_dependent c"
   obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
 proof -
-  from assms[unfolded affine_dependent_explicit] guess s .. then guess u ..
+  from assms[unfolded affine_dependent_explicit]
+  obtain s u where
+      "finite s" "s \<subseteq> c" "setsum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
+    by blast
   then have *: "finite s" "affine_dependent s" and s: "s \<subseteq> c"
     unfolding affine_dependent_explicit by auto
-  from radon_partition[OF *] guess m .. then guess p ..
+  from radon_partition[OF *]
+  obtain m p where "m \<inter> p = {}" "m \<union> p = s" "convex hull m \<inter> convex hull p \<noteq> {}"
+    by blast
   then show ?thesis
     apply (rule_tac that[of p m])
     using s
@@ -5026,13 +5033,15 @@
       proof -
         fix x
         assume "x \<in> X ` g"
-        then guess y unfolding image_iff ..
+        then obtain y where "y \<in> g" "x = X y"
+          unfolding image_iff ..
         then show "x \<in> \<Inter>h"
           using X[THEN bspec[where x=y]] using * f by auto
       next
         fix x
         assume "x \<in> X ` h"
-        then guess y unfolding image_iff ..
+        then obtain y where "y \<in> h" "x = X y"
+          unfolding image_iff ..
         then show "x \<in> \<Inter>g"
           using X[THEN bspec[where x=y]] using * f by auto
       qed auto
@@ -6746,7 +6755,7 @@
 next
   fix x :: 'a
   assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "setsum (op \<bullet> x) Basis < 1"
-  guess a using UNIV_witness[where 'a='b] ..
+  obtain a :: 'b where "a \<in> UNIV" using UNIV_witness ..
   let ?d = "(1 - setsum (op \<bullet> x) Basis) / real (DIM('a))"
   have "Min ((op \<bullet> x) ` Basis) > 0"
     apply (rule Min_grI)
@@ -8938,14 +8947,16 @@
   assume "x < y"
   moreover
   have "open (interior I)" by auto
-  from openE[OF this `x \<in> interior I`] guess e . note e = this
+  from openE[OF this `x \<in> interior I`]
+  obtain e where e: "0 < e" "ball x e \<subseteq> interior I" .
   moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
   ultimately have "x < t" "t < y" "t \<in> ball x e"
     by (auto simp: dist_real_def field_simps split: split_min)
   with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
 
   have "open (interior I)" by auto
-  from openE[OF this `x \<in> interior I`] guess e .
+  from openE[OF this `x \<in> interior I`]
+  obtain e where "0 < e" "ball x e \<subseteq> interior I" .
   moreover def K \<equiv> "x - e / 2"
   with `0 < e` have "K \<in> ball x e" "K < x"
     by (auto simp: dist_real_def)
@@ -8971,7 +8982,8 @@
   assume "y < x"
   moreover
   have "open (interior I)" by auto
-  from openE[OF this `x \<in> interior I`] guess e . note e = this
+  from openE[OF this `x \<in> interior I`]
+  obtain e where e: "0 < e" "ball x e \<subseteq> interior I" .
   moreover def t \<equiv> "x + e / 2"
   ultimately have "x < t" "t \<in> ball x e"
     by (auto simp: dist_real_def field_simps)
@@ -8990,7 +9002,8 @@
     finally show "(f x - f y) / (x - y) \<le> z" .
   next
     have "open (interior I)" by auto
-    from openE[OF this `x \<in> interior I`] guess e . note e = this
+    from openE[OF this `x \<in> interior I`]
+    obtain e where e: "0 < e" "ball x e \<subseteq> interior I" .
     then have "x + e / 2 \<in> ball x e"
       by (auto simp: dist_real_def)
     with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I"