src/HOL/Word/Word.thy

 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + 
     2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
     2 ^ (len_of TYPE('a) - 1)"
   unfolding word_number_of_alt by (rule int_word_sint)
 
-lemma word_of_int_0: "word_of_int 0 = 0"
+lemma word_of_int_0 [simp]: "word_of_int 0 = 0"
   unfolding word_0_wi ..
 
-lemma word_of_int_1: "word_of_int 1 = 1"
+lemma word_of_int_1 [simp]: "word_of_int 1 = 1"
   unfolding word_1_wi ..
 
 lemma word_of_int_bin [simp] : 
   "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
   unfolding word_number_of_alt by auto

   *)
 lemma word_0_wi_Pls: "0 = word_of_int Int.Pls"
   by (simp only: Pls_def word_0_wi)
 
 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
-  by (simp add: word_number_of_alt word_0_wi)
+  by (simp add: word_number_of_alt)
 
 lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
   unfolding Pls_def Bit_def by auto
 
 lemma word_1_no: 

 
 lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
   by (simp add: word_m1_wi number_of_eq)
 
 lemma word_0_bl [simp]: "of_bl [] = 0" 
-  unfolding word_0_wi of_bl_def by (simp add : Pls_def)
+  unfolding of_bl_def by (simp add: Pls_def)
 
 lemma word_1_bl: "of_bl [True] = 1" 
-  unfolding word_1_wi of_bl_def
-  by (simp add : bl_to_bin_def Bit_def Pls_def)
+  unfolding of_bl_def
+  by (simp add: bl_to_bin_def Bit_def Pls_def)
 
 lemma uint_eq_0 [simp] : "(uint 0 = 0)" 
   unfolding word_0_wi
   by (simp add: word_ubin.eq_norm Pls_def [symmetric])
 
-lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
-  by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
+lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
+  by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
 
 lemma to_bl_0 [simp]:
   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
   unfolding uint_bl
   by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])

 
 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
 by (auto simp: unat_0_iff [symmetric])
 
 lemma ucast_0 [simp]: "ucast 0 = 0"
-  unfolding ucast_def by (simp add: word_of_int_0)
+  unfolding ucast_def by simp
 
 lemma sint_0 [simp]: "sint 0 = 0"
   unfolding sint_uint by simp
 
 lemma scast_0 [simp]: "scast 0 = 0"
-  unfolding scast_def by (simp add: word_of_int_0)
+  unfolding scast_def by simp
 
 lemma sint_n1 [simp] : "sint -1 = -1"
   unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
 
 lemma scast_n1 [simp]: "scast -1 = -1"
   unfolding scast_def by simp
 
 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
   unfolding word_1_wi
-  by (simp add: word_ubin.eq_norm bintrunc_minus_simps)
+  by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
 
 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
   unfolding unat_def by simp
 
 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
-  unfolding ucast_def by (simp add: word_of_int_1)
+  unfolding ucast_def by simp
 
 (* now, to get the weaker results analogous to word_div/mod_def *)
 
 lemmas word_arith_alts = 
   word_sub_wi [unfolded succ_def pred_def]

   word_succ_pred: "word_succ (word_pred a) = a" and
   word_mult_succ: "word_succ a * b = b + a * b"
   by (rule word_uint.Abs_cases [of b],
       rule word_uint.Abs_cases [of a],
       simp add: pred_def succ_def add_commute mult_commute 
-                ring_distribs new_word_of_int_homs)+
+                ring_distribs new_word_of_int_homs
+           del: word_of_int_0 word_of_int_1)+
 
 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
   by simp
 
 lemmas uint_word_ariths = 

 lemma Abs_fnat_hom_Suc:
   "word_succ (of_nat a) = of_nat (Suc a)"
   by (simp add: word_of_nat word_of_int_succ_hom add_ac)
 
 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
-  by (simp add: word_of_nat word_0_wi)
+  by simp
 
 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
-  by (simp add: word_of_nat word_1_wi)
+  by simp
 
 lemmas Abs_fnat_homs = 
   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 
   Abs_fnat_hom_0 Abs_fnat_hom_1
 

   "a + b = of_nat (unat a + unat b)" 
   by simp
 
 lemma word_arith_nat_mult:
   "a * b = of_nat (unat a * unat b)"
-  by (simp add: Abs_fnat_hom_mult [symmetric])
+  by (simp add: of_nat_mult)
     
 lemma word_arith_nat_Suc:
   "word_succ a = of_nat (Suc (unat a))"
   by (subst Abs_fnat_hom_Suc [symmetric]) simp
 

   apply (clarsimp simp add : uno_simps)
   done
 
 lemma word_of_int_power_hom: 
   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
-  by (induct n) (simp_all add: word_of_int_hom_syms)
+  by (induct n) (simp_all add: wi_hom_mult [symmetric])
 
 lemma word_arith_power_alt: 
   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
   by (simp add : word_of_int_power_hom [symmetric])
 

   by (simp only: word_number_of_def shiftl1_def)
 
 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
   by (rule trans [OF _ shiftl1_number]) simp
 
-lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
-  unfolding shiftr1_def 
-  by simp (simp add: word_0_wi)
-
-lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
-  apply (unfold sshiftr1_def)
-  apply simp
-  apply (simp add : word_0_wi)
-  done
+lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
+  unfolding shiftr1_def by simp
+
+lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
+  unfolding sshiftr1_def by simp
 
 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
   unfolding sshiftr1_def by auto
 
 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"

   apply (fast intro!: lt2p_lem)
   done
 
 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
-  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
+  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
+    del: word_of_int_0)
   apply (subst word_uint.norm_Rep [symmetric])
   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
   apply auto
   done
 

   "uint x < 0 = False"
   by (simp add: linorder_not_less)
 
 lemma shiftr1_1 [simp]: 
   "shiftr1 (1::'a::len word) = 0"
-  by (simp add: shiftr1_def word_0_wi)
+  unfolding shiftr1_def by simp
 
 lemma shiftr_1[simp]: 
   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   by (induct n) (auto simp: shiftr_def)