From a30419f81debea0a574c65c52c01053ada7736c5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 11 Jul 2024 15:06:33 +1000 Subject: [PATCH] arm-hyp crefine: reduce diff to arm crefine Use the same proof text for both architectures to increase likelihood that patches will apply to both. Signed-off-by: Gerwin Klein --- proof/crefine/ARM_HYP/Refine_C.thy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index d54fc1d452..1c73871530 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -274,7 +274,7 @@ lemma handleSyscall_ccorres: apply (subst ccorres_seq_skip'[symmetric]) apply (rule ccorres_split_nothrow_novcg) apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified]) @@ -303,7 +303,7 @@ lemma handleSyscall_ccorres: apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_Guard)? apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified]) @@ -331,7 +331,7 @@ lemma handleSyscall_ccorres: apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_Guard)? apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])