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 bin_sign applied to numerals
authorhuffman
Tue, 13 Dec 2011 13:10:25 +0100
changeset 45850 50488b8abd58
parent 45849 904d8e0eaec6
child 45851 19f7ac6cf3cc
add simp rules for bin_sign applied to numerals
src/HOL/Word/Bit_Representation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:05:44 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:10:25 2011 +0100
@@ -301,12 +301,17 @@
   bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
 
 lemma bin_sign_simps [simp]:
+  "bin_sign 0 = 0"
+  "bin_sign -1 = -1"
+  "bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)"
+  "bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)"
   "bin_sign Int.Pls = Int.Pls"
   "bin_sign Int.Min = Int.Min"
   "bin_sign (Int.Bit0 w) = bin_sign w"
   "bin_sign (Int.Bit1 w) = bin_sign w"
   "bin_sign (w BIT b) = bin_sign w"
-  by (unfold bin_sign_def numeral_simps Bit_def bitval_def) (simp_all split: bit.split)
+  unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id
+  by (simp_all split: bit.split)
 
 lemma bin_sign_rest [simp]: 
   "bin_sign (bin_rest w) = bin_sign w"
isabelle