src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

 
 lemma radon_ex_lemma:
   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]
     apply (auto simp add: Int_absorb1)
     done

 
 lemma radon:
   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
     apply auto
     done

         prefer 3
         apply rule
       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
       then show ?thesis
         unfolding f using mp(3)[unfolded gh] by blast

     finally show "setsum (op \<bullet> x) Basis < 1" by auto
   qed
 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)
     using as(1)
     apply auto

   (is "_ \<ge> _ + Inf (?F x) * (y - x)")
 proof (cases rule: linorder_cases)
   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)
   ultimately have "K \<in> I" "K < x" "x \<in> I"
     using interior_subset[of I] `x \<in> interior I` by auto

     using `x < y` by (simp add: field_simps)
 next
   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)
   with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
 

     have "(f y - f x) / (y - x) \<le> z"
       by auto
     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"
       by auto
     then show "?F x \<noteq> {}"