1.1 --- a/NEWS Sat Mar 01 09:34:08 2014 +0100
1.2 +++ b/NEWS Sat Mar 01 17:08:39 2014 +0100
1.3 @@ -91,6 +91,13 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* HOL-Word:
1.8 + * Abandoned fact collection "word_arith_alts", which is a
1.9 + duplicate of "word_arith_wis".
1.10 + * Dropped first (duplicated) element in fact collections
1.11 + "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
1.12 + "uint_word_arith_bintrs".
1.13 +
1.14 * Code generator: explicit proof contexts in many ML interfaces.
1.15 INCOMPATIBILITY.
1.16
2.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Mar 01 09:34:08 2014 +0100
2.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Mar 01 17:08:39 2014 +0100
2.3 @@ -5,7 +5,7 @@
2.4 *)
2.5
2.6 theory RMD
2.7 -imports Word
2.8 +imports "~~/src/HOL/Word/Word"
2.9 begin
2.10
2.11
3.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sat Mar 01 09:34:08 2014 +0100
3.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sat Mar 01 17:08:39 2014 +0100
3.3 @@ -5,7 +5,7 @@
3.4 *)
3.5
3.6 theory RMD_Specification
3.7 -imports RMD SPARK
3.8 +imports RMD "~~/src/HOL/SPARK/SPARK"
3.9 begin
3.10
3.11 (* bit operations *)
4.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Mar 01 09:34:08 2014 +0100
4.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Mar 01 17:08:39 2014 +0100
4.3 @@ -456,7 +456,7 @@
4.4 unfolding round_def
4.5 unfolding steps_to_steps'
4.6 unfolding H1[symmetric]
4.7 - by (simp add: uint_word_ariths(2) rdmods
4.8 + by (simp add: uint_word_ariths(1) rdmods
4.9 uint_word_of_int_id)
4.10 qed
4.11
5.1 --- a/src/HOL/Word/Word.thy Sat Mar 01 09:34:08 2014 +0100
5.2 +++ b/src/HOL/Word/Word.thy Sat Mar 01 17:08:39 2014 +0100
5.3 @@ -1192,7 +1192,7 @@
5.4 subsection {* Word Arithmetic *}
5.5
5.6 lemma word_less_alt: "(a < b) = (uint a < uint b)"
5.7 - unfolding word_less_def word_le_def by (simp add: less_le)
5.8 + by (fact word_less_def)
5.9
5.10 lemma signed_linorder: "class.linorder word_sle word_sless"
5.11 by default (unfold word_sle_def word_sless_def, auto)
5.12 @@ -1236,16 +1236,20 @@
5.13 unfolding uint_bl
5.14 by (simp add: word_size bin_to_bl_zero)
5.15
5.16 -lemma uint_0_iff: "(uint x = 0) = (x = 0)"
5.17 - by (auto intro!: word_uint.Rep_eqD)
5.18 -
5.19 -lemma unat_0_iff: "(unat x = 0) = (x = 0)"
5.20 +lemma uint_0_iff:
5.21 + "uint x = 0 \<longleftrightarrow> x = 0"
5.22 + by (simp add: word_uint_eq_iff)
5.23 +
5.24 +lemma unat_0_iff:
5.25 + "unat x = 0 \<longleftrightarrow> x = 0"
5.26 unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
5.27
5.28 -lemma unat_0 [simp]: "unat 0 = 0"
5.29 +lemma unat_0 [simp]:
5.30 + "unat 0 = 0"
5.31 unfolding unat_def by auto
5.32
5.33 -lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
5.34 +lemma size_0_same':
5.35 + "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
5.36 apply (unfold word_size)
5.37 apply (rule box_equals)
5.38 defer
5.39 @@ -1278,8 +1282,7 @@
5.40 unfolding scast_def by simp
5.41
5.42 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
5.43 - unfolding word_1_wi
5.44 - by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
5.45 + by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
5.46
5.47 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
5.48 unfolding unat_def by simp
5.49 @@ -1289,10 +1292,6 @@
5.50
5.51 (* now, to get the weaker results analogous to word_div/mod_def *)
5.52
5.53 -lemmas word_arith_alts =
5.54 - word_sub_wi
5.55 - word_arith_wis (* FIXME: duplicate *)
5.56 -
5.57
5.58 subsection {* Transferring goals from words to ints *}
5.59
5.60 @@ -1308,16 +1307,44 @@
5.61 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
5.62 by simp
5.63
5.64 -lemmas uint_word_ariths =
5.65 - word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
5.66 -
5.67 -lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
5.68 -
5.69 -(* similar expressions for sint (arith operations) *)
5.70 -lemmas sint_word_ariths = uint_word_arith_bintrs
5.71 - [THEN uint_sint [symmetric, THEN trans],
5.72 - unfolded uint_sint bintr_arith1s bintr_ariths
5.73 - len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
5.74 +lemma uint_word_ariths:
5.75 + fixes a b :: "'a::len0 word"
5.76 + shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
5.77 + and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
5.78 + and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
5.79 + and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
5.80 + and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
5.81 + and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
5.82 + and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
5.83 + and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
5.84 + by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
5.85 +
5.86 +lemma uint_word_arith_bintrs:
5.87 + fixes a b :: "'a::len0 word"
5.88 + shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
5.89 + and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
5.90 + and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
5.91 + and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
5.92 + and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
5.93 + and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
5.94 + and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
5.95 + and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
5.96 + by (simp_all add: uint_word_ariths bintrunc_mod2p)
5.97 +
5.98 +lemma sint_word_ariths:
5.99 + fixes a b :: "'a::len word"
5.100 + shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
5.101 + and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
5.102 + and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
5.103 + and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
5.104 + and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
5.105 + and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
5.106 + and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
5.107 + and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
5.108 + by (simp_all add: uint_word_arith_bintrs
5.109 + [THEN uint_sint [symmetric, THEN trans],
5.110 + unfolded uint_sint bintr_arith1s bintr_ariths
5.111 + len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
5.112
5.113 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
5.114 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
5.115 @@ -1417,7 +1444,7 @@
5.116 with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
5.117 by auto
5.118 then show ?thesis
5.119 - by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
5.120 + by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
5.121 qed
5.122
5.123 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
5.124 @@ -3930,7 +3957,7 @@
5.125 apply (clarsimp simp: word_size)+
5.126 apply (rule trans)
5.127 apply (rule test_bit_rcat [OF refl refl])
5.128 - apply (simp add: word_size msrevs)
5.129 + apply (simp add: word_size)
5.130 apply (subst nth_rev)
5.131 apply arith
5.132 apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
5.133 @@ -4480,7 +4507,7 @@
5.134 uint x + uint y
5.135 else
5.136 uint x + uint y - 2^size x)"
5.137 - by (simp add: word_arith_alts int_word_uint mod_add_if_z
5.138 + by (simp add: word_arith_wis int_word_uint mod_add_if_z
5.139 word_size)
5.140
5.141 lemma unat_plus_if_size:
5.142 @@ -4501,16 +4528,7 @@
5.143
5.144 lemma max_lt:
5.145 "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
5.146 - apply (subst word_arith_nat_defs)
5.147 - apply (subst word_unat.eq_norm)
5.148 - apply (subst mod_if)
5.149 - apply clarsimp
5.150 - apply (erule notE)
5.151 - apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
5.152 - apply (erule order_le_less_trans)
5.153 - apply (insert unat_lt2p [of "max a b"])
5.154 - apply simp
5.155 - done
5.156 + by (fact unat_div)
5.157
5.158 lemma uint_sub_if_size:
5.159 "uint (x - y) =
5.160 @@ -4518,7 +4536,7 @@
5.161 uint x - uint y
5.162 else
5.163 uint x - uint y + 2^size x)"
5.164 - by (simp add: word_arith_alts int_word_uint mod_sub_if_z
5.165 + by (simp add: word_arith_wis int_word_uint mod_sub_if_z
5.166 word_size)
5.167
5.168 lemma unat_sub:
5.169 @@ -4725,5 +4743,3 @@
5.170
5.171 end
5.172
5.173 -
5.174 -