72000
|
1 |
(* Author: Jeremy Dawson, NICTA
|
|
2 |
*)
|
|
3 |
|
|
4 |
section \<open>Operation variants with traditional syntax\<close>
|
|
5 |
|
|
6 |
theory Traditional_Syntax
|
72508
|
7 |
imports Word
|
|
8 |
begin
|
|
9 |
|
|
10 |
class semiring_bit_syntax = semiring_bit_shifts
|
|
11 |
begin
|
|
12 |
|
|
13 |
definition test_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close> (infixl "!!" 100)
|
|
14 |
where test_bit_eq_bit: \<open>test_bit = bit\<close>
|
|
15 |
|
|
16 |
definition shiftl :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close> (infixl "<<" 55)
|
|
17 |
where shiftl_eq_push_bit: \<open>a << n = push_bit n a\<close>
|
|
18 |
|
|
19 |
definition shiftr :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close> (infixl ">>" 55)
|
|
20 |
where shiftr_eq_drop_bit: \<open>a >> n = drop_bit n a\<close>
|
|
21 |
|
|
22 |
end
|
|
23 |
|
|
24 |
instance word :: (len) semiring_bit_syntax ..
|
|
25 |
|
|
26 |
context
|
|
27 |
includes lifting_syntax
|
72000
|
28 |
begin
|
|
29 |
|
72508
|
30 |
lemma test_bit_word_transfer [transfer_rule]:
|
|
31 |
\<open>(pcr_word ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) (test_bit :: 'a::len word \<Rightarrow> _)\<close>
|
|
32 |
by (unfold test_bit_eq_bit) transfer_prover
|
|
33 |
|
|
34 |
lemma shiftl_word_transfer [transfer_rule]:
|
|
35 |
\<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) shiftl\<close>
|
|
36 |
by (unfold shiftl_eq_push_bit) transfer_prover
|
|
37 |
|
|
38 |
lemma shiftr_word_transfer [transfer_rule]:
|
|
39 |
\<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (shiftr :: 'a::len word \<Rightarrow> _)\<close>
|
|
40 |
by (unfold shiftr_eq_drop_bit) transfer_prover
|
72000
|
41 |
|
|
42 |
end
|
72508
|
43 |
|
|
44 |
lemma test_bit_word_eq:
|
|
45 |
\<open>test_bit = (bit :: 'a::len word \<Rightarrow> _)\<close>
|
|
46 |
by (fact test_bit_eq_bit)
|
|
47 |
|
|
48 |
lemma shiftl_word_eq:
|
|
49 |
\<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close>
|
|
50 |
by (fact shiftl_eq_push_bit)
|
|
51 |
|
|
52 |
lemma shiftr_word_eq:
|
|
53 |
\<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
|
|
54 |
by (fact shiftr_eq_drop_bit)
|
|
55 |
|
|
56 |
lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v"
|
|
57 |
for u v :: "'a::len word"
|
|
58 |
by (simp add: bit_eq_iff test_bit_eq_bit fun_eq_iff)
|
|
59 |
|
|
60 |
lemma test_bit_size: "w !! n \<Longrightarrow> n < size w"
|
|
61 |
for w :: "'a::len word"
|
|
62 |
by transfer simp
|
|
63 |
|
|
64 |
lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
|
|
65 |
for x y :: "'a::len word"
|
|
66 |
by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)
|
|
67 |
|
|
68 |
lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
|
|
69 |
for u :: "'a::len word"
|
|
70 |
by (simp add: word_size word_eq_iff)
|
|
71 |
|
|
72 |
lemma word_eqD: "u = v \<Longrightarrow> u !! x = v !! x"
|
|
73 |
for u v :: "'a::len word"
|
|
74 |
by simp
|
|
75 |
|
|
76 |
lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bit (uint w) n"
|
|
77 |
by transfer (simp add: bit_take_bit_iff)
|
|
78 |
|
|
79 |
lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
|
|
80 |
|
|
81 |
lemma word_test_bit_def:
|
|
82 |
\<open>test_bit a = bit (uint a)\<close>
|
|
83 |
by transfer (simp add: fun_eq_iff bit_take_bit_iff)
|
|
84 |
|
|
85 |
lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
|
|
86 |
|
|
87 |
lemma word_test_bit_transfer [transfer_rule]:
|
|
88 |
"(rel_fun pcr_word (rel_fun (=) (=)))
|
|
89 |
(\<lambda>x n. n < LENGTH('a) \<and> bit x n) (test_bit :: 'a::len word \<Rightarrow> _)"
|
|
90 |
by (simp only: test_bit_eq_bit) transfer_prover
|
|
91 |
|
|
92 |
lemma test_bit_wi [simp]:
|
|
93 |
"(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bit x n"
|
|
94 |
by transfer simp
|
|
95 |
|
|
96 |
lemma word_ops_nth_size:
|
|
97 |
"n < size x \<Longrightarrow>
|
|
98 |
(x OR y) !! n = (x !! n | y !! n) \<and>
|
|
99 |
(x AND y) !! n = (x !! n \<and> y !! n) \<and>
|
|
100 |
(x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
|
|
101 |
(NOT x) !! n = (\<not> x !! n)"
|
|
102 |
for x :: "'a::len word"
|
|
103 |
by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff)
|
|
104 |
|
|
105 |
lemma word_ao_nth:
|
|
106 |
"(x OR y) !! n = (x !! n | y !! n) \<and>
|
|
107 |
(x AND y) !! n = (x !! n \<and> y !! n)"
|
|
108 |
for x :: "'a::len word"
|
|
109 |
by transfer (auto simp add: bit_or_iff bit_and_iff)
|
|
110 |
|
|
111 |
lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
|
|
112 |
lemmas msb1 = msb0 [where i = 0]
|
|
113 |
|
|
114 |
lemma test_bit_numeral [simp]:
|
|
115 |
"(numeral w :: 'a::len word) !! n \<longleftrightarrow>
|
|
116 |
n < LENGTH('a) \<and> bit (numeral w :: int) n"
|
|
117 |
by transfer (rule refl)
|
|
118 |
|
|
119 |
lemma test_bit_neg_numeral [simp]:
|
|
120 |
"(- numeral w :: 'a::len word) !! n \<longleftrightarrow>
|
|
121 |
n < LENGTH('a) \<and> bit (- numeral w :: int) n"
|
|
122 |
by transfer (rule refl)
|
|
123 |
|
|
124 |
lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
|
|
125 |
by transfer (auto simp add: bit_1_iff)
|
|
126 |
|
|
127 |
lemma nth_0 [simp]: "\<not> (0 :: 'a::len word) !! n"
|
|
128 |
by transfer simp
|
|
129 |
|
|
130 |
lemma nth_minus1 [simp]: "(-1 :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
|
|
131 |
by transfer simp
|
|
132 |
|
|
133 |
lemma shiftl1_code [code]:
|
|
134 |
\<open>shiftl1 w = push_bit 1 w\<close>
|
|
135 |
by transfer (simp add: ac_simps)
|
|
136 |
|
|
137 |
lemma uint_shiftr_eq:
|
|
138 |
\<open>uint (w >> n) = uint w div 2 ^ n\<close>
|
|
139 |
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv)
|
|
140 |
|
|
141 |
lemma shiftr1_code [code]:
|
|
142 |
\<open>shiftr1 w = drop_bit 1 w\<close>
|
|
143 |
by transfer (simp add: drop_bit_Suc)
|
|
144 |
|
|
145 |
lemma shiftl_def:
|
|
146 |
\<open>w << n = (shiftl1 ^^ n) w\<close>
|
|
147 |
proof -
|
|
148 |
have \<open>push_bit n = (((*) 2 ^^ n) :: int \<Rightarrow> int)\<close> for n
|
|
149 |
by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps)
|
|
150 |
then show ?thesis
|
|
151 |
by transfer simp
|
|
152 |
qed
|
|
153 |
|
|
154 |
lemma shiftr_def:
|
|
155 |
\<open>w >> n = (shiftr1 ^^ n) w\<close>
|
|
156 |
proof -
|
|
157 |
have \<open>shiftr1 ^^ n = (drop_bit n :: 'a word \<Rightarrow> 'a word)\<close>
|
|
158 |
apply (induction n)
|
|
159 |
apply simp
|
|
160 |
apply (simp only: shiftr1_eq_div_2 [abs_def] drop_bit_eq_div [abs_def] funpow_Suc_right)
|
|
161 |
apply (use div_exp_eq [of _ 1, where ?'a = \<open>'a word\<close>] in simp)
|
|
162 |
done
|
|
163 |
then show ?thesis
|
|
164 |
by (simp add: shiftr_eq_drop_bit)
|
|
165 |
qed
|
|
166 |
|
|
167 |
lemma bit_shiftl_word_iff:
|
|
168 |
\<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
|
|
169 |
for w :: \<open>'a::len word\<close>
|
|
170 |
by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le)
|
|
171 |
|
|
172 |
lemma bit_shiftr_word_iff:
|
|
173 |
\<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
|
|
174 |
for w :: \<open>'a::len word\<close>
|
|
175 |
by (simp add: shiftr_word_eq bit_drop_bit_eq)
|
|
176 |
|
|
177 |
lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55)
|
|
178 |
is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))\<close>
|
|
179 |
by (simp flip: signed_take_bit_decr_length_iff)
|
|
180 |
|
|
181 |
lemma sshiftr_eq [code]:
|
|
182 |
\<open>w >>> n = signed_drop_bit n w\<close>
|
|
183 |
by transfer simp
|
|
184 |
|
|
185 |
lemma sshiftr_eq_funpow_sshiftr1:
|
|
186 |
\<open>w >>> n = (sshiftr1 ^^ n) w\<close>
|
|
187 |
apply (rule sym)
|
|
188 |
apply (simp add: sshiftr1_eq_signed_drop_bit_Suc_0 sshiftr_eq)
|
|
189 |
apply (induction n)
|
|
190 |
apply simp_all
|
|
191 |
done
|
|
192 |
|
|
193 |
lemma uint_sshiftr_eq:
|
|
194 |
\<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\<close>
|
|
195 |
for w :: \<open>'a::len word\<close>
|
|
196 |
by transfer (simp flip: drop_bit_eq_div)
|
|
197 |
|
|
198 |
lemma sshift1_code [code]:
|
|
199 |
\<open>sshiftr1 w = signed_drop_bit 1 w\<close>
|
|
200 |
by transfer (simp add: drop_bit_Suc)
|
|
201 |
|
|
202 |
lemma sshiftr_0 [simp]: "0 >>> n = 0"
|
|
203 |
by transfer simp
|
|
204 |
|
|
205 |
lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
|
|
206 |
by transfer simp
|
|
207 |
|
|
208 |
lemma bit_sshiftr_word_iff:
|
|
209 |
\<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\<close>
|
|
210 |
for w :: \<open>'a::len word\<close>
|
|
211 |
apply transfer
|
|
212 |
apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le simp flip: bit_Suc)
|
|
213 |
using le_less_Suc_eq apply fastforce
|
|
214 |
using le_less_Suc_eq apply fastforce
|
|
215 |
done
|
|
216 |
|
|
217 |
lemma nth_sshiftr :
|
|
218 |
"(w >>> m) !! n =
|
|
219 |
(n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
|
|
220 |
apply transfer
|
|
221 |
apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le ac_simps)
|
|
222 |
using le_less_Suc_eq apply fastforce
|
|
223 |
using le_less_Suc_eq apply fastforce
|
|
224 |
done
|
|
225 |
|
|
226 |
lemma sshiftr_numeral [simp]:
|
|
227 |
\<open>(numeral k >>> numeral n :: 'a::len word) =
|
|
228 |
word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k)))\<close>
|
|
229 |
apply (rule word_eqI)
|
|
230 |
apply (cases \<open>LENGTH('a)\<close>)
|
|
231 |
apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
|
|
232 |
done
|
|
233 |
|
|
234 |
lemma revcast_down_us [OF refl]:
|
|
235 |
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
|
|
236 |
for w :: "'a::len word"
|
|
237 |
apply (simp add: source_size_def target_size_def)
|
|
238 |
apply (rule bit_word_eqI)
|
|
239 |
apply (simp add: bit_revcast_iff bit_ucast_iff bit_sshiftr_word_iff ac_simps)
|
|
240 |
done
|
|
241 |
|
|
242 |
lemma revcast_down_ss [OF refl]:
|
|
243 |
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
|
|
244 |
for w :: "'a::len word"
|
|
245 |
apply (simp add: source_size_def target_size_def)
|
|
246 |
apply (rule bit_word_eqI)
|
|
247 |
apply (simp add: bit_revcast_iff bit_word_scast_iff bit_sshiftr_word_iff ac_simps)
|
|
248 |
done
|
|
249 |
|
|
250 |
lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n"
|
|
251 |
using sint_signed_drop_bit_eq [of n w]
|
|
252 |
by (simp add: drop_bit_eq_div sshiftr_eq)
|
|
253 |
|
|
254 |
lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
|
|
255 |
|
|
256 |
lemma nth_sint:
|
|
257 |
fixes w :: "'a::len word"
|
|
258 |
defines "l \<equiv> LENGTH('a)"
|
|
259 |
shows "bit (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
|
|
260 |
unfolding sint_uint l_def
|
|
261 |
by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)
|
|
262 |
|
|
263 |
lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
|
|
264 |
by transfer (auto simp add: bit_exp_iff)
|
|
265 |
|
|
266 |
lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)"
|
|
267 |
by transfer (auto simp add: bit_exp_iff)
|
|
268 |
|
|
269 |
lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
|
|
270 |
for x :: "'a::len word"
|
|
271 |
apply (rule xtrans(3))
|
|
272 |
apply (rule_tac [2] y = "x" in le_word_or2)
|
|
273 |
apply (rule word_eqI)
|
|
274 |
apply (auto simp add: word_ao_nth nth_w2p word_size)
|
|
275 |
done
|
|
276 |
|
|
277 |
lemma mask_eq:
|
|
278 |
\<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
|
|
279 |
by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1)
|
|
280 |
|
|
281 |
lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
|
|
282 |
by transfer (simp add: bit_take_bit_iff ac_simps)
|
|
283 |
|
|
284 |
lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0"
|
|
285 |
by transfer simp
|
|
286 |
|
|
287 |
lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0"
|
|
288 |
by transfer simp
|
|
289 |
|
|
290 |
lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
|
|
291 |
by transfer (auto simp add: bit_double_iff)
|
|
292 |
|
|
293 |
lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
|
|
294 |
for w :: "'a::len word"
|
|
295 |
by transfer (auto simp add: bit_push_bit_iff)
|
|
296 |
|
|
297 |
lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
|
|
298 |
|
|
299 |
lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
|
|
300 |
by transfer (auto simp add: bit_take_bit_iff simp flip: bit_Suc)
|
|
301 |
|
|
302 |
lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
|
|
303 |
for w :: "'a::len word"
|
|
304 |
apply (unfold shiftr_def)
|
|
305 |
apply (induct "m" arbitrary: n)
|
|
306 |
apply (auto simp add: nth_shiftr1)
|
|
307 |
done
|
|
308 |
|
|
309 |
lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
|
|
310 |
apply transfer
|
|
311 |
apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc)
|
|
312 |
using le_less_Suc_eq apply fastforce
|
|
313 |
using le_less_Suc_eq apply fastforce
|
|
314 |
done
|
|
315 |
|
|
316 |
lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
|
|
317 |
by (fact uint_shiftr_eq)
|
|
318 |
|
|
319 |
lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
|
|
320 |
by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
|
|
321 |
|
|
322 |
lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
|
|
323 |
by (simp add: shiftl_rev)
|
|
324 |
|
|
325 |
lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
|
|
326 |
by (simp add: rev_shiftl)
|
|
327 |
|
|
328 |
lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
|
|
329 |
by (simp add: shiftr_rev)
|
|
330 |
|
|
331 |
lemma shiftl_numeral [simp]:
|
|
332 |
\<open>numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\<close>
|
|
333 |
by (fact shiftl_word_eq)
|
|
334 |
|
|
335 |
lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
|
|
336 |
for x :: "'a::len word"
|
|
337 |
apply transfer
|
|
338 |
apply (simp add: take_bit_push_bit)
|
|
339 |
done
|
|
340 |
|
|
341 |
lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
|
|
342 |
for w :: "'a::len word"
|
|
343 |
by (induct n) (auto simp: shiftl_def shiftl1_2t)
|
|
344 |
|
|
345 |
lemma shiftr_numeral [simp]:
|
|
346 |
\<open>(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\<close>
|
|
347 |
by (fact shiftr_word_eq)
|
|
348 |
|
|
349 |
lemma nth_mask [simp]:
|
|
350 |
\<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
|
|
351 |
by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)
|
|
352 |
|
|
353 |
lemma slice_shiftr: "slice n w = ucast (w >> n)"
|
|
354 |
apply (rule bit_word_eqI)
|
|
355 |
apply (cases \<open>n \<le> LENGTH('b)\<close>)
|
|
356 |
apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps
|
|
357 |
dest: bit_imp_le_length)
|
|
358 |
done
|
|
359 |
|
|
360 |
lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
|
|
361 |
by (simp add: slice_shiftr nth_ucast nth_shiftr)
|
|
362 |
|
|
363 |
lemma revcast_down_uu [OF refl]:
|
|
364 |
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
|
|
365 |
for w :: "'a::len word"
|
|
366 |
apply (simp add: source_size_def target_size_def)
|
|
367 |
apply (rule bit_word_eqI)
|
|
368 |
apply (simp add: bit_revcast_iff bit_ucast_iff bit_shiftr_word_iff ac_simps)
|
|
369 |
done
|
|
370 |
|
|
371 |
lemma revcast_down_su [OF refl]:
|
|
372 |
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
|
|
373 |
for w :: "'a::len word"
|
|
374 |
apply (simp add: source_size_def target_size_def)
|
|
375 |
apply (rule bit_word_eqI)
|
|
376 |
apply (simp add: bit_revcast_iff bit_word_scast_iff bit_shiftr_word_iff ac_simps)
|
|
377 |
done
|
|
378 |
|
|
379 |
lemma cast_down_rev [OF refl]:
|
|
380 |
"uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
|
|
381 |
for w :: "'a::len word"
|
|
382 |
apply (simp add: source_size_def target_size_def)
|
|
383 |
apply (rule bit_word_eqI)
|
|
384 |
apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
|
|
385 |
done
|
|
386 |
|
|
387 |
lemma revcast_up [OF refl]:
|
|
388 |
"rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
|
|
389 |
rc w = (ucast w :: 'a::len word) << n"
|
|
390 |
apply (simp add: source_size_def target_size_def)
|
|
391 |
apply (rule bit_word_eqI)
|
|
392 |
apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
|
|
393 |
apply auto
|
|
394 |
apply (metis add.commute add_diff_cancel_right)
|
|
395 |
apply (metis diff_add_inverse2 diff_diff_add)
|
|
396 |
done
|
|
397 |
|
|
398 |
lemmas rc1 = revcast_up [THEN
|
|
399 |
revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
|
|
400 |
lemmas rc2 = revcast_down_uu [THEN
|
|
401 |
revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
|
|
402 |
|
|
403 |
lemmas ucast_up =
|
|
404 |
rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
|
|
405 |
lemmas ucast_down =
|
|
406 |
rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
|
|
407 |
|
|
408 |
\<comment> \<open>problem posed by TPHOLs referee:
|
|
409 |
criterion for overflow of addition of signed integers\<close>
|
|
410 |
|
|
411 |
lemma sofl_test:
|
|
412 |
\<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
|
|
413 |
(x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close>
|
|
414 |
for x y :: \<open>'a::len word\<close>
|
|
415 |
proof -
|
|
416 |
obtain n where n: \<open>LENGTH('a) = Suc n\<close>
|
|
417 |
by (cases \<open>LENGTH('a)\<close>) simp_all
|
|
418 |
have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
|
|
419 |
\<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
|
|
420 |
using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
|
|
421 |
by (auto intro: ccontr)
|
|
422 |
have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
|
|
423 |
(sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
|
|
424 |
(sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
|
|
425 |
using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
|
|
426 |
signed_take_bit_int_eq_self [of \<open>LENGTH('a) - 1\<close> \<open>sint x + sint y\<close>]
|
|
427 |
apply (auto simp add: not_less)
|
|
428 |
apply (unfold sint_word_ariths)
|
|
429 |
apply (subst signed_take_bit_int_eq_self)
|
|
430 |
prefer 4
|
|
431 |
apply (subst signed_take_bit_int_eq_self)
|
|
432 |
prefer 7
|
|
433 |
apply (subst signed_take_bit_int_eq_self)
|
|
434 |
prefer 10
|
|
435 |
apply (subst signed_take_bit_int_eq_self)
|
|
436 |
apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
|
|
437 |
done
|
|
438 |
then show ?thesis
|
|
439 |
apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
|
|
440 |
apply (simp add: bit_last_iff)
|
|
441 |
done
|
|
442 |
qed
|
|
443 |
|
|
444 |
lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0"
|
|
445 |
for x :: "'a :: len word"
|
|
446 |
by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size)
|
|
447 |
|
|
448 |
lemma test_bit_cat [OF refl]:
|
|
449 |
"wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
|
|
450 |
(if n < size b then b !! n else a !! (n - size b)))"
|
|
451 |
apply (simp add: word_size not_less; transfer)
|
|
452 |
apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
|
|
453 |
done
|
|
454 |
|
|
455 |
\<comment> \<open>keep quantifiers for use in simplification\<close>
|
|
456 |
lemma test_bit_split':
|
|
457 |
"word_split c = (a, b) \<longrightarrow>
|
|
458 |
(\<forall>n m.
|
|
459 |
b !! n = (n < size b \<and> c !! n) \<and>
|
|
460 |
a !! m = (m < size a \<and> c !! (m + size b)))"
|
|
461 |
by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size
|
|
462 |
bit_drop_bit_eq ac_simps exp_eq_zero_iff
|
|
463 |
dest: bit_imp_le_length)
|
|
464 |
|
|
465 |
lemma test_bit_split:
|
|
466 |
"word_split c = (a, b) \<Longrightarrow>
|
|
467 |
(\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
|
|
468 |
(\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
|
|
469 |
by (simp add: test_bit_split')
|
|
470 |
|
|
471 |
lemma test_bit_split_eq:
|
|
472 |
"word_split c = (a, b) \<longleftrightarrow>
|
|
473 |
((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
|
|
474 |
(\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
|
|
475 |
apply (rule_tac iffI)
|
|
476 |
apply (rule_tac conjI)
|
|
477 |
apply (erule test_bit_split [THEN conjunct1])
|
|
478 |
apply (erule test_bit_split [THEN conjunct2])
|
|
479 |
apply (case_tac "word_split c")
|
|
480 |
apply (frule test_bit_split)
|
|
481 |
apply (erule trans)
|
|
482 |
apply (fastforce intro!: word_eqI simp add: word_size)
|
|
483 |
done
|
|
484 |
|
|
485 |
lemma test_bit_rcat:
|
|
486 |
"sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
|
|
487 |
(n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
|
|
488 |
for wl :: "'a::len word list"
|
|
489 |
by (simp add: word_size word_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
|
|
490 |
(simp add: test_bit_eq_bit)
|
|
491 |
|
|
492 |
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
|
|
493 |
|
|
494 |
lemma max_test_bit: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
|
|
495 |
by (fact nth_minus1)
|
|
496 |
|
|
497 |
lemma shiftr_x_0 [iff]: "x >> 0 = x"
|
|
498 |
for x :: "'a::len word"
|
|
499 |
by transfer simp
|
|
500 |
|
|
501 |
lemma shiftl_x_0 [simp]: "x << 0 = x"
|
|
502 |
for x :: "'a::len word"
|
|
503 |
by (simp add: shiftl_t2n)
|
|
504 |
|
|
505 |
lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
|
|
506 |
by (simp add: shiftl_t2n)
|
|
507 |
|
|
508 |
lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
|
|
509 |
by (induct n) (auto simp: shiftr_def)
|
|
510 |
|
|
511 |
lemma map_nth_0 [simp]: "map ((!!) (0::'a::len word)) xs = replicate (length xs) False"
|
|
512 |
by (induct xs) auto
|
|
513 |
|
|
514 |
lemma word_and_1:
|
|
515 |
"n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word"
|
|
516 |
by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I)
|
|
517 |
|
|
518 |
lemma test_bit_1' [simp]:
|
|
519 |
"(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
|
|
520 |
by simp
|
|
521 |
|
|
522 |
lemma shiftl0:
|
|
523 |
"x << 0 = (x :: 'a :: len word)"
|
|
524 |
by (fact shiftl_x_0)
|
|
525 |
|
|
526 |
end
|