# HG changeset patch
# User huffman
# Date 1325257715 -3600
# Node ID 88ef116e0522e58565434b5987535a778cbafc10
# Parent  8664713db1818a60301a051e0d9caaf2bf103262
add simp rules for bitwise word operations with 1

diff -r 8664713db181 -r 88ef116e0522 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Fri Dec 30 11:11:57 2011 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy	Fri Dec 30 16:08:35 2011 +0100
@@ -95,13 +95,14 @@
 lemma "0 AND 5 = (0 :: byte)" by simp
 lemma "1 AND 1 = (1 :: byte)" by simp
 lemma "1 AND 0 = (0 :: byte)" by simp
-lemma "1 AND 5 = (1 :: byte)" apply simp? oops
-lemma "1 OR 6 = (7 :: byte)" apply simp? oops
+lemma "1 AND 5 = (1 :: byte)" by simp
+lemma "1 OR 6 = (7 :: byte)" by simp
 lemma "1 OR 1 = (1 :: byte)" by simp
-lemma "1 XOR 7 = (6 :: byte)" apply simp? oops
+lemma "1 XOR 7 = (6 :: byte)" by simp
 lemma "1 XOR 1 = (0 :: byte)" by simp
-lemma "NOT 1 = (254 :: byte)" apply simp? oops
+lemma "NOT 1 = (254 :: byte)" by simp
 lemma "NOT 0 = (255 :: byte)" apply simp oops
+(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
 
 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
 
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])