1.1 --- a/src/HOL/Word/Word.thy	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Mar 16 15:51:53 2012 +0100
     1.3 @@ -802,8 +802,10 @@
     1.4  lemma unats_uints: "unats n = nat ` uints n"
     1.5    by (auto simp add : uints_unats image_iff)
     1.6  
     1.7 -lemmas bintr_num = word_ubin.norm_eq_iff [symmetric, folded word_number_of_def]
     1.8 -lemmas sbintr_num = word_sbin.norm_eq_iff [symmetric, folded word_number_of_def]
     1.9 +lemmas bintr_num = word_ubin.norm_eq_iff
    1.10 +  [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
    1.11 +lemmas sbintr_num = word_sbin.norm_eq_iff
    1.12 +  [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
    1.13  
    1.14  lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def]
    1.15  lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def]
    1.16 @@ -812,22 +814,25 @@
    1.17    may want these in reverse, but loop as simp rules, so use following *)
    1.18  
    1.19  lemma num_of_bintr':
    1.20 -  "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow> 
    1.21 +  "bintrunc (len_of TYPE('a :: len0)) (number_of a) = (number_of b) \<Longrightarrow> 
    1.22      number_of a = (number_of b :: 'a word)"
    1.23 -  apply safe
    1.24 -  apply (rule_tac num_of_bintr [symmetric])
    1.25 -  done
    1.26 +  unfolding bintr_num by (erule subst, simp)
    1.27  
    1.28  lemma num_of_sbintr':
    1.29 -  "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow> 
    1.30 +  "sbintrunc (len_of TYPE('a :: len) - 1) (number_of a) = (number_of b) \<Longrightarrow> 
    1.31      number_of a = (number_of b :: 'a word)"
    1.32 -  apply safe
    1.33 -  apply (rule_tac num_of_sbintr [symmetric])
    1.34 -  done
    1.35 -
    1.36 -lemmas num_abs_bintr = sym [THEN trans, OF num_of_bintr word_number_of_def]
    1.37 -lemmas num_abs_sbintr = sym [THEN trans, OF num_of_sbintr word_number_of_def]
    1.38 -  
    1.39 +  unfolding sbintr_num by (erule subst, simp)
    1.40 +
    1.41 +lemma num_abs_bintr:
    1.42 +  "(number_of x :: 'a word) =
    1.43 +    word_of_int (bintrunc (len_of TYPE('a::len0)) (number_of x))"
    1.44 +  by (simp only: word_ubin.Abs_norm word_number_of_alt)
    1.45 +
    1.46 +lemma num_abs_sbintr:
    1.47 +  "(number_of x :: 'a word) =
    1.48 +    word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (number_of x))"
    1.49 +  by (simp only: word_sbin.Abs_norm word_number_of_alt)
    1.50 +
    1.51  (** cast - note, no arg for new length, as it's determined by type of result,
    1.52    thus in "cast w = w, the type means cast to length of w! **)
    1.53  
    1.54 @@ -2880,16 +2885,16 @@
    1.55    by (induct n) (auto simp: shiftl1_2t)
    1.56  
    1.57  lemma shiftr1_bintr [simp]:
    1.58 -  "(shiftr1 (number_of w) :: 'a :: len0 word) = 
    1.59 -    number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
    1.60 -  unfolding shiftr1_def word_number_of_def
    1.61 -  by (simp add : word_ubin.eq_norm)
    1.62 -
    1.63 -lemma sshiftr1_sbintr [simp] :
    1.64 -  "(sshiftr1 (number_of w) :: 'a :: len word) = 
    1.65 -    number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" 
    1.66 -  unfolding sshiftr1_def word_number_of_def
    1.67 -  by (simp add : word_sbin.eq_norm)
    1.68 +  "(shiftr1 (number_of w) :: 'a :: len0 word) =
    1.69 +    word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (number_of w)))"
    1.70 +  unfolding shiftr1_def word_number_of_alt
    1.71 +  by (simp add: word_ubin.eq_norm)
    1.72 +
    1.73 +lemma sshiftr1_sbintr [simp]:
    1.74 +  "(sshiftr1 (number_of w) :: 'a :: len word) =
    1.75 +    word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (number_of w)))"
    1.76 +  unfolding sshiftr1_def word_number_of_alt
    1.77 +  by (simp add: word_sbin.eq_norm)
    1.78  
    1.79  lemma shiftr_no [simp]:
    1.80    "(number_of w::'a::len0 word) >> n = word_of_int
    1.81 @@ -3379,11 +3384,9 @@
    1.82  
    1.83  lemma word_rsplit_no:
    1.84    "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
    1.85 -    map number_of (bin_rsplit (len_of TYPE('a :: len)) 
    1.86 -      (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
    1.87 -  apply (unfold word_rsplit_def word_no_wi)
    1.88 -  apply (simp add: word_ubin.eq_norm)
    1.89 -  done
    1.90 +    map word_of_int (bin_rsplit (len_of TYPE('a :: len)) 
    1.91 +      (len_of TYPE('b), bintrunc (len_of TYPE('b)) (number_of bin)))"
    1.92 +  unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
    1.93  
    1.94  lemmas word_rsplit_no_cl [simp] = word_rsplit_no
    1.95    [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]