1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Word_Lemmas_64_Internal
8imports Word_Lemmas_64
9begin
10
11lemmas unat_add_simple = iffD1[OF unat_add_lem[where 'a = 64, folded word_bits_def]]
12
13lemma unat_length_4_helper:
14  "\<lbrakk>unat (l::machine_word) = length args; \<not> l < 4\<rbrakk> \<Longrightarrow> \<exists>x xa xb xc xs. args = x#xa#xb#xc#xs"
15  apply (case_tac args; clarsimp simp: unat_eq_0)
16  by (rename_tac list, case_tac list, clarsimp, unat_arith)+
17
18lemma ucast_drop_big_mask:
19  "UCAST(64 \<rightarrow> 16) (x && 0xFFFF) = UCAST(64 \<rightarrow> 16) x"
20  by word_bitwise
21
22lemma first_port_last_port_compare:
23  "UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (xa && 0xFFFF))
24        <s UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (x && 0xFFFF))
25       = (UCAST(64 \<rightarrow> 16) xa < UCAST(64 \<rightarrow> 16) x)"
26  apply (clarsimp simp: word_sless_alt ucast_drop_big_mask)
27  apply (subst sint_ucast_eq_uint, clarsimp simp: is_down)+
28  by (simp add: word_less_alt)
29
30lemma machine_word_and_3F_less_40:
31  "(w :: machine_word) && 0x3F < 0x40"
32  by (rule word_and_less', simp)
33
34(* FIXME: move to GenericLib *)
35lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]
36
37lemma unat_mask_3_less_8:
38  "unat (p && mask 3 :: word64) < 8"
39  apply (rule unat_less_helper)
40  apply (rule order_le_less_trans, rule word_and_le1)
41  apply (simp add: mask_def)
42  done
43
44lemma scast_specific_plus64:
45  "scast (of_nat (word_ctz x) + 0x20 :: 64 signed word) = of_nat (word_ctz x) + (0x20 :: machine_word)"
46  by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
47
48lemma scast_specific_plus64_signed:
49  "scast (of_nat (word_ctz x) + 0x20 :: machine_word) = of_nat (word_ctz x) + (0x20 :: 64 signed word)"
50  by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
51
52lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def]
53                          mask_len_id[where 'a=64, simplified]
54
55lemma neq_0_unat: "x \<noteq> 0 \<Longrightarrow> 0 < unat x" for x::machine_word
56  by (simp add: unat_gt_0)
57
58end