# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1460994619 -3600
# Node ID ae2ec7d86ad4880934db10c556959d9a24fb942a
# Parent  00f4461fa99f79fd676d737b5ab6f422330d4bfa
tidying some proofs; getting rid of "nonempty_witness"

diff -r 00f4461fa99f -r ae2ec7d86ad4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 18 15:51:48 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 18 16:50:19 2016 +0100
@@ -10808,7 +10808,7 @@
     shows "affine hull (S \<inter> T) = affine hull S"
 by (simp add: affine_hull_convex_Int_nonempty_interior affine_imp_convex assms)
 
-corollary affine_hull_affine_inter_open:
+corollary affine_hull_affine_Int_open:
   fixes S :: "'a::real_normed_vector set"
   assumes "affine S" "open T" "S \<inter> T \<noteq> {}"
     shows "affine hull (S \<inter> T) = affine hull S"
@@ -10826,7 +10826,7 @@
   assumes "openin (subtopology euclidean (affine hull T)) S" "S \<noteq> {}"
     shows "affine hull S = affine hull T"
 using assms unfolding openin_open
-by (metis affine_affine_hull affine_hull_affine_inter_open hull_hull)
+by (metis affine_affine_hull affine_hull_affine_Int_open hull_hull)
 
 corollary affine_hull_open:
   fixes S :: "'a::real_normed_vector set"
diff -r 00f4461fa99f -r ae2ec7d86ad4 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 18 15:51:48 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 18 16:50:19 2016 +0100
@@ -3969,11 +3969,6 @@
   qed
 qed
 
-lemma nonempty_witness:
-  assumes "s \<noteq> {}"
-  obtains x where "x \<in> s"
-  using assms by auto
-
 lemma operative_division:
   fixes f :: "'a::euclidean_space set \<Rightarrow> 'b"
   assumes "monoidal opp"
@@ -4266,7 +4261,7 @@
 next
   case False
   then have e: "e \<ge> 0"
-    by (metis assms(2) norm_ge_zero order_trans nonempty_witness)
+    by (meson ex_in_conv assms(2) norm_ge_zero order_trans)
   have setsum_le: "setsum (content \<circ> snd) p \<le> content (cbox a b)"
     unfolding additive_content_tagged_division[OF p, symmetric] split_def
     by (auto intro: eq_refl)
@@ -6662,20 +6657,16 @@
         fix x' k'
         assume xk': "(x', k') \<in> p"
         fix z
-        assume "z \<in> interior (g ` k)" and "z \<in> interior (g ` k')"
-        then have *: "interior (g ` k) \<inter> interior (g ` k') \<noteq> {}"
-          by auto
+        assume z: "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
         have same: "(x, k) = (x', k')"
           apply -
           apply (rule ccontr)
           apply (drule p(5)[OF xk xk'])
         proof -
           assume as: "interior k \<inter> interior k' = {}"
-          from nonempty_witness[OF *] guess z .
-          then have "z \<in> g ` (interior k \<inter> interior k')"
-            using interior_image_subset[OF assms(4) inj(1)]
-            unfolding image_Int[OF inj(1)]
-            by auto
+          have "z \<in> g ` (interior k \<inter> interior k')"
+            using interior_image_subset[OF assms(4) inj(1)] z
+            unfolding image_Int[OF inj(1)] by blast
           then show False
             using as by blast
         qed