# HG changeset patch
# User huffman
# Date 1323778908 -3600
# Node ID 19f7ac6cf3cc63b3feb9d05311b7b0289a912490
# Parent  50488b8abd5868d4850ea3385c55095f8bf6f129
add simp rules for bin_rest and bin_last applied to numerals

diff -r 50488b8abd58 -r 19f7ac6cf3cc src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:10:25 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:21:48 2011 +0100
@@ -55,6 +55,22 @@
   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 bin_last_numeral_simps [simp]:
+  "bin_last 0 = 0"
+  "bin_last 1 = 1"
+  "bin_last -1 = 1"
+  "bin_last (number_of (Int.Bit0 w)) = 0"
+  "bin_last (number_of (Int.Bit1 w)) = 1"
+  unfolding bin_last_def by simp_all
+
+lemma bin_rest_numeral_simps [simp]:
+  "bin_rest 0 = 0"
+  "bin_rest 1 = 0"
+  "bin_rest -1 = -1"
+  "bin_rest (number_of (Int.Bit0 w)) = number_of w"
+  "bin_rest (number_of (Int.Bit1 w)) = number_of w"
+  unfolding bin_rest_def by simp_all
+
 lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
   unfolding Bit_def Bit0_def by simp
 
@@ -207,17 +223,6 @@
   "bin_last (w BIT b) = b"
   using bin_rl_simps bin_rl_def by auto
 
-lemma bin_r_l_extras [simp]:
-  "bin_last 0 = (0::bit)"
-  "bin_last (- 1) = (1::bit)"
-  "bin_last -1 = (1::bit)"
-  "bin_last 1 = (1::bit)"
-  "bin_rest 1 = 0"
-  "bin_rest 0 = 0"
-  "bin_rest (- 1) = - 1"
-  "bin_rest -1 = -1"
-  by (simp_all add: bin_last_def bin_rest_def)
-
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   unfolding bin_rest_def [symmetric] by auto