diff -r 8664713db181 -r 88ef116e0522 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Dec 30 11:11:57 2011 +0100
+++ b/src/HOL/Word/Word.thy	Fri Dec 30 16:08:35 2011 +0100
@@ -2106,6 +2106,18 @@
   "number_of a XOR number_of b = (number_of (a XOR b) :: 'a word)"
   unfolding word_no_wi word_wi_log_defs by simp_all
 
+text {* Special cases for when one of the arguments equals 1. *}
+
+lemma word_bitwise_1_simps [simp]:
+  "NOT (1::'a::len0 word) = -2"
+  "(1::'a word) AND number_of b = number_of (Int.Bit1 Int.Pls AND b)"
+  "number_of a AND (1::'a word) = number_of (a AND Int.Bit1 Int.Pls)"
+  "(1::'a word) OR number_of b = number_of (Int.Bit1 Int.Pls OR b)"
+  "number_of a OR (1::'a word) = number_of (a OR Int.Bit1 Int.Pls)"
+  "(1::'a word) XOR number_of b = number_of (Int.Bit1 Int.Pls XOR b)"
+  "number_of a XOR (1::'a word) = number_of (a XOR Int.Bit1 Int.Pls)"
+  unfolding word_1_no word_no_log_defs by simp_all
+
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
                 bin_trunc_ao(2) [symmetric])