src/HOL/Library/Convex.thy
changeset 44890 22f665a2e91c
parent 44282 f0de18b62d63
child 49609 89e10ed7668b
     1.1 --- a/src/HOL/Library/Convex.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4      hence "(\<Sum> j \<in> s. a j) = 0"
     1.5        using asms by auto
     1.6      hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
     1.7 -      using setsum_nonneg_0[where 'b=real] asms by fastsimp
     1.8 +      using setsum_nonneg_0[where 'b=real] asms by fastforce
     1.9      hence ?case using asms by auto }
    1.10    moreover
    1.11    { assume asm: "a i \<noteq> 1"
    1.12 @@ -125,13 +125,13 @@
    1.13      { fix j assume "j \<in> s"
    1.14        hence "?a j \<ge> 0"
    1.15          using i0 asms divide_nonneg_pos
    1.16 -        by fastsimp } note a_nonneg = this
    1.17 +        by fastforce } note a_nonneg = this
    1.18      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
    1.19 -    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
    1.20 +    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
    1.21      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
    1.22      hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
    1.23      from this asms
    1.24 -    have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
    1.25 +    have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastforce
    1.26      hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
    1.27        using asms[unfolded convex_def, rule_format] yai ai1 by auto
    1.28      hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C"
    1.29 @@ -256,7 +256,7 @@
    1.30      using assms(4,5) by (auto simp add: mult_left_mono add_mono)
    1.31    also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
    1.32    finally show ?thesis
    1.33 -    using assms unfolding convex_on_def by fastsimp
    1.34 +    using assms unfolding convex_on_def by fastforce
    1.35  qed
    1.36  
    1.37  lemma convex_distance[intro]:
    1.38 @@ -363,7 +363,7 @@
    1.39      hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
    1.40      hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
    1.41        by (auto simp add: add_pos_pos mult_pos_pos) }
    1.42 -  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
    1.43 +  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
    1.44  qed
    1.45  
    1.46  lemma convex_on_setsum:
    1.47 @@ -393,7 +393,7 @@
    1.48      hence "(\<Sum> j \<in> s. a j) = 0"
    1.49        using asms by auto
    1.50      hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
    1.51 -      using setsum_nonneg_0[where 'b=real] asms by fastsimp
    1.52 +      using setsum_nonneg_0[where 'b=real] asms by fastforce
    1.53      hence ?case using asms by auto }
    1.54    moreover
    1.55    { assume asm: "a i \<noteq> 1"
    1.56 @@ -406,9 +406,9 @@
    1.57      { fix j assume "j \<in> s"
    1.58        hence "?a j \<ge> 0"
    1.59          using i0 asms divide_nonneg_pos
    1.60 -        by fastsimp } note a_nonneg = this
    1.61 +        by fastforce } note a_nonneg = this
    1.62      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
    1.63 -    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
    1.64 +    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
    1.65      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
    1.66      hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
    1.67      have "convex C" using asms by auto
    1.68 @@ -497,7 +497,7 @@
    1.69    let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
    1.70    assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
    1.71    hence "1 - \<mu> \<ge> 0" by auto
    1.72 -  hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
    1.73 +  hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
    1.74    have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
    1.75              \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
    1.76      using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
    1.77 @@ -550,7 +550,7 @@
    1.78          THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
    1.79        by auto
    1.80      hence "z1 \<in> C" using atMostAtLeast_subset_convex
    1.81 -      `convex C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
    1.82 +      `convex C` `x \<in> C` `y \<in> C` `x < y` by fastforce
    1.83      from z1 have z1': "f x - f y = (x - y) * f' z1"
    1.84        by (simp add:field_simps)
    1.85      obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
    1.86 @@ -567,7 +567,7 @@
    1.87      finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
    1.88      have A': "y - z1 \<ge> 0" using z1 by auto
    1.89      have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
    1.90 -      `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
    1.91 +      `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
    1.92      hence B': "f'' z3 \<ge> 0" using assms by auto
    1.93      from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
    1.94      from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
    1.95 @@ -582,7 +582,7 @@
    1.96      finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
    1.97      have A: "z1 - x \<ge> 0" using z1 by auto
    1.98      have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
    1.99 -      `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
   1.100 +      `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
   1.101      hence B: "f'' z2 \<ge> 0" using assms by auto
   1.102      from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
   1.103      from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
   1.104 @@ -608,7 +608,7 @@
   1.105    assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
   1.106    assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   1.107    shows "convex_on C f"
   1.108 -using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
   1.109 +using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
   1.110  
   1.111  lemma minus_log_convex:
   1.112    fixes b :: real