From f00bbb735f3aa0355538418ced44c89e0e65774b Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 9 Jul 2024 12:35:37 +1000 Subject: [PATCH] lib/monads: resync trace monad with nondet Signed-off-by: Corey Lewis --- lib/Monads/nondet/Nondet_Reader_Option.thy | 12 ++++++------ lib/Monads/nondet/Nondet_VCG.thy | 4 ++-- lib/Monads/trace/Trace_More_RG.thy | 14 ++++++++++++++ lib/Monads/trace/Trace_RG.thy | 16 ++++++++++++++++ lib/Monads/trace/Trace_Reader_Option.thy | 19 ++++++++++++++----- lib/Monads/trace/Trace_VCG.thy | 4 ++-- 6 files changed, 54 insertions(+), 15 deletions(-) diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy index 7e5b471f12..297fae9382 100644 --- a/lib/Monads/nondet/Nondet_Reader_Option.thy +++ b/lib/Monads/nondet/Nondet_Reader_Option.thy @@ -70,7 +70,11 @@ lemma gets_the_obind: "gets_the (f |>> g) = gets_the f >>= (\x. gets_the (g x))" by (rule ext) (simp add: monad_simps obind_def split: option.splits) -lemma gets_the_Some_get[simp]: +lemma gets_the_Some_return: + "gets_the (\_. Some x) = return x" + by (simp add: gets_the_def assert_opt_Some) + +lemma gets_the_Some_get: "gets_the Some = get" by (clarsimp simp: gets_the_def gets_def assert_opt_Some) @@ -115,10 +119,6 @@ lemma gets_the_oapply_comp: "gets_the (oapply x \ f) = gets_map f x" by (fastforce simp: gets_map_def gets_the_def o_def gets_def) -lemma gets_the_Some: - "gets_the (\_. Some x) = return x" - by (simp add: gets_the_def assert_opt_Some) - lemma gets_the_oapply2_comp: "gets_the (oapply2 y x \ f) = gets_map (swp f y) x" by (clarsimp simp: gets_map_def gets_the_def o_def gets_def) @@ -136,7 +136,7 @@ lemma fst_assert_opt: lemmas omonad_simps [simp] = gets_the_opt_map assert_opt_Some gets_the_obind gets_the_return gets_the_fail gets_the_returnOk - gets_the_throwError gets_the_assert gets_the_Some + gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get gets_the_oapply_comp diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy index 9e0a7199d7..1ebd4a18f2 100644 --- a/lib/Monads/nondet/Nondet_VCG.thy +++ b/lib/Monads/nondet/Nondet_VCG.thy @@ -227,11 +227,11 @@ lemma return_inv[iff]: lemma hoare_modifyE_var: "\ \s. P s \ Q (f s) \ \ \P\ modify f \\_ s. Q s\" - by(simp add: valid_def modify_def put_def get_def bind_def) + by (simp add: valid_def modify_def put_def get_def bind_def) lemma hoare_if: "\ P' \ \P\ f \Q\; \ P' \ \P\ g \Q\ \ \ \P\ if P' then f else g \Q\" - by (simp add: valid_def) + by simp lemma hoare_pre_subst: "\ P = P'; \P\ f \Q\ \ \ \P'\ f \Q\" diff --git a/lib/Monads/trace/Trace_More_RG.thy b/lib/Monads/trace/Trace_More_RG.thy index d75e92433e..1a8a3c4074 100644 --- a/lib/Monads/trace/Trace_More_RG.thy +++ b/lib/Monads/trace/Trace_More_RG.thy @@ -138,6 +138,20 @@ lemma assertE_tsp: "\P\,\R\ assertE Q \G\,\\rv s0 s. Q \ P s0 s\,\E\" by (wpsimp wp: assertE_wp) +lemma select_inv_rg: + "\P\,\R\ select S \G\,\\_. P\" + by wpsimp + +lemma assert_inv_rg: + "\P\,\R\ assert Q \G\,\\_. P\" + unfolding assert_def + by (cases Q) wpsimp+ + +lemma assert_opt_inv_rg: + "\P\,\R\ assert_opt Q \G\,\\_. P\" + unfolding assert_opt_def + by (cases Q) (wp | simp)+ + lemma case_options_weak_twp: "\ \P\,\R\ f \G\,\Q\; \x. \P'\,\R\ g x \G\,\Q\ \ \ \P and P'\,\R\ case opt of None \ f | Some x \ g x \G\,\Q\" diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy index 42889d9236..aedda7f671 100644 --- a/lib/Monads/trace/Trace_RG.thy +++ b/lib/Monads/trace/Trace_RG.thy @@ -362,6 +362,22 @@ lemma rg_FalseE[simp]: "\\\\,\R\ f \G\,\Q\,\E\ = prefix_closed f" by (simp add: validI_def validIE_def) +lemma rg_modifyE_var: + "\ \s0 s. P s0 s \ Q s0 (f s) \ \ \P\,\R\ modify f \G\,\\_. Q\" + by (simp add: validI_def modify_def put_def get_def bind_def prefix_closed_def rely_def) + +lemma rg_if: + "\ P' \ \P\,\R\ f \G\,\Q\; \ P' \ \P\,\R\ g \G\,\Q\ \ \ \P\,\R\ if P' then f else g \G\,\Q\" + by simp + +lemma rg_pre_subst: + "\ P = P'; \P\,\R\ f \G\,\Q\ \ \ \P'\,\R\ f \G\,\Q\" + by (erule subst) + +lemma rg_post_subst: + "\ Q = Q'; \P\,\R\ f \G\,\Q\ \ \ \P\,\R\ f \G\,\Q'\" + by (erule subst) + lemma rg_post_imp: "\\v s0 s. Q' v s0 s \ Q v s0 s; \P\,\R\ f \G\,\Q'\\ \ \P\,\R\ f \G\,\Q\" by (simp add: validI_def) diff --git a/lib/Monads/trace/Trace_Reader_Option.thy b/lib/Monads/trace/Trace_Reader_Option.thy index 27f59281d0..b493ce65fc 100644 --- a/lib/Monads/trace/Trace_Reader_Option.thy +++ b/lib/Monads/trace/Trace_Reader_Option.thy @@ -70,6 +70,14 @@ lemma gets_the_obind: "gets_the (f |>> g) = gets_the f >>= (\x. gets_the (g x))" by (rule ext) (simp add: monad_simps obind_def split: option.splits) +lemma gets_the_Some_return: + "gets_the (\_. Some x) = return x" + by (simp add: gets_the_def assert_opt_Some) + +lemma gets_the_Some_get: + "gets_the Some = get" + by (clarsimp simp: gets_the_def gets_def assert_opt_Some) + lemma gets_the_return: "gets_the (oreturn x) = return x" by (simp add: monad_simps oreturn_def) @@ -94,6 +102,11 @@ lemma gets_the_assert: "gets_the (oassert P) = assert P" by (simp add: oassert_def assert_def gets_the_fail gets_the_return) +lemma gets_the_ostate_assert: + "gets_the (ostate_assert P) = state_assert P" + by (clarsimp simp: ostate_assert_def state_assert_def gets_the_obind gets_the_Some_get + gets_the_assert) + lemma gets_the_assert_opt: "gets_the (oassert_opt P) = assert_opt P" by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits) @@ -106,10 +119,6 @@ lemma gets_the_oapply_comp: "gets_the (oapply x \ f) = gets_map f x" by (fastforce simp: gets_map_def gets_the_def o_def gets_def) -lemma gets_the_Some: - "gets_the (\_. Some x) = return x" - by (simp add: gets_the_def assert_opt_Some) - lemma gets_the_oapply2_comp: "gets_the (oapply2 y x \ f) = gets_map (swp f y) x" by (clarsimp simp: gets_map_def gets_the_def o_def gets_def) @@ -127,7 +136,7 @@ lemma mres_assert_opt: lemmas omonad_simps [simp] = gets_the_opt_map assert_opt_Some gets_the_obind gets_the_return gets_the_fail gets_the_returnOk - gets_the_throwError gets_the_assert gets_the_Some + gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get gets_the_oapply_comp diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index 4b8170b5d3..268cca5e68 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -223,11 +223,11 @@ lemma return_inv[iff]: lemma hoare_modifyE_var: "\ \s. P s \ Q (f s) \ \ \P\ modify f \\_ s. Q s\" - by(simp add: valid_def modify_def put_def get_def bind_def mres_def) + by (simp add: valid_def modify_def put_def get_def bind_def mres_def) lemma hoare_if: "\ P' \ \P\ f \Q\; \ P' \ \P\ g \Q\ \ \ \P\ if P' then f else g \Q\" - by (simp add: valid_def) + by simp lemma hoare_pre_subst: "\ P = P'; \P\ f \Q\ \ \ \P'\ f \Q\"