From 0aa2914b8453c680c1a783ce6296f6de3937e07b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 23 Jan 2023 18:36:22 +1100 Subject: [PATCH] lib/monads: move empty_fail_guard into NonDetMonadVCG So that it is available together with the other empty_fail lemmas. Eventually, these should go into their own theory. Signed-off-by: Gerwin Klein --- lib/Monad_Equations.thy | 3 --- lib/Monad_WP/NonDetMonadVCG.thy | 4 ++++ 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/Monad_Equations.thy b/lib/Monad_Equations.thy index 9a270ecf3..c4f0cc606 100644 --- a/lib/Monad_Equations.thy +++ b/lib/Monad_Equations.thy @@ -513,9 +513,6 @@ lemma bind_fail_propagates: "empty_fail A \ A >>= (\_. fail) = fail" by (monad_eq simp: empty_fail_def) fastforce -lemma empty_fail_guard [simp]: "empty_fail (state_assert G)" - by (clarsimp simp: state_assert_def assert_def empty_fail_def get_def return_def bind_def) - lemma simple_bind_fail [simp]: "(state_assert X >>= (\_. fail)) = fail" "(modify M >>= (\_. fail)) = fail" diff --git a/lib/Monad_WP/NonDetMonadVCG.thy b/lib/Monad_WP/NonDetMonadVCG.thy index 3722913b5..c7ba33458 100644 --- a/lib/Monad_WP/NonDetMonadVCG.thy +++ b/lib/Monad_WP/NonDetMonadVCG.thy @@ -872,6 +872,10 @@ lemma empty_fail_select[simp]: "empty_fail (select V) = (V \ {})" by (clarsimp simp: select_def empty_fail_def) +lemma empty_fail_guard[simp]: + "empty_fail (state_assert G)" + by (clarsimp simp: state_assert_def empty_fail_get empty_fail_assert) + lemma empty_fail_not_snd: "\ \ snd (m s); empty_fail m \ \ \v. v \ fst (m s)" by (fastforce simp: empty_fail_def)