From b00cbb16436ad6dfc6c872dc6e3996f7dfd22c65 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Wed, 11 Dec 2024 15:22:05 +1100 Subject: [PATCH] aarch64 refine: [squash] fix tcb_cte_cases_neqs_n duplication warning Signed-off-by: Rafal Kolanski --- proof/refine/Invariants_H.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/proof/refine/Invariants_H.thy b/proof/refine/Invariants_H.thy index a604745dd2..2b65be43b4 100644 --- a/proof/refine/Invariants_H.thy +++ b/proof/refine/Invariants_H.thy @@ -1507,8 +1507,10 @@ lemma (in Arch) tcb_cte_cases_distinct_n: requalify_facts Arch.tcb_cte_cases_distinct_n lemmas tcb_cte_cases_neqs_n = - tcb_cte_cases_distinct_n[simplified] - distinct_rev[THEN iffD2, OF tcb_cte_cases_distinct_n, simplified] + conjI[OF + tcb_cte_cases_distinct_n[simplified] + distinct_rev[THEN iffD2, OF tcb_cte_cases_distinct_n, simplified], + simplified conj_ac, simplified] (* remove duplicates from 0/1 simplification *) lemma tcb_cte_cases_simps[simp]: "tcb_cte_cases 0 = Some (tcbCTable, tcbCTable_update)" @@ -1516,7 +1518,6 @@ lemma tcb_cte_cases_simps[simp]: "tcb_cte_cases (2 << cteSizeBits) = Some (tcbReply, tcbReply_update)" "tcb_cte_cases (3 << cteSizeBits) = Some (tcbCaller, tcbCaller_update)" "tcb_cte_cases (4 << cteSizeBits) = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)" - (* FIXME arch-split: warning due to tcb_cte_cases_neqs overlapping *) by (simp add: tcb_cte_cases_neqs_n tcb_cte_cases_def)+ lemmas tcbSlot_defs = tcbCTableSlot_def tcbVTableSlot_def tcbReplySlot_def tcbCallerSlot_def @@ -1529,7 +1530,6 @@ lemma tcb_cte_cases_distinct: tcbReplySlot << cteSizeBits, tcbCallerSlot << cteSizeBits, tcbIPCBufferSlot << cteSizeBits]" - (* FIXME arch-split: warning due to tcb_cte_cases_neqs overlapping *) by (simp add: tcbSlot_defs tcb_cte_cases_neqs_n) lemmas tcb_cte_cases_neqs =