summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 23 Feb 2014 21:45:27 +0100 | |

changeset 55697 | abec82f4e3e9 |

parent 55696 | de2668c50403 |

child 55698 | e42e5671612c |

tuned proofs;

src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy | file | annotate | diff | comparison | revisions |

--- 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"