src/HOL/Library/Convex.thy

   case (insert i s) note asms = this
   { assume "a i = 1"
     hence "(\<Sum> j \<in> s. a j) = 0"
       using asms by auto
     hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
-      using setsum_nonneg_0[where 'b=real] asms by fastsimp
+      using setsum_nonneg_0[where 'b=real] asms by fastforce
     hence ?case using asms by auto }
   moreover
   { assume asm: "a i \<noteq> 1"
     from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
     have fis: "finite (insert i s)" using asms by auto

     hence i0: "1 - a i > 0" by auto
     let "?a j" = "a j / (1 - a i)"
     { fix j assume "j \<in> s"
       hence "?a j \<ge> 0"
         using i0 asms divide_nonneg_pos
-        by fastsimp } note a_nonneg = this
+        by fastforce } note a_nonneg = this
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
-    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
     hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     from this asms
-    have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
+    have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastforce
     hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
       using asms[unfolded convex_def, rule_format] yai ai1 by auto
     hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C"
       using scaleR_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j *\<^sub>R y j" s] by auto
     hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" using i0 by auto

   let ?m = "max (f x) (f y)"
   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
     using assms(4,5) by (auto simp add: mult_left_mono add_mono)
   also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
   finally show ?thesis
-    using assms unfolding convex_on_def by fastsimp
+    using assms unfolding convex_on_def by fastforce
 qed
 
 lemma convex_distance[intro]:
   fixes s :: "'a::real_normed_vector set"
   shows "convex_on s (\<lambda>x. dist a x)"

   moreover
   { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
       by (auto simp add: add_pos_pos mult_pos_pos) }
-  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
+  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
 qed
 
 lemma convex_on_setsum:
   fixes a :: "'a \<Rightarrow> real"
   fixes y :: "'a \<Rightarrow> 'b::real_vector"

     by simp
   { assume "a i = 1"
     hence "(\<Sum> j \<in> s. a j) = 0"
       using asms by auto
     hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
-      using setsum_nonneg_0[where 'b=real] asms by fastsimp
+      using setsum_nonneg_0[where 'b=real] asms by fastforce
     hence ?case using asms by auto }
   moreover
   { assume asm: "a i \<noteq> 1"
     from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
     have fis: "finite (insert i s)" using asms by auto

     hence i0: "1 - a i > 0" by auto
     let "?a j" = "a j / (1 - a i)"
     { fix j assume "j \<in> s"
       hence "?a j \<ge> 0"
         using i0 asms divide_nonneg_pos
-        by fastsimp } note a_nonneg = this
+        by fastforce } note a_nonneg = this
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
-    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
     hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     have "convex C" using asms by auto
     hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
       using asms convex_setsum[OF `finite s`

 proof safe
   fix x y \<mu> :: real
   let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
   assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
   hence "1 - \<mu> \<ge> 0" by auto
-  hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
+  hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
   have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
             \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
     using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
       mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
   hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"

     then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
       using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `y \<in> C` `x < y`],
         THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
       by auto
     hence "z1 \<in> C" using atMostAtLeast_subset_convex
-      `convex C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
+      `convex C` `x \<in> C` `y \<in> C` `x < y` by fastforce
     from z1 have z1': "f x - f y = (x - y) * f' z1"
       by (simp add:field_simps)
     obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
       using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `z1 \<in> C` `x < z1`],
         THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1

       using asm z1' by auto
     also have "\<dots> = (y - z1) * f'' z3" using z3 by auto
     finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
     have A': "y - z1 \<ge> 0" using z1 by auto
     have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
-      `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
+      `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
     hence B': "f'' z3 \<ge> 0" using assms by auto
     from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
     from mult_right_mono_neg[OF this le(2)]
     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"

       using asm z1 by auto
     also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto
     finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
     have A: "z1 - x \<ge> 0" using z1 by auto
     have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
-      `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
+      `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
     hence B: "f'' z2 \<ge> 0" using assms by auto
     from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
     from mult_right_mono[OF this ge(2)]
     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"

   assumes conv: "convex C"
   assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
   assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
   assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   shows "convex_on C f"
-using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
+using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
 
 lemma minus_log_convex:
   fixes b :: real
   assumes "b > 1"
   shows "convex_on {0 <..} (\<lambda> x. - log b x)"