summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 16 Jul 2016 12:11:02 +0200 | |

changeset 63516 | 76492eaf3dc1 |

parent 63515 | 6c46a1e786da |

child 63517 | 8ea738cffabe |

tuned proofs;

src/HOL/Library/Convex.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Discrete.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Convex.thy Sat Jul 16 12:10:37 2016 +0200 +++ b/src/HOL/Library/Convex.thy Sat Jul 16 12:11:02 2016 +0200 @@ -177,16 +177,16 @@ then have "0 \<le> setsum a s" by (simp add: setsum_nonneg) have "a i *\<^sub>R y i + (\<Sum>j\<in>s. a j *\<^sub>R y j) \<in> C" - proof (cases) - assume z: "setsum a s = 0" + proof (cases "setsum a s = 0") + case True with \<open>a i + setsum a s = 1\<close> have "a i = 1" by simp - from setsum_nonneg_0 [OF \<open>finite s\<close> _ z] \<open>\<forall>j\<in>s. 0 \<le> a j\<close> have "\<forall>j\<in>s. a j = 0" + from setsum_nonneg_0 [OF \<open>finite s\<close> _ True] \<open>\<forall>j\<in>s. 0 \<le> a j\<close> have "\<forall>j\<in>s. a j = 0" by simp show ?thesis using \<open>a i = 1\<close> and \<open>\<forall>j\<in>s. a j = 0\<close> and \<open>y i \<in> C\<close> by simp next - assume nz: "setsum a s \<noteq> 0" + case False with \<open>0 \<le> setsum a s\<close> have "0 < setsum a s" by simp then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C" @@ -197,7 +197,7 @@ have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C" by (rule convexD) then show ?thesis - by (simp add: scaleR_setsum_right nz) + by (simp add: scaleR_setsum_right False) qed then show ?case using \<open>finite s\<close> and \<open>i \<notin> s\<close> by simp

--- a/src/HOL/Library/Discrete.thy Sat Jul 16 12:10:37 2016 +0200 +++ b/src/HOL/Library/Discrete.thy Sat Jul 16 12:11:02 2016 +0200 @@ -92,11 +92,12 @@ lemma log_exp2_le: assumes "n > 0" shows "2 ^ log n \<le> n" -using assms proof (induct n rule: log_induct) - show "2 ^ log 1 \<le> (1 :: nat)" by simp + using assms +proof (induct n rule: log_induct) + case one + then show ?case by simp next - fix n :: nat - assume "n \<ge> 2" + case (double n) with log_mono have "log n \<ge> Suc 0" by (simp add: log.simps) assume "2 ^ log (n div 2) \<le> n div 2" @@ -105,7 +106,7 @@ with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2" unfolding power_add [symmetric] by simp also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all - finally show "2 ^ log n \<le> n" . + finally show ?case . qed