161 proof - |
99 proof - |
162 have \<open>((=) ===> pcr_word) of_int of_int\<close> |
100 have \<open>((=) ===> pcr_word) of_int of_int\<close> |
163 by transfer_prover |
101 by transfer_prover |
164 then show ?thesis by (simp add: id_def) |
102 then show ?thesis by (simp add: id_def) |
165 qed |
103 qed |
166 |
|
167 end |
|
168 |
|
169 lemma word_exp_length_eq_0 [simp]: |
|
170 \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close> |
|
171 by transfer simp |
|
172 |
|
173 lemma uint_nonnegative: "0 \<le> uint w" |
|
174 by transfer simp |
|
175 |
|
176 lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" |
|
177 for w :: "'a::len word" |
|
178 by transfer (simp add: take_bit_eq_mod) |
|
179 |
|
180 lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" |
|
181 for w :: "'a::len word" |
|
182 using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) |
|
183 |
|
184 lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b" |
|
185 by transfer simp |
|
186 |
|
187 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b" |
|
188 using word_uint_eqI by auto |
|
189 |
|
190 lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close> |
|
191 is \<open>\<lambda>k. k\<close> . |
|
192 |
|
193 lemma Word_eq_word_of_int [code_post]: |
|
194 \<open>Word.Word = word_of_int\<close> |
|
195 by rule (transfer, rule) |
|
196 |
|
197 lemma uint_word_of_int_eq [code]: |
|
198 \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> |
|
199 by transfer rule |
|
200 |
|
201 lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" |
|
202 by (simp add: uint_word_of_int_eq take_bit_eq_mod) |
|
203 |
|
204 lemma word_of_int_uint: "word_of_int (uint w) = w" |
|
205 by transfer simp |
|
206 |
|
207 lemma split_word_all: "(\<And>x::'a::len word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))" |
|
208 proof |
|
209 fix x :: "'a word" |
|
210 assume "\<And>x. PROP P (word_of_int x)" |
|
211 then have "PROP P (word_of_int (uint x))" . |
|
212 then show "PROP P x" by (simp add: word_of_int_uint) |
|
213 qed |
|
214 |
|
215 lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close> |
|
216 \<comment> \<open>treats the most-significant bit as a sign bit\<close> |
|
217 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
|
218 by (simp add: signed_take_bit_decr_length_iff) |
|
219 |
|
220 lemma sint_uint [code]: |
|
221 \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close> |
|
222 for w :: \<open>'a::len word\<close> |
|
223 by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit) |
|
224 |
|
225 lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close> |
|
226 is \<open>nat \<circ> take_bit LENGTH('a)\<close> |
|
227 by transfer simp |
|
228 |
|
229 lemma nat_uint_eq [simp]: |
|
230 \<open>nat (uint w) = unat w\<close> |
|
231 by transfer simp |
|
232 |
|
233 lemma unat_eq_nat_uint [code]: |
|
234 \<open>unat w = nat (uint w)\<close> |
|
235 by simp |
|
236 |
|
237 lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
238 is \<open>take_bit LENGTH('a)\<close> |
|
239 by simp |
|
240 |
|
241 lemma ucast_eq [code]: |
|
242 \<open>ucast w = word_of_int (uint w)\<close> |
|
243 by transfer simp |
|
244 |
|
245 lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
246 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
|
247 by (simp flip: signed_take_bit_decr_length_iff) |
|
248 |
|
249 lemma scast_eq [code]: |
|
250 \<open>scast w = word_of_int (sint w)\<close> |
|
251 by transfer simp |
|
252 |
|
253 lemma uint_0_eq [simp]: |
|
254 \<open>uint 0 = 0\<close> |
|
255 by transfer simp |
|
256 |
|
257 lemma uint_1_eq [simp]: |
|
258 \<open>uint 1 = 1\<close> |
|
259 by transfer simp |
|
260 |
|
261 lemma word_m1_wi: "- 1 = word_of_int (- 1)" |
|
262 by transfer rule |
|
263 |
|
264 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" |
|
265 by (simp add: word_uint_eq_iff) |
|
266 |
|
267 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" |
|
268 by transfer (auto intro: antisym) |
|
269 |
|
270 lemma unat_0 [simp]: "unat 0 = 0" |
|
271 by transfer simp |
|
272 |
|
273 lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" |
|
274 by (auto simp: unat_0_iff [symmetric]) |
|
275 |
|
276 lemma ucast_0 [simp]: "ucast 0 = 0" |
|
277 by transfer simp |
|
278 |
|
279 lemma sint_0 [simp]: "sint 0 = 0" |
|
280 by (simp add: sint_uint) |
|
281 |
|
282 lemma scast_0 [simp]: "scast 0 = 0" |
|
283 by transfer simp |
|
284 |
|
285 lemma sint_n1 [simp] : "sint (- 1) = - 1" |
|
286 by transfer simp |
|
287 |
|
288 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
|
289 by transfer simp |
|
290 |
|
291 lemma uint_1: "uint (1::'a::len word) = 1" |
|
292 by (fact uint_1_eq) |
|
293 |
|
294 lemma unat_1 [simp]: "unat (1::'a::len word) = 1" |
|
295 by transfer simp |
|
296 |
|
297 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" |
|
298 by transfer simp |
|
299 |
|
300 instantiation word :: (len) size |
|
301 begin |
|
302 |
|
303 lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close> |
|
304 is \<open>\<lambda>_. LENGTH('a)\<close> .. |
|
305 |
|
306 instance .. |
|
307 |
|
308 end |
|
309 |
|
310 lemma word_size [code]: |
|
311 \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
|
312 by (fact size_word.rep_eq) |
|
313 |
|
314 lemma word_size_gt_0 [iff]: "0 < size w" |
|
315 for w :: "'a::len word" |
|
316 by (simp add: word_size) |
|
317 |
|
318 lemmas lens_gt_0 = word_size_gt_0 len_gt_0 |
|
319 |
|
320 lemma lens_not_0 [iff]: |
|
321 \<open>size w \<noteq> 0\<close> for w :: \<open>'a::len word\<close> |
|
322 by auto |
|
323 |
|
324 lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close> |
|
325 is \<open>\<lambda>_. LENGTH('a)\<close> . |
|
326 |
|
327 lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close> |
|
328 is \<open>\<lambda>_. LENGTH('b)\<close> .. |
|
329 |
|
330 lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
|
331 is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> .. |
|
332 |
|
333 lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
|
334 is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> .. |
|
335 |
|
336 lemma is_up_eq: |
|
337 \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close> |
|
338 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
339 by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq) |
|
340 |
|
341 lemma is_down_eq: |
|
342 \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close> |
|
343 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
344 by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq) |
|
345 |
|
346 lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close> |
|
347 is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp |
|
348 |
|
349 lemma word_int_case_eq_uint [code]: |
|
350 \<open>word_int_case f w = f (uint w)\<close> |
|
351 by transfer simp |
|
352 |
|
353 translations |
|
354 "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" |
|
355 "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" |
|
356 |
|
357 |
|
358 subsection \<open>Type-definition locale instantiations\<close> |
|
359 |
|
360 definition uints :: "nat \<Rightarrow> int set" |
|
361 \<comment> \<open>the sets of integers representing the words\<close> |
|
362 where "uints n = range (take_bit n)" |
|
363 |
|
364 definition sints :: "nat \<Rightarrow> int set" |
|
365 where "sints n = range (signed_take_bit (n - 1))" |
|
366 |
|
367 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" |
|
368 by (simp add: uints_def range_bintrunc) |
|
369 |
|
370 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}" |
|
371 by (simp add: sints_def range_sbintrunc) |
|
372 |
|
373 definition unats :: "nat \<Rightarrow> nat set" |
|
374 where "unats n = {i. i < 2 ^ n}" |
|
375 |
|
376 \<comment> \<open>naturals\<close> |
|
377 lemma uints_unats: "uints n = int ` unats n" |
|
378 apply (unfold unats_def uints_num) |
|
379 apply safe |
|
380 apply (rule_tac image_eqI) |
|
381 apply (erule_tac nat_0_le [symmetric]) |
|
382 by auto |
|
383 |
|
384 lemma unats_uints: "unats n = nat ` uints n" |
|
385 by (auto simp: uints_unats image_iff) |
|
386 |
|
387 lemma td_ext_uint: |
|
388 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
389 (\<lambda>w::int. w mod 2 ^ LENGTH('a))" |
|
390 apply (unfold td_ext_def') |
|
391 apply transfer |
|
392 apply (simp add: uints_num take_bit_eq_mod) |
|
393 done |
|
394 |
|
395 interpretation word_uint: |
|
396 td_ext |
|
397 "uint::'a::len word \<Rightarrow> int" |
|
398 word_of_int |
|
399 "uints (LENGTH('a::len))" |
|
400 "\<lambda>w. w mod 2 ^ LENGTH('a::len)" |
|
401 by (fact td_ext_uint) |
|
402 |
|
403 lemmas td_uint = word_uint.td_thm |
|
404 lemmas int_word_uint = word_uint.eq_norm |
|
405 |
|
406 lemma td_ext_ubin: |
|
407 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
408 (take_bit (LENGTH('a)))" |
|
409 apply standard |
|
410 apply transfer |
|
411 apply simp |
|
412 done |
|
413 |
|
414 interpretation word_ubin: |
|
415 td_ext |
|
416 "uint::'a::len word \<Rightarrow> int" |
|
417 word_of_int |
|
418 "uints (LENGTH('a::len))" |
|
419 "take_bit (LENGTH('a::len))" |
|
420 by (fact td_ext_ubin) |
|
421 |
|
422 lemma td_ext_unat [OF refl]: |
|
423 "n = LENGTH('a::len) \<Longrightarrow> |
|
424 td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" |
|
425 apply (standard; transfer) |
|
426 apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self) |
|
427 apply (simp add: take_bit_eq_mod) |
|
428 done |
|
429 |
|
430 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] |
|
431 |
|
432 interpretation word_unat: |
|
433 td_ext |
|
434 "unat::'a::len word \<Rightarrow> nat" |
|
435 of_nat |
|
436 "unats (LENGTH('a::len))" |
|
437 "\<lambda>i. i mod 2 ^ LENGTH('a::len)" |
|
438 by (rule td_ext_unat) |
|
439 |
|
440 lemmas td_unat = word_unat.td_thm |
|
441 |
|
442 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] |
|
443 |
|
444 lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))" |
|
445 for z :: "'a::len word" |
|
446 apply (unfold unats_def) |
|
447 apply clarsimp |
|
448 apply (rule xtrans, rule unat_lt2p, assumption) |
|
449 done |
|
450 |
|
451 lemma td_ext_sbin: |
|
452 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
453 (signed_take_bit (LENGTH('a) - 1))" |
|
454 apply (unfold td_ext_def' sint_uint) |
|
455 apply (simp add : word_ubin.eq_norm) |
|
456 apply (cases "LENGTH('a)") |
|
457 apply (auto simp add : sints_def) |
|
458 apply (rule sym [THEN trans]) |
|
459 apply (rule word_ubin.Abs_norm) |
|
460 apply (simp only: bintrunc_sbintrunc) |
|
461 apply (drule sym) |
|
462 apply simp |
|
463 done |
|
464 |
|
465 lemma td_ext_sint: |
|
466 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
467 (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - |
|
468 2 ^ (LENGTH('a) - 1))" |
|
469 using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) |
|
470 |
|
471 text \<open> |
|
472 We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version |
|
473 and interpretations do not produce thm duplicates. I.e. |
|
474 we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>, |
|
475 because the latter is the same thm as the former. |
|
476 \<close> |
|
477 interpretation word_sint: |
|
478 td_ext |
|
479 "sint ::'a::len word \<Rightarrow> int" |
|
480 word_of_int |
|
481 "sints (LENGTH('a::len))" |
|
482 "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) - |
|
483 2 ^ (LENGTH('a::len) - 1)" |
|
484 by (rule td_ext_sint) |
|
485 |
|
486 interpretation word_sbin: |
|
487 td_ext |
|
488 "sint ::'a::len word \<Rightarrow> int" |
|
489 word_of_int |
|
490 "sints (LENGTH('a::len))" |
|
491 "signed_take_bit (LENGTH('a::len) - 1)" |
|
492 by (rule td_ext_sbin) |
|
493 |
|
494 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm] |
|
495 |
|
496 lemmas td_sint = word_sint.td |
|
497 |
|
498 |
|
499 subsection \<open>Arithmetic operations\<close> |
|
500 |
|
501 instantiation word :: (len) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" |
|
502 begin |
|
503 |
|
504 lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
505 is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b" |
|
506 by simp |
|
507 |
|
508 lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
509 is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b" |
|
510 by simp |
|
511 |
|
512 instance |
|
513 by standard (transfer, simp add: algebra_simps)+ |
|
514 |
|
515 end |
|
516 |
|
517 lemma word_div_def [code]: |
|
518 "a div b = word_of_int (uint a div uint b)" |
|
519 by transfer rule |
|
520 |
|
521 lemma word_mod_def [code]: |
|
522 "a mod b = word_of_int (uint a mod uint b)" |
|
523 by transfer rule |
|
524 |
|
525 |
|
526 |
|
527 text \<open>Legacy theorems:\<close> |
|
528 |
|
529 lemma word_add_def [code]: |
|
530 "a + b = word_of_int (uint a + uint b)" |
|
531 by transfer (simp add: take_bit_add) |
|
532 |
|
533 lemma word_sub_wi [code]: |
|
534 "a - b = word_of_int (uint a - uint b)" |
|
535 by transfer (simp add: take_bit_diff) |
|
536 |
|
537 lemma word_mult_def [code]: |
|
538 "a * b = word_of_int (uint a * uint b)" |
|
539 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
540 |
|
541 lemma word_minus_def [code]: |
|
542 "- a = word_of_int (- uint a)" |
|
543 by transfer (simp add: take_bit_minus) |
|
544 |
|
545 lemma word_0_wi: |
|
546 "0 = word_of_int 0" |
|
547 by transfer simp |
|
548 |
|
549 lemma word_1_wi: |
|
550 "1 = word_of_int 1" |
|
551 by transfer simp |
|
552 |
|
553 lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" |
|
554 by (auto simp add: take_bit_eq_mod intro: mod_add_cong) |
|
555 |
|
556 lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1" |
|
557 by (auto simp add: take_bit_eq_mod intro: mod_diff_cong) |
|
558 |
|
559 lemma word_succ_alt [code]: |
|
560 "word_succ a = word_of_int (uint a + 1)" |
|
561 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
562 |
|
563 lemma word_pred_alt [code]: |
|
564 "word_pred a = word_of_int (uint a - 1)" |
|
565 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
566 |
|
567 lemmas word_arith_wis = |
|
568 word_add_def word_sub_wi word_mult_def |
|
569 word_minus_def word_succ_alt word_pred_alt |
|
570 word_0_wi word_1_wi |
|
571 |
|
572 lemma wi_homs: |
|
573 shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" |
|
574 and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" |
|
575 and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" |
|
576 and wi_hom_neg: "- word_of_int a = word_of_int (- a)" |
|
577 and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" |
|
578 and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)" |
|
579 by (transfer, simp)+ |
|
580 |
|
581 lemmas wi_hom_syms = wi_homs [symmetric] |
|
582 |
|
583 lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi |
|
584 |
|
585 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] |
|
586 |
|
587 instance word :: (len) comm_monoid_add .. |
|
588 |
|
589 instance word :: (len) semiring_numeral .. |
|
590 |
|
591 lemma word_of_nat: "of_nat n = word_of_int (int n)" |
|
592 by (induct n) (auto simp add : word_of_int_hom_syms) |
|
593 |
|
594 lemma word_of_int: "of_int = word_of_int" |
|
595 apply (rule ext) |
|
596 apply (case_tac x rule: int_diff_cases) |
|
597 apply (simp add: word_of_nat wi_hom_sub) |
|
598 done |
|
599 |
|
600 lemma word_of_int_eq: |
|
601 "word_of_int = of_int" |
|
602 by (rule ext) (transfer, rule) |
|
603 |
|
604 definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50) |
|
605 where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)" |
|
606 |
|
607 context |
|
608 includes lifting_syntax |
|
609 begin |
|
610 |
104 |
611 lemma [transfer_rule]: |
105 lemma [transfer_rule]: |
612 \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close> |
106 \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close> |
613 proof - |
107 proof - |
614 have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q") |
108 have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q") |
629 transfer_prover |
123 transfer_prover |
630 qed |
124 qed |
631 |
125 |
632 end |
126 end |
633 |
127 |
634 instance word :: (len) semiring_modulo |
128 lemma word_exp_length_eq_0 [simp]: |
635 proof |
129 \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close> |
|
130 by transfer simp |
|
131 |
|
132 |
|
133 subsubsection \<open>Basic code generation setup\<close> |
|
134 |
|
135 lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close> |
|
136 is \<open>take_bit LENGTH('a)\<close> . |
|
137 |
|
138 lemma [code abstype]: |
|
139 \<open>Word.Word (uint w) = w\<close> |
|
140 by transfer simp |
|
141 |
|
142 quickcheck_generator word |
|
143 constructors: |
|
144 \<open>0 :: 'a::len word\<close>, |
|
145 \<open>numeral :: num \<Rightarrow> 'a::len word\<close> |
|
146 |
|
147 instantiation word :: (len) equal |
|
148 begin |
|
149 |
|
150 lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close> |
|
151 is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
152 by simp |
|
153 |
|
154 instance |
|
155 by (standard; transfer) rule |
|
156 |
|
157 end |
|
158 |
|
159 lemma [code]: |
|
160 \<open>HOL.equal v w \<longleftrightarrow> HOL.equal (uint v) (uint w)\<close> |
|
161 by transfer (simp add: equal) |
|
162 |
|
163 lemma [code]: |
|
164 \<open>uint 0 = 0\<close> |
|
165 by transfer simp |
|
166 |
|
167 lemma [code]: |
|
168 \<open>uint 1 = 1\<close> |
|
169 by transfer simp |
|
170 |
|
171 lemma [code]: |
|
172 \<open>uint (v + w) = take_bit LENGTH('a) (uint v + uint w)\<close> |
|
173 for v w :: \<open>'a::len word\<close> |
|
174 by transfer (simp add: take_bit_add) |
|
175 |
|
176 lemma [code]: |
|
177 \<open>uint (- w) = (let k = uint w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close> |
|
178 for w :: \<open>'a::len word\<close> |
|
179 by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if) |
|
180 |
|
181 lemma [code]: |
|
182 \<open>uint (v - w) = take_bit LENGTH('a) (uint v - uint w)\<close> |
|
183 for v w :: \<open>'a::len word\<close> |
|
184 by transfer (simp add: take_bit_diff) |
|
185 |
|
186 lemma [code]: |
|
187 \<open>uint (v * w) = take_bit LENGTH('a) (uint v * uint w)\<close> |
|
188 for v w :: \<open>'a::len word\<close> |
|
189 by transfer (simp add: take_bit_mult) |
|
190 |
|
191 |
|
192 subsubsection \<open>Basic conversions\<close> |
|
193 |
|
194 lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close> |
|
195 is \<open>\<lambda>k. k\<close> . |
|
196 |
|
197 lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close> |
|
198 is \<open>nat \<circ> take_bit LENGTH('a)\<close> |
|
199 by simp |
|
200 |
|
201 lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close> |
|
202 \<comment> \<open>treats the most-significant bit as a sign bit\<close> |
|
203 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
|
204 by (simp add: signed_take_bit_decr_length_iff) |
|
205 |
|
206 lemma nat_uint_eq [simp]: |
|
207 \<open>nat (uint w) = unat w\<close> |
|
208 by transfer simp |
|
209 |
|
210 lemma of_nat_word_eq_iff: |
|
211 \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close> |
|
212 by transfer (simp add: take_bit_of_nat) |
|
213 |
|
214 lemma of_nat_word_eq_0_iff: |
|
215 \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close> |
|
216 using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) |
|
217 |
|
218 lemma of_int_word_eq_iff: |
|
219 \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
220 by transfer rule |
|
221 |
|
222 lemma of_int_word_eq_0_iff: |
|
223 \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close> |
|
224 using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) |
|
225 |
|
226 |
|
227 subsubsection \<open>Basic ordering\<close> |
|
228 |
|
229 instantiation word :: (len) linorder |
|
230 begin |
|
231 |
|
232 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
233 is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b" |
|
234 by simp |
|
235 |
|
236 lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
237 is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" |
|
238 by simp |
|
239 |
|
240 instance |
|
241 by (standard; transfer) auto |
|
242 |
|
243 end |
|
244 |
|
245 interpretation word_order: ordering_top \<open>(\<le>)\<close> \<open>(<)\<close> \<open>- 1 :: 'a::len word\<close> |
|
246 by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1) |
|
247 |
|
248 interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close> |
|
249 by (standard; transfer) simp |
|
250 |
|
251 lemma word_le_def [code]: |
|
252 "a \<le> b \<longleftrightarrow> uint a \<le> uint b" |
|
253 by transfer rule |
|
254 |
|
255 lemma word_less_def [code]: |
|
256 "a < b \<longleftrightarrow> uint a < uint b" |
|
257 by transfer rule |
|
258 |
|
259 lemma word_greater_zero_iff: |
|
260 \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> |
|
261 by transfer (simp add: less_le) |
|
262 |
|
263 lemma of_nat_word_less_eq_iff: |
|
264 \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close> |
|
265 by transfer (simp add: take_bit_of_nat) |
|
266 |
|
267 lemma of_nat_word_less_iff: |
|
268 \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close> |
|
269 by transfer (simp add: take_bit_of_nat) |
|
270 |
|
271 lemma of_int_word_less_eq_iff: |
|
272 \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close> |
|
273 by transfer rule |
|
274 |
|
275 lemma of_int_word_less_iff: |
|
276 \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close> |
|
277 by transfer rule |
|
278 |
|
279 |
|
280 subsection \<open>Bit-wise operations\<close> |
|
281 |
|
282 instantiation word :: (len) semiring_modulo |
|
283 begin |
|
284 |
|
285 lift_definition divide_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
|
286 is \<open>\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b\<close> |
|
287 by simp |
|
288 |
|
289 lift_definition modulo_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
|
290 is \<open>\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b\<close> |
|
291 by simp |
|
292 |
|
293 instance proof |
636 show "a div b * b + a mod b = a" for a b :: "'a word" |
294 show "a div b * b + a mod b = a" for a b :: "'a word" |
637 proof transfer |
295 proof transfer |
638 fix k l :: int |
296 fix k l :: int |
639 define r :: int where "r = 2 ^ LENGTH('a)" |
297 define r :: int where "r = 2 ^ LENGTH('a)" |
640 then have r: "take_bit LENGTH('a) k = k mod r" for k |
298 then have r: "take_bit LENGTH('a) k = k mod r" for k |
666 by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) |
326 by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) |
667 show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" |
327 show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" |
668 for a :: "'a word" |
328 for a :: "'a word" |
669 by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) |
329 by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) |
670 qed |
330 qed |
671 |
|
672 lemma exp_eq_zero_iff: |
|
673 \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close> |
|
674 by transfer simp |
|
675 |
|
676 lemma double_eq_zero_iff: |
|
677 \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
678 for a :: \<open>'a::len word\<close> |
|
679 proof - |
|
680 define n where \<open>n = LENGTH('a) - Suc 0\<close> |
|
681 then have *: \<open>LENGTH('a) = Suc n\<close> |
|
682 by simp |
|
683 have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
684 using that by transfer |
|
685 (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *) |
|
686 moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close> |
|
687 by transfer simp |
|
688 then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close> |
|
689 by (simp add: *) |
|
690 ultimately show ?thesis |
|
691 by auto |
|
692 qed |
|
693 |
|
694 |
|
695 subsection \<open>Ordering\<close> |
|
696 |
|
697 instantiation word :: (len) linorder |
|
698 begin |
|
699 |
|
700 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
701 is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b" |
|
702 by simp |
|
703 |
|
704 lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
705 is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" |
|
706 by simp |
|
707 |
|
708 instance |
|
709 by (standard; transfer) auto |
|
710 |
|
711 end |
|
712 |
|
713 interpretation word_order: ordering_top \<open>(\<le>)\<close> \<open>(<)\<close> \<open>- 1 :: 'a::len word\<close> |
|
714 by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1) |
|
715 |
|
716 interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close> |
|
717 by (standard; transfer) simp |
|
718 |
|
719 lemma word_le_def [code]: |
|
720 "a \<le> b \<longleftrightarrow> uint a \<le> uint b" |
|
721 by transfer rule |
|
722 |
|
723 lemma word_less_def [code]: |
|
724 "a < b \<longleftrightarrow> uint a < uint b" |
|
725 by transfer rule |
|
726 |
|
727 lemma word_greater_zero_iff: |
|
728 \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> |
|
729 by transfer (simp add: less_le) |
|
730 |
|
731 lemma of_nat_word_eq_iff: |
|
732 \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close> |
|
733 by transfer (simp add: take_bit_of_nat) |
|
734 |
|
735 lemma of_nat_word_less_eq_iff: |
|
736 \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close> |
|
737 by transfer (simp add: take_bit_of_nat) |
|
738 |
|
739 lemma of_nat_word_less_iff: |
|
740 \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close> |
|
741 by transfer (simp add: take_bit_of_nat) |
|
742 |
|
743 lemma of_nat_word_eq_0_iff: |
|
744 \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close> |
|
745 using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) |
|
746 |
|
747 lemma of_int_word_eq_iff: |
|
748 \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
749 by transfer rule |
|
750 |
|
751 lemma of_int_word_less_eq_iff: |
|
752 \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close> |
|
753 by transfer rule |
|
754 |
|
755 lemma of_int_word_less_iff: |
|
756 \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close> |
|
757 by transfer rule |
|
758 |
|
759 lemma of_int_word_eq_0_iff: |
|
760 \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close> |
|
761 using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) |
|
762 |
|
763 lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <=s _)\<close> [50, 51] 50) |
|
764 is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k \<le> signed_take_bit (LENGTH('a) - 1) l\<close> |
|
765 by (simp flip: signed_take_bit_decr_length_iff) |
|
766 |
|
767 lemma word_sle_eq [code]: |
|
768 \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close> |
|
769 by transfer simp |
|
770 |
|
771 lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <s _)\<close> [50, 51] 50) |
|
772 is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k < signed_take_bit (LENGTH('a) - 1) l\<close> |
|
773 by (simp flip: signed_take_bit_decr_length_iff) |
|
774 |
|
775 lemma word_sless_eq: |
|
776 \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close> |
|
777 by transfer (simp add: signed_take_bit_decr_length_iff less_le) |
|
778 |
|
779 lemma [code]: |
|
780 \<open>a <s b \<longleftrightarrow> sint a < sint b\<close> |
|
781 by transfer simp |
|
782 |
|
783 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
|
784 by (fact word_less_def) |
|
785 |
|
786 lemma signed_linorder: "class.linorder word_sle word_sless" |
|
787 by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff) |
|
788 |
|
789 interpretation signed: linorder "word_sle" "word_sless" |
|
790 by (rule signed_linorder) |
|
791 |
|
792 lemma word_zero_le [simp]: "0 \<le> y" |
|
793 for y :: "'a::len word" |
|
794 by transfer simp |
|
795 |
|
796 lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *) |
|
797 by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p) |
|
798 |
|
799 lemma word_n1_ge [simp]: "y \<le> -1" |
|
800 for y :: "'a::len word" |
|
801 by (fact word_order.extremum) |
|
802 |
|
803 lemmas word_not_simps [simp] = |
|
804 word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] |
|
805 |
|
806 lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y" |
|
807 for y :: "'a::len word" |
|
808 by (simp add: less_le) |
|
809 |
|
810 lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y |
|
811 |
|
812 lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b" |
|
813 by (auto simp add: word_sle_eq word_sless_eq less_le) |
|
814 |
|
815 lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b" |
|
816 by transfer (simp add: nat_le_eq_zle) |
|
817 |
|
818 lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b" |
|
819 by transfer (auto simp add: less_le [of 0]) |
|
820 |
|
821 lemmas unat_mono = word_less_nat_alt [THEN iffD1] |
|
822 |
|
823 instance word :: (len) wellorder |
|
824 proof |
|
825 fix P :: "'a word \<Rightarrow> bool" and a |
|
826 assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)" |
|
827 have "wf (measure unat)" .. |
|
828 moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat" |
|
829 by (auto simp add: word_less_nat_alt) |
|
830 ultimately have "wf {(a, b :: ('a::len) word). a < b}" |
|
831 by (rule wf_subset) |
|
832 then show "P a" using * |
|
833 by induction blast |
|
834 qed |
|
835 |
|
836 lemma wi_less: |
|
837 "(word_of_int n < (word_of_int m :: 'a::len word)) = |
|
838 (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" |
|
839 unfolding word_less_alt by (simp add: word_uint.eq_norm) |
|
840 |
|
841 lemma wi_le: |
|
842 "(word_of_int n \<le> (word_of_int m :: 'a::len word)) = |
|
843 (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))" |
|
844 unfolding word_le_def by (simp add: word_uint.eq_norm) |
|
845 |
|
846 |
|
847 subsection \<open>Bit-wise operations\<close> |
|
848 |
331 |
849 lemma word_bit_induct [case_names zero even odd]: |
332 lemma word_bit_induct [case_names zero even odd]: |
850 \<open>P a\<close> if word_zero: \<open>P 0\<close> |
333 \<open>P a\<close> if word_zero: \<open>P 0\<close> |
851 and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close> |
334 and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close> |
852 and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close> |
335 and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close> |
1124 |
607 |
1125 lemma not_bit_length [simp]: |
608 lemma not_bit_length [simp]: |
1126 \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
609 \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
1127 by transfer simp |
610 by transfer simp |
1128 |
611 |
|
612 |
|
613 subsection \<open>Conversions including casts\<close> |
|
614 |
|
615 lemma uint_nonnegative: "0 \<le> uint w" |
|
616 by transfer simp |
|
617 |
|
618 lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" |
|
619 for w :: "'a::len word" |
|
620 by transfer (simp add: take_bit_eq_mod) |
|
621 |
|
622 lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" |
|
623 for w :: "'a::len word" |
|
624 using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) |
|
625 |
|
626 lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b" |
|
627 by transfer simp |
|
628 |
|
629 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b" |
|
630 using word_uint_eqI by auto |
|
631 |
|
632 lemma Word_eq_word_of_int [code_post]: |
|
633 \<open>Word.Word = word_of_int\<close> |
|
634 by rule (transfer, rule) |
|
635 |
|
636 lemma uint_word_of_int_eq [code]: |
|
637 \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> |
|
638 by transfer rule |
|
639 |
|
640 lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" |
|
641 by (simp add: uint_word_of_int_eq take_bit_eq_mod) |
|
642 |
|
643 lemma word_of_int_uint: "word_of_int (uint w) = w" |
|
644 by transfer simp |
|
645 |
|
646 lemma word_div_def [code]: |
|
647 "a div b = word_of_int (uint a div uint b)" |
|
648 by transfer rule |
|
649 |
|
650 lemma word_mod_def [code]: |
|
651 "a mod b = word_of_int (uint a mod uint b)" |
|
652 by transfer rule |
|
653 |
|
654 lemma split_word_all: "(\<And>x::'a::len word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))" |
|
655 proof |
|
656 fix x :: "'a word" |
|
657 assume "\<And>x. PROP P (word_of_int x)" |
|
658 then have "PROP P (word_of_int (uint x))" . |
|
659 then show "PROP P x" by (simp add: word_of_int_uint) |
|
660 qed |
|
661 |
|
662 lemma sint_uint [code]: |
|
663 \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close> |
|
664 for w :: \<open>'a::len word\<close> |
|
665 by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit) |
|
666 |
|
667 lemma unat_eq_nat_uint [code]: |
|
668 \<open>unat w = nat (uint w)\<close> |
|
669 by simp |
|
670 |
|
671 lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
672 is \<open>take_bit LENGTH('a)\<close> |
|
673 by simp |
|
674 |
|
675 lemma ucast_eq [code]: |
|
676 \<open>ucast w = word_of_int (uint w)\<close> |
|
677 by transfer simp |
|
678 |
|
679 lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
680 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
|
681 by (simp flip: signed_take_bit_decr_length_iff) |
|
682 |
|
683 lemma scast_eq [code]: |
|
684 \<open>scast w = word_of_int (sint w)\<close> |
|
685 by transfer simp |
|
686 |
|
687 lemma uint_0_eq [simp]: |
|
688 \<open>uint 0 = 0\<close> |
|
689 by transfer simp |
|
690 |
|
691 lemma uint_1_eq [simp]: |
|
692 \<open>uint 1 = 1\<close> |
|
693 by transfer simp |
|
694 |
|
695 lemma word_m1_wi: "- 1 = word_of_int (- 1)" |
|
696 by transfer rule |
|
697 |
|
698 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" |
|
699 by (simp add: word_uint_eq_iff) |
|
700 |
|
701 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" |
|
702 by transfer (auto intro: antisym) |
|
703 |
|
704 lemma unat_0 [simp]: "unat 0 = 0" |
|
705 by transfer simp |
|
706 |
|
707 lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" |
|
708 by (auto simp: unat_0_iff [symmetric]) |
|
709 |
|
710 lemma ucast_0 [simp]: "ucast 0 = 0" |
|
711 by transfer simp |
|
712 |
|
713 lemma sint_0 [simp]: "sint 0 = 0" |
|
714 by (simp add: sint_uint) |
|
715 |
|
716 lemma scast_0 [simp]: "scast 0 = 0" |
|
717 by transfer simp |
|
718 |
|
719 lemma sint_n1 [simp] : "sint (- 1) = - 1" |
|
720 by transfer simp |
|
721 |
|
722 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
|
723 by transfer simp |
|
724 |
|
725 lemma uint_1: "uint (1::'a::len word) = 1" |
|
726 by (fact uint_1_eq) |
|
727 |
|
728 lemma unat_1 [simp]: "unat (1::'a::len word) = 1" |
|
729 by transfer simp |
|
730 |
|
731 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" |
|
732 by transfer simp |
|
733 |
|
734 instantiation word :: (len) size |
|
735 begin |
|
736 |
|
737 lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close> |
|
738 is \<open>\<lambda>_. LENGTH('a)\<close> .. |
|
739 |
|
740 instance .. |
|
741 |
|
742 end |
|
743 |
|
744 lemma word_size [code]: |
|
745 \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
|
746 by (fact size_word.rep_eq) |
|
747 |
|
748 lemma word_size_gt_0 [iff]: "0 < size w" |
|
749 for w :: "'a::len word" |
|
750 by (simp add: word_size) |
|
751 |
|
752 lemmas lens_gt_0 = word_size_gt_0 len_gt_0 |
|
753 |
|
754 lemma lens_not_0 [iff]: |
|
755 \<open>size w \<noteq> 0\<close> for w :: \<open>'a::len word\<close> |
|
756 by auto |
|
757 |
|
758 lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close> |
|
759 is \<open>\<lambda>_. LENGTH('a)\<close> . |
|
760 |
|
761 lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close> |
|
762 is \<open>\<lambda>_. LENGTH('b)\<close> .. |
|
763 |
|
764 lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
|
765 is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> .. |
|
766 |
|
767 lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
|
768 is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> .. |
|
769 |
|
770 lemma is_up_eq: |
|
771 \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close> |
|
772 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
773 by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq) |
|
774 |
|
775 lemma is_down_eq: |
|
776 \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close> |
|
777 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
778 by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq) |
|
779 |
|
780 lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close> |
|
781 is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp |
|
782 |
|
783 lemma word_int_case_eq_uint [code]: |
|
784 \<open>word_int_case f w = f (uint w)\<close> |
|
785 by transfer simp |
|
786 |
|
787 translations |
|
788 "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" |
|
789 "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" |
|
790 |
|
791 |
|
792 subsection \<open>Arithmetic operations\<close> |
|
793 |
|
794 text \<open>Legacy theorems:\<close> |
|
795 |
|
796 lemma word_add_def [code]: |
|
797 "a + b = word_of_int (uint a + uint b)" |
|
798 by transfer (simp add: take_bit_add) |
|
799 |
|
800 lemma word_sub_wi [code]: |
|
801 "a - b = word_of_int (uint a - uint b)" |
|
802 by transfer (simp add: take_bit_diff) |
|
803 |
|
804 lemma word_mult_def [code]: |
|
805 "a * b = word_of_int (uint a * uint b)" |
|
806 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
807 |
|
808 lemma word_minus_def [code]: |
|
809 "- a = word_of_int (- uint a)" |
|
810 by transfer (simp add: take_bit_minus) |
|
811 |
|
812 lemma word_0_wi: |
|
813 "0 = word_of_int 0" |
|
814 by transfer simp |
|
815 |
|
816 lemma word_1_wi: |
|
817 "1 = word_of_int 1" |
|
818 by transfer simp |
|
819 |
|
820 lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" |
|
821 by (auto simp add: take_bit_eq_mod intro: mod_add_cong) |
|
822 |
|
823 lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1" |
|
824 by (auto simp add: take_bit_eq_mod intro: mod_diff_cong) |
|
825 |
|
826 lemma word_succ_alt [code]: |
|
827 "word_succ a = word_of_int (uint a + 1)" |
|
828 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
829 |
|
830 lemma word_pred_alt [code]: |
|
831 "word_pred a = word_of_int (uint a - 1)" |
|
832 by transfer (simp add: take_bit_eq_mod mod_simps) |
|
833 |
|
834 lemmas word_arith_wis = |
|
835 word_add_def word_sub_wi word_mult_def |
|
836 word_minus_def word_succ_alt word_pred_alt |
|
837 word_0_wi word_1_wi |
|
838 |
|
839 lemma wi_homs: |
|
840 shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" |
|
841 and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" |
|
842 and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" |
|
843 and wi_hom_neg: "- word_of_int a = word_of_int (- a)" |
|
844 and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" |
|
845 and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)" |
|
846 by (transfer, simp)+ |
|
847 |
|
848 lemmas wi_hom_syms = wi_homs [symmetric] |
|
849 |
|
850 lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi |
|
851 |
|
852 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] |
|
853 |
|
854 lemma word_of_nat: "of_nat n = word_of_int (int n)" |
|
855 by (induct n) (auto simp add : word_of_int_hom_syms) |
|
856 |
|
857 lemma word_of_int: "of_int = word_of_int" |
|
858 apply (rule ext) |
|
859 apply (case_tac x rule: int_diff_cases) |
|
860 apply (simp add: word_of_nat wi_hom_sub) |
|
861 done |
|
862 |
|
863 lemma word_of_int_eq: |
|
864 "word_of_int = of_int" |
|
865 by (rule ext) (transfer, rule) |
|
866 |
|
867 definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50) |
|
868 where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)" |
|
869 |
|
870 lemma exp_eq_zero_iff: |
|
871 \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close> |
|
872 by transfer simp |
|
873 |
|
874 lemma double_eq_zero_iff: |
|
875 \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
876 for a :: \<open>'a::len word\<close> |
|
877 proof - |
|
878 define n where \<open>n = LENGTH('a) - Suc 0\<close> |
|
879 then have *: \<open>LENGTH('a) = Suc n\<close> |
|
880 by simp |
|
881 have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
882 using that by transfer |
|
883 (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *) |
|
884 moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close> |
|
885 by transfer simp |
|
886 then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close> |
|
887 by (simp add: *) |
|
888 ultimately show ?thesis |
|
889 by auto |
|
890 qed |
|
891 |
|
892 |
|
893 subsection \<open>Ordering\<close> |
|
894 |
|
895 lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <=s _)\<close> [50, 51] 50) |
|
896 is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k \<le> signed_take_bit (LENGTH('a) - 1) l\<close> |
|
897 by (simp flip: signed_take_bit_decr_length_iff) |
|
898 |
|
899 lemma word_sle_eq [code]: |
|
900 \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close> |
|
901 by transfer simp |
|
902 |
|
903 lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <s _)\<close> [50, 51] 50) |
|
904 is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k < signed_take_bit (LENGTH('a) - 1) l\<close> |
|
905 by (simp flip: signed_take_bit_decr_length_iff) |
|
906 |
|
907 lemma word_sless_eq: |
|
908 \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close> |
|
909 by transfer (simp add: signed_take_bit_decr_length_iff less_le) |
|
910 |
|
911 lemma [code]: |
|
912 \<open>a <s b \<longleftrightarrow> sint a < sint b\<close> |
|
913 by transfer simp |
|
914 |
|
915 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
|
916 by (fact word_less_def) |
|
917 |
|
918 lemma signed_linorder: "class.linorder word_sle word_sless" |
|
919 by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff) |
|
920 |
|
921 interpretation signed: linorder "word_sle" "word_sless" |
|
922 by (rule signed_linorder) |
|
923 |
|
924 lemma word_zero_le [simp]: "0 \<le> y" |
|
925 for y :: "'a::len word" |
|
926 by transfer simp |
|
927 |
|
928 lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *) |
|
929 by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p) |
|
930 |
|
931 lemma word_n1_ge [simp]: "y \<le> -1" |
|
932 for y :: "'a::len word" |
|
933 by (fact word_order.extremum) |
|
934 |
|
935 lemmas word_not_simps [simp] = |
|
936 word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] |
|
937 |
|
938 lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y" |
|
939 for y :: "'a::len word" |
|
940 by (simp add: less_le) |
|
941 |
|
942 lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y |
|
943 |
|
944 lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b" |
|
945 by transfer simp |
|
946 |
|
947 lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b" |
|
948 by transfer (simp add: nat_le_eq_zle) |
|
949 |
|
950 lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b" |
|
951 by transfer (auto simp add: less_le [of 0]) |
|
952 |
|
953 lemmas unat_mono = word_less_nat_alt [THEN iffD1] |
|
954 |
|
955 instance word :: (len) wellorder |
|
956 proof |
|
957 fix P :: "'a word \<Rightarrow> bool" and a |
|
958 assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)" |
|
959 have "wf (measure unat)" .. |
|
960 moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat" |
|
961 by (auto simp add: word_less_nat_alt) |
|
962 ultimately have "wf {(a, b :: ('a::len) word). a < b}" |
|
963 by (rule wf_subset) |
|
964 then show "P a" using * |
|
965 by induction blast |
|
966 qed |
|
967 |
|
968 lemma wi_less: |
|
969 "(word_of_int n < (word_of_int m :: 'a::len word)) = |
|
970 (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" |
|
971 by transfer (simp add: take_bit_eq_mod) |
|
972 |
|
973 lemma wi_le: |
|
974 "(word_of_int n \<le> (word_of_int m :: 'a::len word)) = |
|
975 (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))" |
|
976 by transfer (simp add: take_bit_eq_mod) |
|
977 |
|
978 |
|
979 subsection \<open>Bit-wise operations\<close> |
|
980 |
|
981 |
1129 lemma uint_take_bit_eq [code]: |
982 lemma uint_take_bit_eq [code]: |
1130 \<open>uint (take_bit n w) = take_bit n (uint w)\<close> |
983 \<open>uint (take_bit n w) = take_bit n (uint w)\<close> |
1131 by transfer (simp add: ac_simps) |
984 by transfer (simp add: ac_simps) |
1132 |
985 |
1133 lemma take_bit_word_eq_self: |
986 lemma take_bit_word_eq_self: |
1471 moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close> |
1324 moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close> |
1472 by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+ |
1325 by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+ |
1473 ultimately show ?case |
1326 ultimately show ?case |
1474 by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp |
1327 by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp |
1475 qed |
1328 qed |
|
1329 |
|
1330 |
|
1331 subsection \<open>Type-definition locale instantiations\<close> |
|
1332 |
|
1333 definition uints :: "nat \<Rightarrow> int set" |
|
1334 \<comment> \<open>the sets of integers representing the words\<close> |
|
1335 where "uints n = range (take_bit n)" |
|
1336 |
|
1337 definition sints :: "nat \<Rightarrow> int set" |
|
1338 where "sints n = range (signed_take_bit (n - 1))" |
|
1339 |
|
1340 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" |
|
1341 by (simp add: uints_def range_bintrunc) |
|
1342 |
|
1343 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}" |
|
1344 by (simp add: sints_def range_sbintrunc) |
|
1345 |
|
1346 definition unats :: "nat \<Rightarrow> nat set" |
|
1347 where "unats n = {i. i < 2 ^ n}" |
|
1348 |
|
1349 \<comment> \<open>naturals\<close> |
|
1350 lemma uints_unats: "uints n = int ` unats n" |
|
1351 apply (unfold unats_def uints_num) |
|
1352 apply safe |
|
1353 apply (rule_tac image_eqI) |
|
1354 apply (erule_tac nat_0_le [symmetric]) |
|
1355 by auto |
|
1356 |
|
1357 lemma unats_uints: "unats n = nat ` uints n" |
|
1358 by (auto simp: uints_unats image_iff) |
|
1359 |
|
1360 lemma td_ext_uint: |
|
1361 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
1362 (\<lambda>w::int. w mod 2 ^ LENGTH('a))" |
|
1363 apply (unfold td_ext_def') |
|
1364 apply transfer |
|
1365 apply (simp add: uints_num take_bit_eq_mod) |
|
1366 done |
|
1367 |
|
1368 interpretation word_uint: |
|
1369 td_ext |
|
1370 "uint::'a::len word \<Rightarrow> int" |
|
1371 word_of_int |
|
1372 "uints (LENGTH('a::len))" |
|
1373 "\<lambda>w. w mod 2 ^ LENGTH('a::len)" |
|
1374 by (fact td_ext_uint) |
|
1375 |
|
1376 lemmas td_uint = word_uint.td_thm |
|
1377 lemmas int_word_uint = word_uint.eq_norm |
|
1378 |
|
1379 lemma td_ext_ubin: |
|
1380 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
1381 (take_bit (LENGTH('a)))" |
|
1382 apply standard |
|
1383 apply transfer |
|
1384 apply simp |
|
1385 done |
|
1386 |
|
1387 interpretation word_ubin: |
|
1388 td_ext |
|
1389 "uint::'a::len word \<Rightarrow> int" |
|
1390 word_of_int |
|
1391 "uints (LENGTH('a::len))" |
|
1392 "take_bit (LENGTH('a::len))" |
|
1393 by (fact td_ext_ubin) |
|
1394 |
|
1395 lemma td_ext_unat [OF refl]: |
|
1396 "n = LENGTH('a::len) \<Longrightarrow> |
|
1397 td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" |
|
1398 apply (standard; transfer) |
|
1399 apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self) |
|
1400 apply (simp add: take_bit_eq_mod) |
|
1401 done |
|
1402 |
|
1403 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] |
|
1404 |
|
1405 interpretation word_unat: |
|
1406 td_ext |
|
1407 "unat::'a::len word \<Rightarrow> nat" |
|
1408 of_nat |
|
1409 "unats (LENGTH('a::len))" |
|
1410 "\<lambda>i. i mod 2 ^ LENGTH('a::len)" |
|
1411 by (rule td_ext_unat) |
|
1412 |
|
1413 lemmas td_unat = word_unat.td_thm |
|
1414 |
|
1415 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] |
|
1416 |
|
1417 lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))" |
|
1418 for z :: "'a::len word" |
|
1419 apply (unfold unats_def) |
|
1420 apply clarsimp |
|
1421 apply (rule xtrans, rule unat_lt2p, assumption) |
|
1422 done |
|
1423 |
|
1424 lemma td_ext_sbin: |
|
1425 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
1426 (signed_take_bit (LENGTH('a) - 1))" |
|
1427 apply (unfold td_ext_def' sint_uint) |
|
1428 apply (simp add : word_ubin.eq_norm) |
|
1429 apply (cases "LENGTH('a)") |
|
1430 apply (auto simp add : sints_def) |
|
1431 apply (rule sym [THEN trans]) |
|
1432 apply (rule word_ubin.Abs_norm) |
|
1433 apply (simp only: bintrunc_sbintrunc) |
|
1434 apply (drule sym) |
|
1435 apply simp |
|
1436 done |
|
1437 |
|
1438 lemma td_ext_sint: |
|
1439 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
1440 (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - |
|
1441 2 ^ (LENGTH('a) - 1))" |
|
1442 using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) |
|
1443 |
|
1444 text \<open> |
|
1445 We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version |
|
1446 and interpretations do not produce thm duplicates. I.e. |
|
1447 we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>, |
|
1448 because the latter is the same thm as the former. |
|
1449 \<close> |
|
1450 interpretation word_sint: |
|
1451 td_ext |
|
1452 "sint ::'a::len word \<Rightarrow> int" |
|
1453 word_of_int |
|
1454 "sints (LENGTH('a::len))" |
|
1455 "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) - |
|
1456 2 ^ (LENGTH('a::len) - 1)" |
|
1457 by (rule td_ext_sint) |
|
1458 |
|
1459 interpretation word_sbin: |
|
1460 td_ext |
|
1461 "sint ::'a::len word \<Rightarrow> int" |
|
1462 word_of_int |
|
1463 "sints (LENGTH('a::len))" |
|
1464 "signed_take_bit (LENGTH('a::len) - 1)" |
|
1465 by (rule td_ext_sbin) |
|
1466 |
|
1467 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm] |
|
1468 |
|
1469 lemmas td_sint = word_sint.td |
1476 |
1470 |
1477 |
1471 |
1478 subsection \<open>More shift operations\<close> |
1472 subsection \<open>More shift operations\<close> |
1479 |
1473 |
1480 lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> |
1474 lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> |