From 75db914627b4ff1ee66bb4aed388c9825d1e4e76 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 28 Mar 2023 12:31:34 +1100 Subject: [PATCH] word_lib: new lemmas about mask, AND, and shift Signed-off-by: Corey Lewis --- lib/Word_Lib/Word_Lemmas_Internal.thy | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 7fd871067..80257e586 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -1,4 +1,5 @@ (* + * Copyright 2023, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause @@ -718,4 +719,23 @@ lemma mask_alignment_ugliness: apply (meson linorder_not_le) by (auto simp: le_def) +lemma word_and_mask_shift_eq_0: + "n \ m \ x && mask n >> m = 0" + by word_eqI + +lemma word_mask_and_neg_shift_eq_0: + "n < m \ - (1 << m) && mask n = 0" + by (metis NOT_mask_AND_mask add.inverse_neutral leD less_imp_le mask_AND_NOT_mask mask_eqs(10) + shiftl_1 t2n_mask_eq_if) + +lemma aligned_mask_plus_bounded: + "\ is_aligned x m; m < n; n < LENGTH('a) \ \ (x && mask n) + 2^m \ 2^n" for x :: "'a::len word" + by (metis add_mask_fold and_mask_less' is_aligned_add_step_le is_aligned_after_mask is_aligned_mask + leD leI order_less_imp_le t2n_mask_eq_if word_less_sub_1) + +lemma aligned_mask_le_mask_minus: + "\ is_aligned x m; m \ n; n < LENGTH('a)\ \ x && mask n \ mask n - mask m" for x :: "'a::len word" + by (metis and_mask_less' is_aligned_after_mask is_aligned_neg_mask_eq' + mask_2pm1 mask_sub neg_mask_mono_le word_less_sub_le) + end