# HG changeset patch
# User huffman
# Date 1323778225 -3600
# Node ID 50488b8abd5868d4850ea3385c55095f8bf6f129
# Parent  904d8e0eaec67fda98e3d65cbe3fc13664e78bdb
add simp rules for bin_sign applied to numerals

diff -r 904d8e0eaec6 -r 50488b8abd58 src/HOL/Word/Bit_Representation.thy
--- 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"