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