src/HOL/Word/Bit_Representation.thy

   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 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"
   "bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0"
   "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
 
 lemma bit_bool: