src/HOL/Library/Convex_Euclidean_Space.thy
 changeset 33269 3b7e2dbbd684 parent 32960 69916a850301
```     1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
1.3 @@ -1133,7 +1133,7 @@
1.4      hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
1.5        apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
1.6        apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
1.7 -  thus ?thesis unfolding convex_def cone_def by blast
1.8 +  thus ?thesis unfolding convex_def cone_def by auto
1.9  qed
1.10
1.11  lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
1.12 @@ -1742,17 +1742,16 @@
1.13      using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
1.14      using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
1.15    hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
1.16 -  def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
1.17 +  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
1.18    show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
1.19      apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
1.20      from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
1.21        apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
1.22 -    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
1.23 +    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
1.24      fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
1.25    next
1.26      fix x assume "x\<in>s"
1.27 -    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
1.28 -      unfolding setle_def
1.29 +    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
1.30        using ab[THEN bspec[where x=x]] by auto
1.31      thus "k + b / 2 < inner a x" using `0 < b` by auto
1.32    qed
1.33 @@ -1794,11 +1793,20 @@
1.34    assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
1.35    shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
1.36  proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
1.37 -  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"  using assms(3-5) by auto
1.38 -  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
1.39 -  thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
1.40 -    apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
1.41 -    prefer 4 using assms(3-5) by blast+ qed
1.42 +  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
1.43 +    using assms(3-5) by auto
1.44 +  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
1.45 +    by (force simp add: inner_diff)
1.46 +  thus ?thesis
1.47 +    apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
1.48 +    apply auto
1.49 +    apply (rule Sup[THEN isLubD2])
1.50 +    prefer 4
1.51 +    apply (rule Sup_least)
1.52 +     using assms(3-5) apply (auto simp add: setle_def)
1.53 +    apply (metis COMBC_def Collect_def Collect_mem_eq)
1.54 +    done
1.55 +qed
1.56
1.57  subsection {* More convexity generalities. *}
1.58
1.59 @@ -2571,12 +2579,17 @@
1.60      thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
1.61        by(auto simp add: vector_component_simps) qed
1.62    hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
1.63 -    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
1.64 -  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
1.65 -
1.66 -subsection {* Line segments, starlike sets etc.                                         *)
1.67 -(* Use the same overloading tricks as for intervals, so that                 *)
1.68 -(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *}
1.69 +    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
1.70 +    apply force
1.71 +    done
1.72 +  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
1.73 +    using `d>0` by auto
1.74 +qed
1.75 +
1.76 +subsection {* Line segments, Starlike Sets, etc.*}
1.77 +
1.78 +(* Use the same overloading tricks as for intervals, so that
1.79 +   segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
1.80
1.81  definition
1.82    midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
```