# HG changeset patch
# User huffman
# Date 1321595405 -3600
# Node ID 73a4f31d41c44fef13da198b0a2aaa960acad1fe
# Parent  3eb6319febfed77a4827f29dca043ccd073d7d70
Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs

diff -r 3eb6319febfe -r 73a4f31d41c4 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Nov 18 04:56:35 2011 +0100
+++ b/src/HOL/Word/Word.thy	Fri Nov 18 06:50:05 2011 +0100
@@ -1252,8 +1252,7 @@
   [THEN trans [OF uint_cong int_word_uint], standard]
 
 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
-  unfolding word_pred_def number_of_eq
-  by (simp add : pred_def word_no_wi)
+  unfolding word_pred_def uint_eq_0 pred_def by simp
 
 lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min"
   by (simp add: word_pred_0_n1 number_of_eq)
@@ -2164,11 +2163,11 @@
 lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
 
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
-  by (simp add: word_or_def word_no_wi [symmetric] number_of_is_id
+  by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
                 bin_trunc_ao(2) [symmetric])
 
 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
-  by (simp add: word_and_def number_of_is_id word_no_wi [symmetric]
+  by (simp add: word_and_def word_wi_log_defs word_ubin.eq_norm
                 bin_trunc_ao(1) [symmetric]) 
 
 lemma word_ops_nth_size:
@@ -2177,7 +2176,7 @@
     (x AND y) !! n = (x !! n & y !! n) & 
     (x XOR y) !! n = (x !! n ~= y !! n) & 
     (NOT x) !! n = (~ x !! n)"
-  unfolding word_size word_no_wi word_test_bit_def word_log_defs
+  unfolding word_size word_test_bit_def word_log_defs
   by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
 
 lemma word_ao_nth:
@@ -2336,26 +2335,26 @@
   xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard]
 
 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 
-  unfolding to_bl_def word_log_defs
-  by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric] bin_to_bl_def[symmetric])
+  unfolding to_bl_def word_log_defs bl_not_bin
+  by (simp add: word_ubin.eq_norm)
 
 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
   unfolding to_bl_def word_log_defs bl_xor_bin
-  by (simp add: number_of_is_id word_no_wi [symmetric])
+  by (simp add: word_ubin.eq_norm)
 
 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
-  unfolding to_bl_def word_log_defs
-  by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
+  unfolding to_bl_def word_log_defs bl_or_bin
+  by (simp add: word_ubin.eq_norm)
 
 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
-  unfolding to_bl_def word_log_defs
-  by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
+  unfolding to_bl_def word_log_defs bl_and_bin
+  by (simp add: word_ubin.eq_norm)
 
 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
   by (auto simp: word_test_bit_def word_lsb_def)
 
 lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
-  unfolding word_lsb_def word_1_no word_0_no by auto
+  unfolding word_lsb_def uint_eq_0 uint_1 by simp
 
 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
   apply (unfold word_lsb_def uint_bl bin_to_bl_def)