From f8016c1403d4a75ccf31111358c567f9d30c9278 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 23 Oct 2024 11:42:48 +1100 Subject: [PATCH] x64 crefine: remove unused lemmas Signed-off-by: Gerwin Klein --- proof/crefine/X64/Arch_C.thy | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy index a1ea859c37..ad07f5ffad 100644 --- a/proof/crefine/X64/Arch_C.thy +++ b/proof/crefine/X64/Arch_C.thy @@ -1468,21 +1468,6 @@ lemma obj_at_pte_aligned: elim!: is_aligned_weaken) done -(* FIXME x64: dont know what these are for yet *) -lemma addrFromPPtr_mask_5: - "addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)" - apply (simp add:addrFromPPtr_def X64.pptrBase_def) - apply word_bitwise - apply (simp add:mask_def) - done - -lemma addrFromPPtr_mask_6: - "addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)" - apply (simp add:addrFromPPtr_def X64.pptrBase_def) - apply word_bitwise - apply (simp add:mask_def) - done - lemma cpde_relation_invalid: "cpde_relation pdea pde \ (pde_get_tag pde = scast pde_pde_pt \ pde_pde_pt_CL.present_CL (pde_pde_pt_lift pde) = 0) = isInvalidPDE pdea" apply (simp add: cpde_relation_def Let_def)