--- 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