# HG changeset patch
# User huffman
# Date 1323777944 -3600
# Node ID 904d8e0eaec67fda98e3d65cbe3fc13664e78bdb
# Parent  ec252975e82c1277f4af7352aa85f82c7cfb21d0
add simp rules for BIT applied to numerals

diff -r ec252975e82c -r 904d8e0eaec6 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 12:55:36 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:05:44 2011 +0100
@@ -46,6 +46,15 @@
 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
   by (metis bin_rest_BIT bin_last_BIT)
 
+lemma BIT_bin_simps [simp]:
+  "number_of w BIT 0 = number_of (Int.Bit0 w)"
+  "number_of w BIT 1 = number_of (Int.Bit1 w)"
+  unfolding Bit_def number_of_is_id numeral_simps by simp_all
+
+lemma BIT_special_simps [simp]:
+  shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+  unfolding Bit_def by simp_all
+
 lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
   unfolding Bit_def Bit0_def by simp