From b91e1d95fbe9b4328055897364518dc443c04882 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 20 Dec 2024 15:42:26 +1030 Subject: [PATCH] rt ainvs: remove set_map_fst_filter_zip from AInvs (now in Lib) Signed-off-by: Michael McInerney --- proof/invariant-abstract/IpcDet_AI.thy | 6 ------ 1 file changed, 6 deletions(-) diff --git a/proof/invariant-abstract/IpcDet_AI.thy b/proof/invariant-abstract/IpcDet_AI.thy index f09bfff78b..f07e8d56a6 100644 --- a/proof/invariant-abstract/IpcDet_AI.thy +++ b/proof/invariant-abstract/IpcDet_AI.thy @@ -369,12 +369,6 @@ lemma tcb_ep_append_valid_ep: \\q'. valid_ep (update_ep_queue ep q')\" by (cases ep) (wpsimp wp: tcb_ep_append_valid_SendEP tcb_ep_append_valid_RecvEP)+ -lemma set_map_fst_filter_zip: - "set (map fst (filter P (zip xs ys))) \ set xs" - apply (induct xs, simp) - apply (case_tac ys; simp) - by (metis (mono_tags, lifting) image_Collect_subsetI insertI2 set_zip_helper) - lemma tcb_ep_append_rv_wf: "\\\ tcb_ep_append t q \\rv s. set rv = set (t # q)\" apply (simp add: tcb_ep_append_def)