From 27d838af862f771b700f43ee245b3b4239dce1fe Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Sun, 26 Mar 2023 16:50:56 +1030 Subject: [PATCH] lib+proof: rename bind_assoc_reverse to bind_assoc_return_reverse This also improves the style of this lemma Signed-off-by: Michael McInerney --- lib/Monads/Monad_Equations.thy | 14 +++++++++++--- lib/clib/Corres_UL_C.thy | 2 +- proof/refine/ARM/Retype_R.thy | 2 +- proof/refine/ARM_HYP/Retype_R.thy | 2 +- proof/refine/RISCV64/Retype_R.thy | 2 +- proof/refine/X64/Retype_R.thy | 2 +- 6 files changed, 16 insertions(+), 8 deletions(-) diff --git a/lib/Monads/Monad_Equations.thy b/lib/Monads/Monad_Equations.thy index 3595718f7..a2ce88969 100644 --- a/lib/Monads/Monad_Equations.thy +++ b/lib/Monads/Monad_Equations.thy @@ -388,9 +388,17 @@ lemma bind_assoc2: "(do x \ a; _ \ b; c x od) = (do x \ (do x' \ a; _ \ b; return x' od); c x od)" by (simp add: bind_assoc) -lemma bind_assoc_reverse: - "(do x \ A; _ \ B x; C x od) = - (do x \ do x \ A; _ \ B x; return x od; C x od)" +lemma bind_assoc_return_reverse: + "do x \ f; + _ \ g x; + h x + od = + do x \ do x \ f; + _ \ g x; + return x + od; + h x + od" by (simp only: bind_assoc return_bind) lemma if_bind: diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 21fea52e1..a8ab1afb8 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -827,7 +827,7 @@ text \ state. The extra return statement on the Haskell side allows us to establish a nontrivial return relation - between the values set on the concrete and abstract side. The @{thm bind_assoc_reverse} rule + between the values set on the concrete and abstract side. The @{thm bind_assoc_return_reverse} rule may assist with rewriting statements to add the extra return needed by this rule\ lemma ccorres_call_getter_setter: assumes cul: "ccorresG sr \ (=) xf' P (i ` P') [] getter (Call f)" diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy index a996d3a28..b7fdfee02 100644 --- a/proof/refine/ARM/Retype_R.thy +++ b/proof/refine/ARM/Retype_R.thy @@ -5329,7 +5329,7 @@ lemma corres_retype_region_createNewCaps: \ \CapTable\ apply (subst retype_region2_extra_ext_trivial) apply (simp add: APIType_map2_def) - apply (subst bind_assoc_reverse[of "createObjects y n (KOCTE makeObject) us"]) + apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) apply (subst liftM_def [of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) apply simp diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index 83e1c0eeb..0d14a725e 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -5381,7 +5381,7 @@ lemma corres_retype_region_createNewCaps: \ \CapTable\ apply (subst retype_region2_extra_ext_trivial) apply (simp add: APIType_map2_def) - apply (subst bind_assoc_reverse[of "createObjects y n (KOCTE makeObject) us"]) + apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) apply (subst liftM_def [of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) apply simp diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy index 84722a58e..b6a18523b 100644 --- a/proof/refine/RISCV64/Retype_R.thy +++ b/proof/refine/RISCV64/Retype_R.thy @@ -5162,7 +5162,7 @@ lemma corres_retype_region_createNewCaps: \ \CapTable\ apply (subst retype_region2_extra_ext_trivial) apply (simp add: APIType_map2_def) - apply (subst bind_assoc_reverse[of "createObjects y n (KOCTE makeObject) us"]) + apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) apply (subst liftM_def[of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) apply simp apply (rule corres_rel_imp) diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index 7ca3e8441..c4c141120 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -5436,7 +5436,7 @@ lemma corres_retype_region_createNewCaps: \ \CapTable\ apply (subst retype_region2_extra_ext_trivial) apply (simp add: APIType_map2_def) - apply (subst bind_assoc_reverse[of "createObjects y n (KOCTE makeObject) us"]) + apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) apply (subst liftM_def[of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) apply simp apply (rule corres_rel_imp)