# HG changeset patch
# User noschinl
# Date 1400251202 -7200
# Node ID 376604d56b54ecd8fd7cb1dda648a54a68a39a49
# Parent  0c1b4987e6b288a32107e6d90ab8f792cae646f4
added lemmas for -1

diff -r 0c1b4987e6b2 -r 376604d56b54 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)