1.1 --- a/src/HOL/Word/Word.thy Mon Dec 26 18:32:43 2011 +0100
1.2 +++ b/src/HOL/Word/Word.thy Tue Dec 27 11:38:55 2011 +0100
1.3 @@ -632,10 +632,10 @@
1.4 2 ^ (len_of TYPE('a) - 1)"
1.5 unfolding word_number_of_alt by (rule int_word_sint)
1.6
1.7 -lemma word_of_int_0: "word_of_int 0 = 0"
1.8 +lemma word_of_int_0 [simp]: "word_of_int 0 = 0"
1.9 unfolding word_0_wi ..
1.10
1.11 -lemma word_of_int_1: "word_of_int 1 = 1"
1.12 +lemma word_of_int_1 [simp]: "word_of_int 1 = 1"
1.13 unfolding word_1_wi ..
1.14
1.15 lemma word_of_int_bin [simp] :
1.16 @@ -1106,7 +1106,7 @@
1.17 by (simp only: Pls_def word_0_wi)
1.18
1.19 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
1.20 - by (simp add: word_number_of_alt word_0_wi)
1.21 + by (simp add: word_number_of_alt)
1.22
1.23 lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
1.24 unfolding Pls_def Bit_def by auto
1.25 @@ -1122,18 +1122,18 @@
1.26 by (simp add: word_m1_wi number_of_eq)
1.27
1.28 lemma word_0_bl [simp]: "of_bl [] = 0"
1.29 - unfolding word_0_wi of_bl_def by (simp add : Pls_def)
1.30 + unfolding of_bl_def by (simp add: Pls_def)
1.31
1.32 lemma word_1_bl: "of_bl [True] = 1"
1.33 - unfolding word_1_wi of_bl_def
1.34 - by (simp add : bl_to_bin_def Bit_def Pls_def)
1.35 + unfolding of_bl_def
1.36 + by (simp add: bl_to_bin_def Bit_def Pls_def)
1.37
1.38 lemma uint_eq_0 [simp] : "(uint 0 = 0)"
1.39 unfolding word_0_wi
1.40 by (simp add: word_ubin.eq_norm Pls_def [symmetric])
1.41
1.42 -lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
1.43 - by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
1.44 +lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
1.45 + by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
1.46
1.47 lemma to_bl_0 [simp]:
1.48 "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
1.49 @@ -1167,13 +1167,13 @@
1.50 by (auto simp: unat_0_iff [symmetric])
1.51
1.52 lemma ucast_0 [simp]: "ucast 0 = 0"
1.53 - unfolding ucast_def by (simp add: word_of_int_0)
1.54 + unfolding ucast_def by simp
1.55
1.56 lemma sint_0 [simp]: "sint 0 = 0"
1.57 unfolding sint_uint by simp
1.58
1.59 lemma scast_0 [simp]: "scast 0 = 0"
1.60 - unfolding scast_def by (simp add: word_of_int_0)
1.61 + unfolding scast_def by simp
1.62
1.63 lemma sint_n1 [simp] : "sint -1 = -1"
1.64 unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
1.65 @@ -1183,13 +1183,13 @@
1.66
1.67 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
1.68 unfolding word_1_wi
1.69 - by (simp add: word_ubin.eq_norm bintrunc_minus_simps)
1.70 + by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
1.71
1.72 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
1.73 unfolding unat_def by simp
1.74
1.75 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
1.76 - unfolding ucast_def by (simp add: word_of_int_1)
1.77 + unfolding ucast_def by simp
1.78
1.79 (* now, to get the weaker results analogous to word_div/mod_def *)
1.80
1.81 @@ -1212,7 +1212,8 @@
1.82 by (rule word_uint.Abs_cases [of b],
1.83 rule word_uint.Abs_cases [of a],
1.84 simp add: pred_def succ_def add_commute mult_commute
1.85 - ring_distribs new_word_of_int_homs)+
1.86 + ring_distribs new_word_of_int_homs
1.87 + del: word_of_int_0 word_of_int_1)+
1.88
1.89 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
1.90 by simp
1.91 @@ -1787,10 +1788,10 @@
1.92 by (simp add: word_of_nat word_of_int_succ_hom add_ac)
1.93
1.94 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
1.95 - by (simp add: word_of_nat word_0_wi)
1.96 + by simp
1.97
1.98 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
1.99 - by (simp add: word_of_nat word_1_wi)
1.100 + by simp
1.101
1.102 lemmas Abs_fnat_homs =
1.103 Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
1.104 @@ -1802,7 +1803,7 @@
1.105
1.106 lemma word_arith_nat_mult:
1.107 "a * b = of_nat (unat a * unat b)"
1.108 - by (simp add: Abs_fnat_hom_mult [symmetric])
1.109 + by (simp add: of_nat_mult)
1.110
1.111 lemma word_arith_nat_Suc:
1.112 "word_succ a = of_nat (Suc (unat a))"
1.113 @@ -2067,7 +2068,7 @@
1.114
1.115 lemma word_of_int_power_hom:
1.116 "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
1.117 - by (induct n) (simp_all add: word_of_int_hom_syms)
1.118 + by (induct n) (simp_all add: wi_hom_mult [symmetric])
1.119
1.120 lemma word_arith_power_alt:
1.121 "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
1.122 @@ -2596,15 +2597,11 @@
1.123 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
1.124 by (rule trans [OF _ shiftl1_number]) simp
1.125
1.126 -lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
1.127 - unfolding shiftr1_def
1.128 - by simp (simp add: word_0_wi)
1.129 -
1.130 -lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
1.131 - apply (unfold sshiftr1_def)
1.132 - apply simp
1.133 - apply (simp add : word_0_wi)
1.134 - done
1.135 +lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
1.136 + unfolding shiftr1_def by simp
1.137 +
1.138 +lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
1.139 + unfolding sshiftr1_def by simp
1.140
1.141 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
1.142 unfolding sshiftr1_def by auto
1.143 @@ -3102,7 +3099,8 @@
1.144
1.145 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
1.146 apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
1.147 - apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
1.148 + apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
1.149 + del: word_of_int_0)
1.150 apply (subst word_uint.norm_Rep [symmetric])
1.151 apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
1.152 apply auto
1.153 @@ -4279,7 +4277,7 @@
1.154
1.155 lemma shiftr1_1 [simp]:
1.156 "shiftr1 (1::'a::len word) = 0"
1.157 - by (simp add: shiftr1_def word_0_wi)
1.158 + unfolding shiftr1_def by simp
1.159
1.160 lemma shiftr_1[simp]:
1.161 "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"