equal
deleted
inserted
replaced
149 by (simp add: ac_simps) |
149 by (simp add: ac_simps) |
150 then have "2 dvd 1" |
150 then have "2 dvd 1" |
151 using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp |
151 using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp |
152 then show False by simp |
152 then show False by simp |
153 qed |
153 qed |
|
154 |
|
155 lemma odd_numeral_BitM [simp]: |
|
156 \<open>odd (numeral (Num.BitM w))\<close> |
|
157 by (cases w) simp_all |
154 |
158 |
155 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" |
159 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" |
156 by (induct n) auto |
160 by (induct n) auto |
157 |
161 |
158 lemma mask_eq_sum_exp: |
162 lemma mask_eq_sum_exp: |