1.1 --- a/src/HOL/Word/Word.thy Sat Mar 01 09:34:08 2014 +0100
1.2 +++ b/src/HOL/Word/Word.thy Sat Mar 01 17:08:39 2014 +0100
1.3 @@ -1192,7 +1192,7 @@
1.4 subsection {* Word Arithmetic *}
1.5
1.6 lemma word_less_alt: "(a < b) = (uint a < uint b)"
1.7 - unfolding word_less_def word_le_def by (simp add: less_le)
1.8 + by (fact word_less_def)
1.9
1.10 lemma signed_linorder: "class.linorder word_sle word_sless"
1.11 by default (unfold word_sle_def word_sless_def, auto)
1.12 @@ -1236,16 +1236,20 @@
1.13 unfolding uint_bl
1.14 by (simp add: word_size bin_to_bl_zero)
1.15
1.16 -lemma uint_0_iff: "(uint x = 0) = (x = 0)"
1.17 - by (auto intro!: word_uint.Rep_eqD)
1.18 -
1.19 -lemma unat_0_iff: "(unat x = 0) = (x = 0)"
1.20 +lemma uint_0_iff:
1.21 + "uint x = 0 \<longleftrightarrow> x = 0"
1.22 + by (simp add: word_uint_eq_iff)
1.23 +
1.24 +lemma unat_0_iff:
1.25 + "unat x = 0 \<longleftrightarrow> x = 0"
1.26 unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
1.27
1.28 -lemma unat_0 [simp]: "unat 0 = 0"
1.29 +lemma unat_0 [simp]:
1.30 + "unat 0 = 0"
1.31 unfolding unat_def by auto
1.32
1.33 -lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
1.34 +lemma size_0_same':
1.35 + "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
1.36 apply (unfold word_size)
1.37 apply (rule box_equals)
1.38 defer
1.39 @@ -1278,8 +1282,7 @@
1.40 unfolding scast_def by simp
1.41
1.42 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
1.43 - unfolding word_1_wi
1.44 - by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
1.45 + by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
1.46
1.47 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
1.48 unfolding unat_def by simp
1.49 @@ -1289,10 +1292,6 @@
1.50
1.51 (* now, to get the weaker results analogous to word_div/mod_def *)
1.52
1.53 -lemmas word_arith_alts =
1.54 - word_sub_wi
1.55 - word_arith_wis (* FIXME: duplicate *)
1.56 -
1.57
1.58 subsection {* Transferring goals from words to ints *}
1.59
1.60 @@ -1308,16 +1307,44 @@
1.61 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
1.62 by simp
1.63
1.64 -lemmas uint_word_ariths =
1.65 - word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
1.66 -
1.67 -lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
1.68 -
1.69 -(* similar expressions for sint (arith operations) *)
1.70 -lemmas sint_word_ariths = uint_word_arith_bintrs
1.71 - [THEN uint_sint [symmetric, THEN trans],
1.72 - unfolded uint_sint bintr_arith1s bintr_ariths
1.73 - len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
1.74 +lemma uint_word_ariths:
1.75 + fixes a b :: "'a::len0 word"
1.76 + shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
1.77 + and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
1.78 + and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
1.79 + and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
1.80 + and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
1.81 + and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
1.82 + and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
1.83 + and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
1.84 + by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
1.85 +
1.86 +lemma uint_word_arith_bintrs:
1.87 + fixes a b :: "'a::len0 word"
1.88 + shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
1.89 + and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
1.90 + and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
1.91 + and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
1.92 + and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
1.93 + and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
1.94 + and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
1.95 + and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
1.96 + by (simp_all add: uint_word_ariths bintrunc_mod2p)
1.97 +
1.98 +lemma sint_word_ariths:
1.99 + fixes a b :: "'a::len word"
1.100 + shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
1.101 + and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
1.102 + and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
1.103 + and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
1.104 + and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
1.105 + and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
1.106 + and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
1.107 + and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
1.108 + by (simp_all add: uint_word_arith_bintrs
1.109 + [THEN uint_sint [symmetric, THEN trans],
1.110 + unfolded uint_sint bintr_arith1s bintr_ariths
1.111 + len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
1.112
1.113 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
1.114 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
1.115 @@ -1417,7 +1444,7 @@
1.116 with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
1.117 by auto
1.118 then show ?thesis
1.119 - by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
1.120 + by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
1.121 qed
1.122
1.123 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
1.124 @@ -3930,7 +3957,7 @@
1.125 apply (clarsimp simp: word_size)+
1.126 apply (rule trans)
1.127 apply (rule test_bit_rcat [OF refl refl])
1.128 - apply (simp add: word_size msrevs)
1.129 + apply (simp add: word_size)
1.130 apply (subst nth_rev)
1.131 apply arith
1.132 apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
1.133 @@ -4480,7 +4507,7 @@
1.134 uint x + uint y
1.135 else
1.136 uint x + uint y - 2^size x)"
1.137 - by (simp add: word_arith_alts int_word_uint mod_add_if_z
1.138 + by (simp add: word_arith_wis int_word_uint mod_add_if_z
1.139 word_size)
1.140
1.141 lemma unat_plus_if_size:
1.142 @@ -4501,16 +4528,7 @@
1.143
1.144 lemma max_lt:
1.145 "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
1.146 - apply (subst word_arith_nat_defs)
1.147 - apply (subst word_unat.eq_norm)
1.148 - apply (subst mod_if)
1.149 - apply clarsimp
1.150 - apply (erule notE)
1.151 - apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
1.152 - apply (erule order_le_less_trans)
1.153 - apply (insert unat_lt2p [of "max a b"])
1.154 - apply simp
1.155 - done
1.156 + by (fact unat_div)
1.157
1.158 lemma uint_sub_if_size:
1.159 "uint (x - y) =
1.160 @@ -4518,7 +4536,7 @@
1.161 uint x - uint y
1.162 else
1.163 uint x - uint y + 2^size x)"
1.164 - by (simp add: word_arith_alts int_word_uint mod_sub_if_z
1.165 + by (simp add: word_arith_wis int_word_uint mod_sub_if_z
1.166 word_size)
1.167
1.168 lemma unat_sub:
1.169 @@ -4725,5 +4743,3 @@
1.170
1.171 end
1.172
1.173 -
1.174 -