equal
deleted
inserted
replaced
224 then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close> |
224 then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close> |
225 by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff) |
225 by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff) |
226 (cases m, simp_all add: bit_Suc) |
226 (cases m, simp_all add: bit_Suc) |
227 qed |
227 qed |
228 |
228 |
229 lemma set_bit_Suc [simp]: |
229 lemma set_bit_Suc: |
230 \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close> |
230 \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close> |
231 proof (rule bit_eqI) |
231 proof (rule bit_eqI) |
232 fix m |
232 fix m |
233 assume *: \<open>2 ^ m \<noteq> 0\<close> |
233 assume *: \<open>2 ^ m \<noteq> 0\<close> |
234 show \<open>bit (set_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * set_bit n (a div 2)) m\<close> |
234 show \<open>bit (set_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * set_bit n (a div 2)) m\<close> |
255 then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close> |
255 then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close> |
256 by (simp add: bit_unset_bit_iff bit_double_iff) |
256 by (simp add: bit_unset_bit_iff bit_double_iff) |
257 (cases m, simp_all add: bit_Suc) |
257 (cases m, simp_all add: bit_Suc) |
258 qed |
258 qed |
259 |
259 |
260 lemma unset_bit_Suc [simp]: |
260 lemma unset_bit_Suc: |
261 \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close> |
261 \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close> |
262 proof (rule bit_eqI) |
262 proof (rule bit_eqI) |
263 fix m |
263 fix m |
264 assume *: \<open>2 ^ m \<noteq> 0\<close> |
264 assume *: \<open>2 ^ m \<noteq> 0\<close> |
265 then show \<open>bit (unset_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * unset_bit n (a div 2)) m\<close> |
265 then show \<open>bit (unset_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * unset_bit n (a div 2)) m\<close> |
284 then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close> |
284 then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close> |
285 by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff) |
285 by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff) |
286 (cases m, simp_all add: bit_Suc) |
286 (cases m, simp_all add: bit_Suc) |
287 qed |
287 qed |
288 |
288 |
289 lemma flip_bit_Suc [simp]: |
289 lemma flip_bit_Suc: |
290 \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close> |
290 \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close> |
291 proof (rule bit_eqI) |
291 proof (rule bit_eqI) |
292 fix m |
292 fix m |
293 assume *: \<open>2 ^ m \<noteq> 0\<close> |
293 assume *: \<open>2 ^ m \<noteq> 0\<close> |
294 show \<open>bit (flip_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * flip_bit n (a div 2)) m\<close> |
294 show \<open>bit (flip_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * flip_bit n (a div 2)) m\<close> |