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