changeset 70183 | 3ea80c950023 |
parent 67120 | 491fd7f0b5df |
child 70191 | bdc835d934b7 |
70182:ca9dfa7ee3bd | 70183:3ea80c950023 |
---|---|
80 |
80 |
81 lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1" |
81 lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1" |
82 for a b :: bit |
82 for a b :: bit |
83 by (induct a) simp_all |
83 by (induct a) simp_all |
84 |
84 |
85 lemma bit_nand_same [simp]: "x AND NOT x = 0" |
|
86 for x :: bit |
|
87 by (cases x) simp_all |
|
88 |
|
85 end |
89 end |