# HG changeset patch
# User huffman
# Date 1323797584 -3600
# Node ID caa99836aed8df51531edd8ed9379d0106612bcd
# Parent  b49cffac6c97c5fa4478a7fa7b4c768fe0ad6f89
more simp rules for sbintrunc

diff -r b49cffac6c97 -r caa99836aed8 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 15:34:59 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 18:33:04 2011 +0100
@@ -379,6 +379,9 @@
 lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
   by (induct n) (auto simp add: Int.Pls_def)
 
+lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
+  by (induct n) (auto, simp add: number_of_is_id)
+
 lemma bintrunc_Suc_numeral:
   "bintrunc (Suc n) 1 = 1"
   "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
@@ -386,9 +389,14 @@
   "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
   by simp_all
 
+lemma sbintrunc_0_numeral [simp]:
+  "sbintrunc 0 1 = -1"
+  "sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
+  "sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
+  by (simp_all, unfold Pls_def number_of_is_id, 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