summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Convex.thy

changeset 61694 | 6571c78c9667 |

parent 61585 | a9599d3d7610 |

child 62376 | 85f38d5f8807 |

1.1 --- a/src/HOL/Library/Convex.thy Tue Nov 17 12:01:19 2015 +0100 1.2 +++ b/src/HOL/Library/Convex.thy Tue Nov 17 12:32:08 2015 +0000 1.3 @@ -884,19 +884,19 @@ 1.4 assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y" 1.5 def z \<equiv> "(1 - t) * x + t * y" 1.6 with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast 1.7 - 1.8 + 1.9 from xy t have xz: "z > x" by (simp add: z_def algebra_simps) 1.10 have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps) 1.11 also from xy t have "... > 0" by (intro mult_pos_pos) simp_all 1.12 finally have yz: "z < y" by simp 1.13 - 1.14 + 1.15 from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>" 1.16 by (intro MVT2) (auto intro!: assms(2)) 1.17 then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto 1.18 from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>" 1.19 by (intro MVT2) (auto intro!: assms(2)) 1.20 then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto 1.21 - 1.22 + 1.23 from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" .. 1.24 also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto 1.25 with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto 1.26 @@ -926,11 +926,11 @@ 1.27 proof (cases y x rule: linorder_cases) 1.28 assume less: "x < y" 1.29 hence d: "d > 0" by (simp add: d_def) 1.30 - from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 1.31 + from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 1.32 by (simp_all add: d_def divide_simps) 1.33 have "f c = f (x + (c - x) * 1)" by simp 1.34 also from less have "1 = ((y - x) / d)" by (simp add: d_def) 1.35 - also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 1.36 + also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 1.37 by (simp add: field_simps) 1.38 also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less 1.39 by (intro convex_onD_Icc) simp_all 1.40 @@ -945,11 +945,11 @@ 1.41 proof (cases y x rule: linorder_cases) 1.42 assume less: "x < y" 1.43 hence d: "d > 0" by (simp add: d_def) 1.44 - from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 1.45 + from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 1.46 by (simp_all add: d_def divide_simps) 1.47 have "f c = f (y - (y - c) * 1)" by simp 1.48 also from less have "1 = ((y - x) / d)" by (simp add: d_def) 1.49 - also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 1.50 + also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 1.51 by (simp add: field_simps) 1.52 also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less 1.53 by (intro convex_onD_Icc) (simp_all add: field_simps)