# HG changeset patch
# User huffman
# Date 1323800496 -3600
# Node ID 24f563d9449775e69423029a1f98def79a4bdaf6
# Parent  19f7ac6cf3cc63b3feb9d05311b7b0289a912490
add simp rules for bintrunc applied to numerals

diff -r 19f7ac6cf3cc -r 24f563d94497 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 13:21:48 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 19:21:36 2011 +0100
@@ -370,6 +370,16 @@
 
 subsection "Simplifications for (s)bintrunc"
 
+lemma bintrunc_n_0 [simp]: "bintrunc 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"
+  "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 bit_bool:
   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   by (cases b') auto
@@ -452,6 +462,7 @@
 
 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
   bintrunc_Bit0 bintrunc_Bit1
+  bintrunc_Suc_numeral
 
 lemmas sbintrunc_Suc_Pls = 
   sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps]
@@ -535,9 +546,9 @@
 lemmas bintrunc_BIT_minus_I = bmsts(3)
 
 lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
-  by auto
+  by (fact bintrunc.Z) (* FIXME: delete *)
 lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
-  by auto
+  by (fact bintrunc.Z) (* FIXME: delete *)
 
 lemma bintrunc_Suc_lem:
   "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"