# HG changeset patch
# User huffman
# Date 1187655313 -7200
# Node ID 4aa80fadc071b3609ec9331bc59f7c7d44012925
# Parent  bb0d3b49fef08efba3eb7a86ffa7886108b48a4f
move scast/ucast stuff to its own subsection

diff -r bb0d3b49fef0 -r 4aa80fadc071 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Tue Aug 21 01:07:05 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Aug 21 02:15:13 2007 +0200
@@ -55,22 +55,6 @@
   norm_sint :: "nat => int => int"
   "norm_sint n w == (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
 
-  -- "cast a word to a different length"
-  scast :: "'a :: len word => 'b :: len word"
-  "scast w == word_of_int (sint w)"
-  ucast :: "'a :: len0 word => 'b :: len0 word"
-  "ucast w == word_of_int (uint w)"
-
-  -- "whether a cast (or other) function is to a longer or shorter length"
-  source_size :: "('a :: len0 word => 'b) => nat"
-  "source_size c == let arb = arbitrary ; x = c arb in size arb"  
-  target_size :: "('a => 'b :: len0 word) => nat"
-  "target_size c == size (c arbitrary)"
-  is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_up c == source_size c <= target_size c"
-  is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_down c == target_size c <= source_size c"
-
 constdefs
   of_bl :: "bool list => 'a :: len0 word" 
   "of_bl bl == word_of_int (bl_to_bin bl)"
@@ -628,7 +612,45 @@
   OF num_of_bintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
 lemmas num_abs_sbintr = sym [THEN trans,
   OF num_of_sbintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
-  
+
+lemma word_rev_tf': 
+  "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
+  unfolding of_bl_def uint_bl
+  by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
+
+lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
+
+lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
+  simplified, simplified rev_take, simplified]
+
+lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
+  by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
+
+lemmas test_bit_def' = word_test_bit_def [THEN meta_eq_to_obj_eq, THEN fun_cong]
+
+lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
+lemmas word_log_bin_defs = word_log_defs
+
+
+subsection {* Casting words to different lengths *}
+
+constdefs
+  -- "cast a word to a different length"
+  scast :: "'a :: len word => 'b :: len word"
+  "scast w == word_of_int (sint w)"
+  ucast :: "'a :: len0 word => 'b :: len0 word"
+  "ucast w == word_of_int (uint w)"
+
+  -- "whether a cast (or other) function is to a longer or shorter length"
+  source_size :: "('a :: len0 word => 'b) => nat"
+  "source_size c == let arb = arbitrary ; x = c arb in size arb"  
+  target_size :: "('a => 'b :: len0 word) => nat"
+  "target_size c == size (c arbitrary)"
+  is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
+  "is_up c == source_size c <= target_size c"
+  is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
+  "is_down c == target_size c <= source_size c"
+
 (** cast - note, no arg for new length, as it's determined by type of result,
   thus in "cast w = w, the type means cast to length of w! **)
 
@@ -680,16 +702,6 @@
   apply simp
   done
 
-lemma word_rev_tf': 
-  "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
-  unfolding of_bl_def uint_bl
-  by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
-
-lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
-
-lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
-  simplified, simplified rev_take, simplified]
-
 lemma to_bl_ucast: 
   "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) = 
    replicate (len_of TYPE('a) - len_of TYPE('b)) False @
@@ -802,8 +814,6 @@
    inj_on (ucast :: 'a word => 'b word) A"
   by (rule inj_on_inverseI, erule ucast_down_ucast_id)
 
-lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
-  by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
   
 lemma ucast_down_no': 
   "uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
@@ -820,9 +830,4 @@
     
 lemmas ucast_down_bl = ucast_down_bl' [OF refl]
 
-lemmas test_bit_def' = word_test_bit_def [THEN meta_eq_to_obj_eq, THEN fun_cong]
-
-lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-lemmas word_log_bin_defs = word_log_defs
-
 end