equal
deleted
inserted
replaced
90 qed |
90 qed |
91 |
91 |
92 lemma log_exp2_le: |
92 lemma log_exp2_le: |
93 assumes "n > 0" |
93 assumes "n > 0" |
94 shows "2 ^ log n \<le> n" |
94 shows "2 ^ log n \<le> n" |
95 using assms proof (induct n rule: log_induct) |
95 using assms |
96 show "2 ^ log 1 \<le> (1 :: nat)" by simp |
96 proof (induct n rule: log_induct) |
|
97 case one |
|
98 then show ?case by simp |
97 next |
99 next |
98 fix n :: nat |
100 case (double n) |
99 assume "n \<ge> 2" |
|
100 with log_mono have "log n \<ge> Suc 0" |
101 with log_mono have "log n \<ge> Suc 0" |
101 by (simp add: log.simps) |
102 by (simp add: log.simps) |
102 assume "2 ^ log (n div 2) \<le> n div 2" |
103 assume "2 ^ log (n div 2) \<le> n div 2" |
103 with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp |
104 with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp |
104 then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp |
105 then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp |
105 with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2" |
106 with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2" |
106 unfolding power_add [symmetric] by simp |
107 unfolding power_add [symmetric] by simp |
107 also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all |
108 also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all |
108 finally show "2 ^ log n \<le> n" . |
109 finally show ?case . |
109 qed |
110 qed |
110 |
111 |
111 |
112 |
112 subsection \<open>Discrete square root\<close> |
113 subsection \<open>Discrete square root\<close> |
113 |
114 |