93 lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp |
93 lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp |
94 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp |
94 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp |
95 lemma "0 AND 5 = (0 :: byte)" by simp |
95 lemma "0 AND 5 = (0 :: byte)" by simp |
96 lemma "1 AND 1 = (1 :: byte)" by simp |
96 lemma "1 AND 1 = (1 :: byte)" by simp |
97 lemma "1 AND 0 = (0 :: byte)" by simp |
97 lemma "1 AND 0 = (0 :: byte)" by simp |
98 lemma "1 AND 5 = (1 :: byte)" apply simp? oops |
98 lemma "1 AND 5 = (1 :: byte)" by simp |
99 lemma "1 OR 6 = (7 :: byte)" apply simp? oops |
99 lemma "1 OR 6 = (7 :: byte)" by simp |
100 lemma "1 OR 1 = (1 :: byte)" by simp |
100 lemma "1 OR 1 = (1 :: byte)" by simp |
101 lemma "1 XOR 7 = (6 :: byte)" apply simp? oops |
101 lemma "1 XOR 7 = (6 :: byte)" by simp |
102 lemma "1 XOR 1 = (0 :: byte)" by simp |
102 lemma "1 XOR 1 = (0 :: byte)" by simp |
103 lemma "NOT 1 = (254 :: byte)" apply simp? oops |
103 lemma "NOT 1 = (254 :: byte)" by simp |
104 lemma "NOT 0 = (255 :: byte)" apply simp oops |
104 lemma "NOT 0 = (255 :: byte)" apply simp oops |
|
105 (* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *) |
105 |
106 |
106 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp |
107 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp |
107 |
108 |
108 lemma "(0b0010 :: 4 word) !! 1" by simp |
109 lemma "(0b0010 :: 4 word) !! 1" by simp |
109 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp |
110 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp |