2279 "- numeral a OR 1 = word_of_int (- numeral a OR 1)" |
2279 "- numeral a OR 1 = word_of_int (- numeral a OR 1)" |
2280 "1 XOR numeral b = word_of_int (1 XOR numeral b)" |
2280 "1 XOR numeral b = word_of_int (1 XOR numeral b)" |
2281 "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" |
2281 "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" |
2282 "numeral a XOR 1 = word_of_int (numeral a XOR 1)" |
2282 "numeral a XOR 1 = word_of_int (numeral a XOR 1)" |
2283 "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" |
2283 "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" |
|
2284 by (transfer, simp)+ |
|
2285 |
|
2286 text {* Special cases for when one of the arguments equals -1. *} |
|
2287 |
|
2288 lemma word_bitwise_m1_simps [simp]: |
|
2289 "NOT (-1::'a::len0 word) = 0" |
|
2290 "(-1::'a::len0 word) AND x = x" |
|
2291 "x AND (-1::'a::len0 word) = x" |
|
2292 "(-1::'a::len0 word) OR x = -1" |
|
2293 "x OR (-1::'a::len0 word) = -1" |
|
2294 " (-1::'a::len0 word) XOR x = NOT x" |
|
2295 "x XOR (-1::'a::len0 word) = NOT x" |
2284 by (transfer, simp)+ |
2296 by (transfer, simp)+ |
2285 |
2297 |
2286 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)" |
2298 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)" |
2287 by (transfer, simp add: bin_trunc_ao) |
2299 by (transfer, simp add: bin_trunc_ao) |
2288 |
2300 |