1.1 --- a/src/HOL/Word/WordShift.thy	Wed Aug 22 17:13:42 2007 +0200
     1.2 +++ b/src/HOL/Word/WordShift.thy	Wed Aug 22 17:58:37 2007 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  *)
     1.5  
     1.6  header {* Shifting, Rotating, and Splitting Words *}
     1.7 -
     1.8  theory WordShift imports WordBitwise WordBoolList begin
     1.9  
    1.10  subsection "Bit shifting"
    1.11 @@ -22,30 +21,13 @@
    1.12    sshiftr1 :: "'a :: len word => 'a word" 
    1.13    "sshiftr1 w == word_of_int (bin_rest (sint w))"
    1.14  
    1.15 -  bshiftr1 :: "bool => 'a :: len word => 'a word"
    1.16 -  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
    1.17 -
    1.18    sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
    1.19    "w >>> n == (sshiftr1 ^ n) w"
    1.20  
    1.21 -  mask :: "nat => 'a::len word"
    1.22 -  "mask n == (1 << n) - 1"
    1.23 -
    1.24 -  revcast :: "'a :: len0 word => 'b :: len0 word"
    1.25 -  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
    1.26 -
    1.27 -  slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
    1.28 -  "slice1 n w == of_bl (takefill False n (to_bl w))"
    1.29 -
    1.30 -  slice :: "nat => 'a :: len0 word => 'b :: len0 word"
    1.31 -  "slice n w == slice1 (size w - n) w"
    1.32 -
    1.33  defs (overloaded)
    1.34    shiftl_def: "(w::'a::len0 word) << n == (shiftl1 ^ n) w"
    1.35    shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w"
    1.36  
    1.37 -lemmas slice_def' = slice_def [unfolded word_size]
    1.38 -
    1.39  lemma shiftl1_number [simp] :
    1.40    "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
    1.41    apply (unfold shiftl1_def word_number_of_def)
    1.42 @@ -205,6 +187,10 @@
    1.43  
    1.44  subsubsection "shift functions in terms of lists of bools"
    1.45  
    1.46 +definition
    1.47 +  bshiftr1 :: "bool => 'a :: len word => 'a word" where
    1.48 +  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
    1.49 +
    1.50  lemmas bshiftr1_no_bin [simp] = 
    1.51    bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
    1.52  
    1.53 @@ -493,6 +479,10 @@
    1.54  
    1.55  subsubsection "Mask"
    1.56  
    1.57 +definition
    1.58 +  mask :: "nat => 'a::len word" where
    1.59 +  "mask n == (1 << n) - 1"
    1.60 +
    1.61  lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
    1.62    apply (unfold mask_def test_bit_bl)
    1.63    apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
    1.64 @@ -629,6 +619,10 @@
    1.65  
    1.66  subsubsection "Revcast"
    1.67  
    1.68 +definition
    1.69 +  revcast :: "'a :: len0 word => 'b :: len0 word" where
    1.70 +  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
    1.71 +
    1.72  lemmas revcast_def' = revcast_def [simplified]
    1.73  lemmas revcast_def'' = revcast_def' [simplified word_size]
    1.74  lemmas revcast_no_def [simp] =
    1.75 @@ -752,6 +746,16 @@
    1.76  
    1.77  subsubsection "Slices"
    1.78  
    1.79 +definition
    1.80 +  slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
    1.81 +  "slice1 n w == of_bl (takefill False n (to_bl w))"
    1.82 +
    1.83 +definition
    1.84 +  slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
    1.85 +  "slice n w == slice1 (size w - n) w"
    1.86 +
    1.87 +lemmas slice_def' = slice_def [unfolded word_size]
    1.88 +
    1.89  lemmas slice1_no_bin [simp] =
    1.90    slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]
    1.91