author paulson Mon, 18 Apr 2016 16:50:19 +0100 changeset 63018 ae2ec7d86ad4 parent 63017 00f4461fa99f child 63021 905e15764bb4
tidying some proofs; getting rid of "nonempty_witness"
```--- 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"```
```--- 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)"
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```