From d275068826afa90a2354109c9f08412d4bd96818 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 11 Jan 2023 12:03:26 +1100 Subject: [PATCH] lib: move empty_fail lemmas up into NonDetMonadVCG This enables a few more moves of remaining lemmas in NonDetMonadLemmaBucket into the theories they belong thematically. Signed-off-by: Gerwin Klein --- lib/Monad_Commute.thy | 4 -- lib/Monad_Equations.thy | 34 +++++++++++ lib/Monad_WP/NonDetMonadVCG.thy | 50 ++++++++++++++++- lib/NonDetMonadLemmaBucket.thy | 99 ++------------------------------- 4 files changed, 86 insertions(+), 101 deletions(-) diff --git a/lib/Monad_Commute.thy b/lib/Monad_Commute.thy index e57b35a0f..f38b6f6aa 100644 --- a/lib/Monad_Commute.thy +++ b/lib/Monad_Commute.thy @@ -13,10 +13,6 @@ theory Monad_Commute More_Monad (* for mapM_x *) begin -lemma empty_fail_not_snd: - "\ \ snd (m s); empty_fail m \ \ \v. v \ fst (m s)" - by (fastforce simp: empty_fail_def) - definition monad_commute where "monad_commute P a b \ diff --git a/lib/Monad_Equations.thy b/lib/Monad_Equations.thy index 4c98432ea..9a270ecf3 100644 --- a/lib/Monad_Equations.thy +++ b/lib/Monad_Equations.thy @@ -523,4 +523,38 @@ lemma simple_bind_fail [simp]: "(gets X >>= (\_. fail)) = fail" by (auto intro!: bind_fail_propagates) +lemma bind_inv_inv_comm: + "\ \P. \P\ f \\_. P\; \P. \P\ g \\_. P\; + empty_fail f; empty_fail g \ \ + do x \ f; y \ g; n x y od = do y \ g; x \ f; n x y od" + apply (rule ext) + apply (rename_tac s) + apply (rule_tac s="(do (x, y) \ do x \ f; y \ (\_. g s) ; (\_. return (x, y) s) od; + n x y od) s" in trans) + apply (simp add: bind_assoc) + apply (intro bind_apply_cong, simp_all)[1] + apply (metis in_inv_by_hoareD) + apply (simp add: return_def bind_def) + apply (metis in_inv_by_hoareD) + apply (rule_tac s="(do (x, y) \ do y \ g; x \ (\_. f s) ; (\_. return (x, y) s) od; + n x y od) s" in trans[rotated]) + apply (simp add: bind_assoc) + apply (intro bind_apply_cong, simp_all)[1] + apply (metis in_inv_by_hoareD) + apply (simp add: return_def bind_def) + apply (metis in_inv_by_hoareD) + apply (rule bind_apply_cong, simp_all) + apply (clarsimp simp: bind_def split_def return_def) + apply (auto | drule(1) empty_failD3)+ + done + +lemma bind_known_operation_eq: + "\ no_fail P f; \Q\ f \\rv s. rv = x \ s = t\; P s; Q s; empty_fail f \ + \ (f >>= g) s = g x t" + apply (drule(1) no_failD) + apply (subgoal_tac "fst (f s) = {(x, t)}") + apply (clarsimp simp: bind_def) + apply (fastforce simp: valid_def empty_fail_def) + done + end \ No newline at end of file diff --git a/lib/Monad_WP/NonDetMonadVCG.thy b/lib/Monad_WP/NonDetMonadVCG.thy index 364058f3f..ad11e3929 100644 --- a/lib/Monad_WP/NonDetMonadVCG.thy +++ b/lib/Monad_WP/NonDetMonadVCG.thy @@ -12,6 +12,11 @@ imports Strengthen begin +(* FIXME lib: split this theory into at least: Hoare logic things, Det, EmptyFail, NoFail *) +(* FIXME lib: put definitions of det, empty_fail, no_fail, into Det, EmptyFail, NoFail *) +(* FIXME lib: move Hoare logic stuff from NonDetMonadLemmas to here *) +(* FIXME lib: move monad equalities from here to NonDetMonadLemmas *) + section "Satisfiability" text \ @@ -796,8 +801,7 @@ lemma empty_fail_return [simp, wp]: by (simp add: empty_fail_def return_def) lemma empty_fail_bindE: - "\ empty_fail f; \rv. empty_fail (g rv) \ - \ empty_fail (f >>=E g)" + "\ empty_fail f; \rv. empty_fail (g rv) \ \ empty_fail (f >>=E g)" apply (simp add: bindE_def) apply (erule empty_fail_bind) apply (simp add: lift_def throwError_def split: sum.split) @@ -825,6 +829,10 @@ lemma empty_fail [simp]: "empty_fail fail" by (simp add: fail_def empty_fail_def) +lemma empty_fail_assert: + "empty_fail (assert P)" + unfolding assert_def by simp + lemma empty_fail_assert_opt [simp]: "empty_fail (assert_opt x)" by (simp add: assert_opt_def split: option.splits) @@ -837,6 +845,44 @@ lemma empty_fail_gets_map[simp]: "empty_fail (gets_map f p)" unfolding gets_map_def by simp +lemma empty_fail_error_bits[simp]: + "empty_fail (returnOk v)" + "empty_fail (throwError v)" + "empty_fail (liftE f) = empty_fail f" + by (fastforce simp: returnOk_def throwError_def liftE_def empty_fail_def bind_def return_def)+ + +lemma empty_fail_whenEs: + "empty_fail f \ empty_fail (whenE P f)" + "empty_fail f \ empty_fail (unlessE P f)" + by (auto simp add: whenE_def unlessE_def) + +lemma empty_fail_assertE: + "empty_fail (assertE P)" + by (simp add: assertE_def split: if_split) + +lemma empty_fail_get: + "empty_fail get" + by (simp add: empty_fail_def get_def) + +lemma empty_fail_catch: + "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catch f g)" + by (simp add: catch_def split: sum.split) + +lemma empty_fail_select[simp]: + "empty_fail (select V) = (V \ {})" + by (clarsimp simp: select_def empty_fail_def) + +lemma empty_fail_not_snd: + "\ \ snd (m s); empty_fail m \ \ \v. v \ fst (m s)" + by (fastforce simp: empty_fail_def) + +lemmas empty_failD2 = empty_fail_not_snd[rotated] + +lemma empty_failD3: + "\ empty_fail f; \ snd (f s) \ \ fst (f s) \ {}" + by (drule(1) empty_failD2, clarsimp) + + subsection "Failure" lemma fail_wp: "\\x. True\ fail \Q\" diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 383d15e3d..9daa175ce 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -98,18 +98,6 @@ lemma mapME_x_inv_wp: apply assumption done - -lemma empty_fail_error_bits: - "empty_fail (returnOk v)" - "empty_fail (throwError v)" - "empty_fail (liftE f) = empty_fail f" - apply (simp_all add: returnOk_def throwError_def) - apply (rule iffI, simp_all add: liftE_def) - apply (simp add: empty_fail_def bind_def return_def) - apply (erule allEI) - apply clarsimp - done - lemma mapM_upd: assumes "\x rv s s'. (rv,s') \ fst (f x s) \ x \ set xs \ (rv, g s') \ fst (f x (g s))" shows "(rv,s') \ fst (mapM f xs s) \ (rv, g s') \ fst (mapM f xs (g s))" @@ -130,15 +118,6 @@ next done qed -lemma empty_fail_whenEs: - "empty_fail f \ empty_fail (whenE P f)" - "empty_fail f \ empty_fail (unlessE P f)" - by (auto simp add: whenE_def unlessE_def empty_fail_error_bits split: if_split) - -lemma empty_fail_assertE: - "empty_fail (assertE P)" - by (simp add: assertE_def empty_fail_error_bits split: if_split) - lemma gets_the_validE_R_wp: "\\s. f s \ None \ isRight (the (f s)) \ Q (theRight (the (f s))) s\ gets_the f @@ -173,45 +152,12 @@ lemma list_case_return: (* FIXME lib: move to Lib *) = return (case xs of [] \ v | y # ys \ f y ys)" by (simp split: list.split) +lemma lifted_if_collapse: (* FIXME lib: move to Lib *) + "(if P then \ else f) = (\s. \P \ f s)" + by auto + lemmas list_case_return2 = list_case_return (* FIXME lib: eliminate *) -lemma empty_fail_get: - "empty_fail get" - by (simp add: empty_fail_def get_def) - -lemma empty_failD2: - "\ empty_fail f; \ snd (f s) \ \ \v. v \ fst (f s)" - by (fastforce simp add: empty_fail_def) - -lemma empty_failD3: - "\ empty_fail f; \ snd (f s) \ \ fst (f s) \ {}" - by (drule(1) empty_failD2, clarsimp) - -lemma bind_inv_inv_comm: - "\ \P. \P\ f \\_. P\; \P. \P\ g \\_. P\; - empty_fail f; empty_fail g \ \ - do x \ f; y \ g; n x y od = do y \ g; x \ f; n x y od" - apply (rule ext) - apply (rename_tac s) - apply (rule_tac s="(do (x, y) \ do x \ f; y \ (\_. g s) ; (\_. return (x, y) s) od; - n x y od) s" in trans) - apply (simp add: bind_assoc) - apply (intro bind_apply_cong, simp_all)[1] - apply (metis in_inv_by_hoareD) - apply (simp add: return_def bind_def) - apply (metis in_inv_by_hoareD) - apply (rule_tac s="(do (x, y) \ do y \ g; x \ (\_. f s) ; (\_. return (x, y) s) od; - n x y od) s" in trans[rotated]) - apply (simp add: bind_assoc) - apply (intro bind_apply_cong, simp_all)[1] - apply (metis in_inv_by_hoareD) - apply (simp add: return_def bind_def) - apply (metis in_inv_by_hoareD) - apply (rule bind_apply_cong, simp_all) - apply (clarsimp simp: bind_def split_def return_def) - apply (auto | drule(1) empty_failD3)+ - done - lemma no_fail_mapM: "\x. no_fail \ (f x) \ no_fail \ (mapM f xs)" apply (induct xs) @@ -220,11 +166,6 @@ lemma no_fail_mapM: apply (wp|fastforce)+ done - -lemma lifted_if_collapse: (* FIXME lib: move to Lib *) - "(if P then \ else f) = (\s. \P \ f s)" - by auto - lemma filterM_preserved: "\ \x. x \ set xs \ \P\ m x \\rv. P\ \ \ \P\ filterM m xs \\rv. P\" @@ -314,10 +255,6 @@ lemma mapM_x_wp: shows "set xs \ S \ \P\ mapM_x f xs \\rv. P\" by (subst mapM_x_mapM) (wp mapM_wp x) - -lemma empty_fail_assert : "empty_fail (assert P)" - unfolding assert_def by simp - lemma no_fail_mapM': assumes rl: "\x. no_fail (\_. P x) (f x)" shows "no_fail (\_. \x \ set xs. P x) (mapM f xs)" @@ -361,19 +298,6 @@ lemma empty_fail_sequence_x : shows "empty_fail (sequence_x ms)" using assms by (induct ms) (auto simp: sequence_x_def) -lemma bind_known_operation_eq: - "\ no_fail P f; \Q\ f \\rv s. rv = x \ s = t\; P s; Q s; empty_fail f \ - \ (f >>= g) s = g x t" - apply (drule(1) no_failD) - apply (subgoal_tac "fst (f s) = {(x, t)}") - apply (clarsimp simp: bind_def) - apply (rule not_psubset_eq) - apply (drule(1) empty_failD2, clarsimp) - apply fastforce - apply clarsimp - apply (drule(1) use_valid, simp+) - done - lemma mapME_set: assumes est: "\x. \R\ f x \P\, -" and invp: "\x y. \R and P x\ f y \\_. P x\, -" @@ -415,13 +339,6 @@ lemma empty_fail_mapM_x [simp]: apply (clarsimp simp: mapM_x_Cons) done -lemma empty_fail_catch: - "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catch f g)" - apply (simp add: catch_def) - apply (erule empty_fail_bind) - apply (simp split: sum.split) - done - lemma valid_isRight_theRight_split: "\P\ f \\rv s. Q True rv s\,\\e s. \v. Q False v s\ \ \P\ f \\rv s. Q (isRight rv) (theRight rv) s\" @@ -470,12 +387,4 @@ lemma case_option_find_give_me_a_map: apply (simp add: lift_def throwError_def returnOk_def split: sum.split) done -lemma empty_fail_select [simp]: "empty_fail (select V) = (V \ {})" - apply (clarsimp simp: select_def empty_fail_def) - done - -lemma empty_fail_liftE [simp]: - "empty_fail (liftE X) = empty_fail X" - by (rule empty_fail_error_bits) - end