# HG changeset patch
# User wenzelm
# Date 1468663862 -7200
# Node ID 76492eaf3dc1b801559c4ee7d1094f910a55bc7f
# Parent  6c46a1e786da35d32abedcef3fd9412a09109758
tuned proofs;

diff -r 6c46a1e786da -r 76492eaf3dc1 src/HOL/Library/Convex.thy
--- 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
diff -r 6c46a1e786da -r 76492eaf3dc1 src/HOL/Library/Discrete.thy
--- 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