--- 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