# HG changeset patch
# User huffman
# Date 1330086783 -3600
# Node ID 0abbf6dd09eeee5b83245566fc69ea03c5a03fc7
# Parent  573aff6b9b0a54ff3a4f997f450ea11a2a5e7957
remove ill-formed lemma of_bl_no; adapt proofs

diff -r 573aff6b9b0a -r 0abbf6dd09ee src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Feb 24 13:25:21 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 13:33:03 2012 +0100
@@ -755,9 +755,6 @@
   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)
@@ -766,7 +763,7 @@
 
 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
@@ -1005,17 +1002,21 @@
 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]
@@ -2031,8 +2032,7 @@
 
 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)
@@ -2042,7 +2042,7 @@
    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