added lemmas for -1
authornoschinl
Fri, 16 May 2014 16:40:02 +0200
changeset 56979 376604d56b54
parent 56978 0c1b4987e6b2
child 56980 9c5220e05e04
added lemmas for -1
src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri May 16 12:56:39 2014 +0200
+++ b/src/HOL/Word/Word.thy	Fri May 16 16:40:02 2014 +0200
@@ -2283,6 +2283,18 @@
   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
   by (transfer, simp)+
 
+text {* Special cases for when one of the arguments equals -1. *}
+
+lemma word_bitwise_m1_simps [simp]:
+  "NOT (-1::'a::len0 word) = 0"
+  "(-1::'a::len0 word) AND x = x"
+  "x AND (-1::'a::len0 word) = x"
+  "(-1::'a::len0 word) OR x = -1"
+  "x OR (-1::'a::len0 word) = -1"
+  " (-1::'a::len0 word) XOR x = NOT x"
+  "x XOR (-1::'a::len0 word) = NOT x"
+  by (transfer, simp)+
+
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (transfer, simp add: bin_trunc_ao)