# HG changeset patch
# User huffman
# Date 1323786899 -3600
# Node ID b49cffac6c97c5fa4478a7fa7b4c768fe0ad6f89
# Parent  40554613b4f09cb5544b872a5333de642d7f4f03
add simp rules for sbintrunc applied to numerals

diff -r 40554613b4f0 -r b49cffac6c97 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 14:39:14 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 15:34:59 2011 +0100
@@ -376,6 +376,9 @@
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
   by (induct n) (auto simp add: Int.Pls_def)
 
+lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
+  by (induct n) (auto simp add: Int.Pls_def)
+
 lemma bintrunc_Suc_numeral:
   "bintrunc (Suc n) 1 = 1"
   "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
@@ -383,6 +386,13 @@
   "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
   by simp_all
 
+lemma sbintrunc_Suc_numeral:
+  "sbintrunc (Suc n) 1 = 1"
+  "sbintrunc (Suc n) -1 = sbintrunc n -1 BIT 1"
+  "sbintrunc (Suc n) (number_of (Int.Bit0 w)) = sbintrunc n (number_of w) BIT 0"
+  "sbintrunc (Suc n) (number_of (Int.Bit1 w)) = sbintrunc n (number_of w) BIT 1"
+  by simp_all
+
 lemma bit_bool:
   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   by (cases b') auto
@@ -486,6 +496,7 @@
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
+  sbintrunc_Suc_numeral
 
 lemmas sbintrunc_Pls = 
   sbintrunc.Z [where bin="Int.Pls",