equal
deleted
inserted
replaced
26 0 < n div 2 \<Longrightarrow> P (n div 2)" |
26 0 < n div 2 \<Longrightarrow> P (n div 2)" |
27 then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp |
27 then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp |
28 assume "n > 0" |
28 assume "n > 0" |
29 show "P n" |
29 show "P n" |
30 proof (cases "n = 1") |
30 proof (cases "n = 1") |
31 case True with one show ?thesis by simp |
31 case True |
|
32 with one show ?thesis by simp |
32 next |
33 next |
33 case False with \<open>n > 0\<close> have "n \<ge> 2" by auto |
34 case False |
34 moreover with * have "P (n div 2)" . |
35 with \<open>n > 0\<close> have "n \<ge> 2" by auto |
35 ultimately show ?thesis by (rule double) |
36 with * have "P (n div 2)" . |
|
37 with \<open>n \<ge> 2\<close> show ?thesis by (rule double) |
36 qed |
38 qed |
37 qed |
39 qed |
38 |
40 |
39 lemma log_zero [simp]: "log 0 = 0" |
41 lemma log_zero [simp]: "log 0 = 0" |
40 by (simp add: log.simps) |
42 by (simp add: log.simps) |