src/HOL/Word/Word.thy

     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   apply (unfold of_bl_def)
   apply (clarsimp simp add : trunc_bl2bin [symmetric])
   done
 
-lemma of_bl_no: "of_bl bl = number_of (bl_to_bin bl)"
-  by (fact of_bl_def [folded word_number_of_def])
-
 lemma test_bit_of_bl:  
   "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
   apply (unfold of_bl_def word_test_bit_def)
   apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
   done
 
 lemma no_of_bl: 
   "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
-  unfolding word_size of_bl_no by (simp add : word_number_of_def)
+  unfolding word_size of_bl_def by (simp add: word_number_of_def)
 
 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   unfolding word_size to_bl_def by auto
 
 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"

   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 [OF refl]:
-  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
-  apply (unfold word_number_of_def is_down)
+lemma ucast_down_wi [OF refl]:
+  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x"
+  apply (unfold is_down)
   apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   apply (erule bintrunc_bintrunc_ge)
   done
 
+lemma ucast_down_no [OF refl]:
+  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
+  unfolding word_number_of_alt by clarify (rule ucast_down_wi)
+
 lemma ucast_down_bl [OF refl]:
   "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
-  unfolding of_bl_no by clarify (erule ucast_down_no)
+  unfolding of_bl_def by clarify (erule ucast_down_wi)
 
 lemmas slice_def' = slice_def [unfolded word_size]
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def

   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
   by (simp add : word_of_int_power_hom [symmetric])
 
 lemma of_bl_length_less: 
   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
-  apply (unfold of_bl_no [unfolded word_number_of_def]
-                word_less_alt word_number_of_alt)
+  apply (unfold of_bl_def word_less_alt word_number_of_alt)
   apply safe
   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
                        del: word_of_int_bin)
   apply (simp add: mod_pos_pos_trivial)
   apply (subst mod_pos_pos_trivial)
     apply (rule bl_to_bin_ge0)
    apply (rule order_less_trans)
     apply (rule bl_to_bin_lt2p)
    apply simp
-  apply (rule bl_to_bin_lt2p)    
+  apply (rule bl_to_bin_lt2p)
   done
 
 
 subsection "Cardinality, finiteness of set of words"