1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -4506,38 +4506,30 @@
     1.4      apply (erule_tac x="x - y" in ballE)
     1.5      apply (auto simp add: inner_diff)
     1.6      done
     1.7 -  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
     1.8 +  def k \<equiv> "SUP x:t. a \<bullet> x"
     1.9    show ?thesis
    1.10      apply (rule_tac x="-a" in exI)
    1.11      apply (rule_tac x="-(k + b / 2)" in exI)
    1.12 -    apply rule
    1.13 -    apply rule
    1.14 -    defer
    1.15 -    apply rule
    1.16 +    apply (intro conjI ballI)
    1.17      unfolding inner_minus_left and neg_less_iff_less
    1.18    proof -
    1.19 -    from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
    1.20 -      apply (erule_tac x=y in ballE)
    1.21 -      apply (rule setleI)
    1.22 -      using `y \<in> s`
    1.23 -      apply auto
    1.24 -      done
    1.25 -    then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k"
    1.26 +    fix x assume "x \<in> t"
    1.27 +    then have "inner a x - b / 2 < k"
    1.28        unfolding k_def
    1.29 -      apply (rule_tac isLub_cSup)
    1.30 -      using assms(5)
    1.31 -      apply auto
    1.32 -      done
    1.33 -    fix x
    1.34 -    assume "x \<in> t"
    1.35 -    then show "inner a x < (k + b / 2)"
    1.36 -      using `0<b` and isLubD2[OF k, of "inner a x"] by auto
    1.37 +    proof (subst less_cSUP_iff)
    1.38 +      show "t \<noteq> {}" by fact
    1.39 +      show "bdd_above (op \<bullet> a ` t)"
    1.40 +        using ab[rule_format, of y] `y \<in> s`
    1.41 +        by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
    1.42 +    qed (auto intro!: bexI[of _ x] `0<b`)
    1.43 +    then show "inner a x < k + b / 2"
    1.44 +      by auto
    1.45    next
    1.46      fix x
    1.47      assume "x \<in> s"
    1.48      then have "k \<le> inner a x - b"
    1.49        unfolding k_def
    1.50 -      apply (rule_tac cSup_least)
    1.51 +      apply (rule_tac cSUP_least)
    1.52        using assms(5)
    1.53        using ab[THEN bspec[where x=x]]
    1.54        apply auto
    1.55 @@ -4626,20 +4618,14 @@
    1.56    from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
    1.57    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.58      using assms(3-5) by auto
    1.59 -  then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
    1.60 +  then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
    1.61      by (force simp add: inner_diff)
    1.62 -  then show ?thesis
    1.63 -    apply (rule_tac x=a in exI)
    1.64 -    apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI)
    1.65 +  then have bdd: "bdd_above ((op \<bullet> a)`s)"
    1.66 +    using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *])
    1.67 +  show ?thesis
    1.68      using `a\<noteq>0`
    1.69 -    apply auto
    1.70 -    apply (rule isLub_cSup[THEN isLubD2])
    1.71 -    prefer 4
    1.72 -    apply (rule cSup_least)
    1.73 -    using assms(3-5)
    1.74 -    apply (auto simp add: setle_def)
    1.75 -    apply metis
    1.76 -    done
    1.77 +    by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
    1.78 +       (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *)
    1.79  qed
    1.80  
    1.81