equal
deleted
inserted
replaced
55 |
55 |
56 lemma and_zero_eq [simp]: |
56 lemma and_zero_eq [simp]: |
57 "a AND 0 = 0" |
57 "a AND 0 = 0" |
58 by (simp add: bit_eq_iff bit_and_iff) |
58 by (simp add: bit_eq_iff bit_and_iff) |
59 |
59 |
60 lemma one_and_eq [simp]: |
60 lemma one_and_eq: |
61 "1 AND a = a mod 2" |
61 "1 AND a = a mod 2" |
62 by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) |
62 by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) |
63 |
63 |
64 lemma and_one_eq [simp]: |
64 lemma and_one_eq: |
65 "a AND 1 = a mod 2" |
65 "a AND 1 = a mod 2" |
66 using one_and_eq [of a] by (simp add: ac_simps) |
66 using one_and_eq [of a] by (simp add: ac_simps) |
67 |
67 |
68 lemma one_or_eq: |
68 lemma one_or_eq: |
69 "1 OR a = a + of_bool (even a)" |
69 "1 OR a = a + of_bool (even a)" |