# HG changeset patch
# User huffman
# Date 1187798317 -7200
# Node ID 30887caeba62fc304fd7bf74b0adcc975d60c9cd
# Parent  317b207bc1ab8282f535fb50b9edad0f583a0f0c
move constant definitions to their respective subsections

diff -r 317b207bc1ab -r 30887caeba62 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Wed Aug 22 17:13:42 2007 +0200
+++ b/src/HOL/Word/WordShift.thy	Wed Aug 22 17:58:37 2007 +0200
@@ -6,7 +6,6 @@
 *)
 
 header {* Shifting, Rotating, and Splitting Words *}
-
 theory WordShift imports WordBitwise WordBoolList begin
 
 subsection "Bit shifting"
@@ -22,30 +21,13 @@
   sshiftr1 :: "'a :: len word => 'a word" 
   "sshiftr1 w == word_of_int (bin_rest (sint w))"
 
-  bshiftr1 :: "bool => 'a :: len word => 'a word"
-  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
-
   sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
   "w >>> n == (sshiftr1 ^ n) w"
 
-  mask :: "nat => 'a::len word"
-  "mask n == (1 << n) - 1"
-
-  revcast :: "'a :: len0 word => 'b :: len0 word"
-  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
-
-  slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
-  "slice1 n w == of_bl (takefill False n (to_bl w))"
-
-  slice :: "nat => 'a :: len0 word => 'b :: len0 word"
-  "slice n w == slice1 (size w - n) w"
-
 defs (overloaded)
   shiftl_def: "(w::'a::len0 word) << n == (shiftl1 ^ n) w"
   shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w"
 
-lemmas slice_def' = slice_def [unfolded word_size]
-
 lemma shiftl1_number [simp] :
   "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
   apply (unfold shiftl1_def word_number_of_def)
@@ -205,6 +187,10 @@
 
 subsubsection "shift functions in terms of lists of bools"
 
+definition
+  bshiftr1 :: "bool => 'a :: len word => 'a word" where
+  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
+
 lemmas bshiftr1_no_bin [simp] = 
   bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
 
@@ -493,6 +479,10 @@
 
 subsubsection "Mask"
 
+definition
+  mask :: "nat => 'a::len word" where
+  "mask n == (1 << n) - 1"
+
 lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
   apply (unfold mask_def test_bit_bl)
   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
@@ -629,6 +619,10 @@
 
 subsubsection "Revcast"
 
+definition
+  revcast :: "'a :: len0 word => 'b :: len0 word" where
+  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+
 lemmas revcast_def' = revcast_def [simplified]
 lemmas revcast_def'' = revcast_def' [simplified word_size]
 lemmas revcast_no_def [simp] =
@@ -752,6 +746,16 @@
 
 subsubsection "Slices"
 
+definition
+  slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
+  "slice1 n w == of_bl (takefill False n (to_bl w))"
+
+definition
+  slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
+  "slice n w == slice1 (size w - n) w"
+
+lemmas slice_def' = slice_def [unfolded word_size]
+
 lemmas slice1_no_bin [simp] =
   slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]