equal
deleted
inserted
replaced
1104 |
1104 |
1105 lemma even_drop_bit_iff_not_bit: |
1105 lemma even_drop_bit_iff_not_bit: |
1106 \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close> |
1106 \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close> |
1107 by (simp add: bit_iff_odd_drop_bit) |
1107 by (simp add: bit_iff_odd_drop_bit) |
1108 |
1108 |
|
1109 lemma div_push_bit_of_1_eq_drop_bit: |
|
1110 \<open>a div push_bit n 1 = drop_bit n a\<close> |
|
1111 by (simp add: push_bit_eq_mult drop_bit_eq_div) |
|
1112 |
1109 lemma bits_ident: |
1113 lemma bits_ident: |
1110 "push_bit n (drop_bit n a) + take_bit n a = a" |
1114 "push_bit n (drop_bit n a) + take_bit n a = a" |
1111 using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) |
1115 using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) |
1112 |
1116 |
1113 lemma push_bit_push_bit [simp]: |
1117 lemma push_bit_push_bit [simp]: |