x64 crefine: remove unused lemmas

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Oct 24, 2024 · f8016c1 · f8016c1
1 parent ef5b608
commit f8016c1
Showing 1 changed file with 0 additions and 15 deletions.
diff --git 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 \<Longrightarrow> (pde_get_tag pde = scast pde_pde_pt \<and> pde_pde_pt_CL.present_CL (pde_pde_pt_lift pde) = 0) = isInvalidPDE pdea"
   apply (simp add: cpde_relation_def Let_def)