Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add simp rules for BIT applied to numerals
authorhuffman
Tue, 13 Dec 2011 13:05:44 +0100
changeset 45849 904d8e0eaec6
parent 45848 ec252975e82c
child 45850 50488b8abd58
add simp rules for BIT applied to numerals
src/HOL/Word/Bit_Representation.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle