# HG changeset patch
# User huffman
# Date 1323530662 -3600
# Node ID ff10ec0d62ea1d366f199b65582ab2e1dddf427a
# Parent  0f1c049c147e5dcb12ddb8932ea4cba4ece77881
generalize some lemmas

diff -r 0f1c049c147e -r ff10ec0d62ea src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Dec 10 13:00:58 2011 +0100
+++ b/src/HOL/Word/Word.thy	Sat Dec 10 16:24:22 2011 +0100
@@ -2818,6 +2818,12 @@
   apply (fast intro!: Suc_leI)
   done
 
+(* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
+lemma bl_shiftl1':
+  "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
+  unfolding shiftl1_bl
+  by (simp add: word_rep_drop drop_Suc del: drop_append)
+
 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
   apply (unfold shiftr1_def uint_bl of_bl_def)
   apply (simp add: butlast_rest_bin word_size)
@@ -2829,20 +2835,25 @@
   unfolding shiftr1_bl
   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
 
-
-(* relate the two above : TODO - remove the :: len restriction on
-  this theorem and others depending on it *)
+(* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
+lemma bl_shiftr1':
+  "to_bl (shiftr1 w) = butlast (False # to_bl w)"
+  apply (rule word_bl.Abs_inverse')
+  apply (simp del: butlast.simps)
+  apply (simp add: shiftr1_bl of_bl_def)
+  done
+
 lemma shiftl1_rev: 
-  "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
+  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
   apply (unfold word_reverse_def)
   apply (rule word_bl.Rep_inverse' [symmetric])
-  apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
+  apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
   apply (cases "to_bl w")
    apply auto
   done
 
 lemma shiftl_rev: 
-  "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
+  "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
   apply (unfold shiftl_def shiftr_def)
   apply (induct "n")
    apply (auto simp add : shiftl1_rev)
@@ -2893,14 +2904,12 @@
   apply (auto simp: word_size)
   done
 
-lemma take_shiftr [rule_format] :
-  "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = 
-    replicate n False" 
+lemma take_shiftr:
+  "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
   apply (unfold shiftr_def)
   apply (induct n)
    prefer 2
-   apply (simp add: bl_shiftr1)
-   apply (rule impI)
+   apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
    apply (rule take_butlast [THEN trans])
   apply (auto simp: word_size)
   done