From 0ca0a8e408446b982febbf94fa04574d1f9e00df Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Sat, 24 Feb 2024 12:51:08 +1100 Subject: [PATCH] lib/monads/trace: add connection to reader option Signed-off-by: Corey Lewis --- lib/Monads/ROOT | 1 + lib/Monads/trace/Trace_Monad.thy | 4 +- lib/Monads/trace/Trace_Reader_Option.thy | 220 +++++++++++++++++++++++ 3 files changed, 223 insertions(+), 2 deletions(-) create mode 100644 lib/Monads/trace/Trace_Reader_Option.thy diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index 6a54998f39..733bc3f127 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -53,6 +53,7 @@ session Monads (lib) = HOL + Trace_In_Monad Trace_More_VCG Trace_No_Fail + Trace_Reader_Option Trace_Sat Strengthen Nondet_Strengthen_Setup diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index eca5898a8f..9125a8441d 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -694,8 +694,8 @@ inductive_set whileLoop_results :: "\ \ C r s \ \ ((r, s), ([], Result (r, s))) \ whileLoop_results C B" | "\ C r s; (ts, Failed) \ B r s \ \ ((r, s), (ts, Failed)) \ whileLoop_results C B" | "\ C r s; (ts, Incomplete) \ B r s \ \ ((r, s), (ts, Incomplete)) \ whileLoop_results C B" - | "\ C r s; (ts, Result (r', s')) \ B r s; ((r', s'), (ts',z)) \ whileLoop_results C B \ - \ ((r, s), (ts'@ts,z)) \ whileLoop_results C B" + | "\ C r s; (ts, Result (r', s')) \ B r s; ((r', s'), (ts',z)) \ whileLoop_results C B; ts''=ts'@ts \ + \ ((r, s), (ts'',z)) \ whileLoop_results C B" \ \FIXME: there are fewer lemmas here than in NonDetMonad and I don't understand this well enough to know whether this is correct or not.\ diff --git a/lib/Monads/trace/Trace_Reader_Option.thy b/lib/Monads/trace/Trace_Reader_Option.thy new file mode 100644 index 0000000000..d822656a8b --- /dev/null +++ b/lib/Monads/trace/Trace_Reader_Option.thy @@ -0,0 +1,220 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Reader option monad syntax plus the connection between the reader option monad and the trace monad *) + +theory Trace_Reader_Option +imports + Trace_No_Fail + Reader_Option_VCG +begin + +(* FIXME: remove this syntax, standardise on do {..} instead *) +(* Syntax defined here so we can reuse Trace_Monad definitions *) +syntax + "_doO" :: "[dobinds, 'a] => 'a" ("(DO (_);// (_)//OD)" 100) + +translations + "_doO (_dobinds b bs) e" == "_doO b (_doO bs e)" + "_doO (_nobind b) e" == "b |>> (CONST K_bind e)" + "DO x <- a; e OD" == "a |>> (\x. e)" + + +lemma ovalid_K_bind_wp[wp]: + "ovalid P f Q \ ovalid P (K_bind f x) Q" + by simp + +lemma ovalidNF_K_bind_wp[wp]: + "ovalidNF P f Q \ ovalidNF P (K_bind f x) Q" + by simp + +lemma no_ofail_K_bind[wp]: + "no_ofail P f \ no_ofail P (K_bind f x)" + by simp + +lemma no_ofail_gets_the_eq: + "no_ofail P f \ no_fail P (gets_the (f :: ('s, 'a) lookup))" + by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def + get_def assert_opt_def bind_def return_def fail_def + split: option.split) + +lemmas no_ofail_gets_the = + no_ofail_gets_the_eq[THEN iffD1] + + +(* Lemmas relating ovalid and valid *) +lemma ovalid_gets_the: + "ovalid P f Q \ \P\ gets_the f \Q\" + apply wpsimp + apply (fastforce dest: use_ovalid) + done + + +lemmas monad_simps = + gets_the_def bind_def assert_def assert_opt_def + simpler_gets_def fail_def return_def + +lemma gets_the_opt_map: + "gets_the (f |> g) = do x \ gets_the f; assert_opt (g x) od" + by (rule ext) (simp add: monad_simps opt_map_def split: option.splits) + +lemma gets_the_opt_o: + "gets_the (f |> Some o g) = do x \ gets_the f; return (g x) od" + by (simp add: gets_the_opt_map assert_opt_Some) + +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_return: + "gets_the (oreturn x) = return x" + by (simp add: monad_simps oreturn_def) + +lemma gets_the_fail: + "gets_the ofail = fail" + by (simp add: monad_simps ofail_def) + +lemma gets_the_ogets: + "gets_the (ogets s) = gets s" + by (clarsimp simp: monad_simps ogets_def) + +lemma gets_the_returnOk: + "gets_the (oreturnOk x) = returnOk x" + by (simp add: monad_simps oreturnOk_def returnOk_def) + +lemma gets_the_throwError: + "gets_the (othrow e) = throwError e" + by (simp add: monad_simps othrow_def throwError_def) + +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_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) + +lemma gets_the_if_distrib: + "gets_the (if P then f else g) = (if P then gets_the f else gets_the g)" + by simp + +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) + +lemma gets_obind_bind_eq: + "(gets (f |>> (\x. g x))) = + (gets f >>= (\x. case x of None \ return None | Some y \ gets (g y)))" + by (auto simp: simpler_gets_def bind_def obind_def return_def split: option.splits) + +lemma mres_assert_opt: + "mres (assert_opt opt s) = (if opt = None then {} else {(the opt,s)})" + by (clarsimp simp: assert_opt_def fail_def return_def mres_def vimage_def split: option.split) + + +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_oapply_comp + +lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def + + +section "Relation between option monad loops and trace monad loops." + +(* Option monad whileLoop formalisation thanks to Lars Noschinski . *) + +lemma gets_the_conv: + "(gets_the B s) = (case B s of Some r' \ ({([], Result (r', s))}) | _ \ {([], Failed)})" + by (auto simp: gets_the_def gets_def get_def bind_def return_def fail_def assert_opt_def split: option.splits) + +lemma gets_the_loop_terminates: + "whileLoop_terminates C (\a. gets_the (B a)) r s + \ (\rs'. (Some r, rs') \ option_while' (\a. C a s) (\a. B a s))" (is "?L \ ?R") +proof + assume ?L then show ?R + proof (induct rule: whileLoop_terminates.induct[case_names 1 2]) + case (2 r s) then show ?case + by (cases "B r s") (auto simp: gets_the_conv intro: option_while'.intros) + qed (auto intro: option_while'.intros) +next + assume ?R then show ?L + proof (elim exE) + fix rs' assume "(Some r, rs') \ option_while' (\a. C a s) (\a. B a s)" + then have "whileLoop_terminates C (\a. gets_the (B a)) (the (Some r)) s" + by induct (auto intro: whileLoop_terminates.intros simp: gets_the_conv) + then show ?thesis by simp + qed +qed + +lemma The_eqD: + "\The P = x; \!x. P x\ \ P x" + by (metis theI) + +lemma gets_the_whileLoop: + fixes C :: "'a \ 's \ bool" + assumes terminates: "\s. whileLoop_terminates C (\a. gets_the (B a)) r s" + shows "whileLoop C (\a. gets_the (B a)) r = gets_the (owhile C B r)" +proof - + { fix r s r' s' ts assume "((r,s), ts, Result (r', s')) \ whileLoop_results C (\a. gets_the (B a))" + then have "s = s' \ ts = [] \(Some r, Some r') \ option_while' (\a. C a s) (\a. B a s)" + by (induct r s ts "Result (r', s')") + (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } + note wl'_Result = this + + { fix r s ts assume "((r,s), ts, Failed) \ whileLoop_results C (\a. gets_the (B a))" + then have "ts = [] \ (Some r, None) \ option_while' (\a. C a s) (\a. B a s)" + by (induct r s ts "Failed :: (('s, 'a) tmres)") + (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } + note wl'_Failed = this + + { fix r s ts assume "((r,s), ts, Incomplete) \ whileLoop_results C (\a. gets_the (B a))" + then have "False" + by (induct r s ts "Incomplete :: (('s, 'a) tmres)") + (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } + note wl'_Incomplete = this + + { fix r s r' assume "(Some r, Some r') \ option_while' (\a. C a s) (\a. B a s)" + then have "((r,s), [], Result (r',s)) \ whileLoop_results C (\a. gets_the (B a))" + by (induct "Some r" "Some r'" arbitrary: r) + (auto intro: whileLoop_results.intros simp: gets_the_conv) } + note option_while'_Some = this + + { fix r s assume "(Some r, None) \ option_while' (\a. C a s) (\a. B a s)" + then have "((r,s), [], Failed) \ whileLoop_results C (\a. gets_the (B a))" + by (induct "Some r" "None :: 'a option" arbitrary: r) + (auto intro: whileLoop_results.intros simp: gets_the_conv) } + note option_while'_None = this + + have "\s. owhile C B r s = None + \ whileLoop C (\a. gets_the (B a)) r s = {([], Failed)}" + using terminates + by (intro subset_antisym; + clarsimp simp: whileLoop_def owhile_def option_while_def gets_the_loop_terminates + split: if_split_asm intro!: option_while'_None dest!: The_eqD) + (case_tac b, auto dest!: wl'_Result wl'_Failed wl'_Incomplete option_while'_inj option_while'_THE) + moreover + have "\s r'. owhile C B r s = Some r' + \ whileLoop C (\a. gets_the (B a)) r s = {([], Result (r', s))}" + by (intro subset_antisym; + clarsimp simp: whileLoop_def owhile_def option_while_def option_while'_THE + split: if_split_asm intro!: option_while'_Some) + (case_tac b, auto dest: wl'_Result wl'_Failed wl'_Incomplete option_while'_inj) + ultimately + show ?thesis + by (auto simp: fun_eq_iff gets_the_conv split: option.split) +qed + +end