lib/monads/trace: update definitions and rules taken from nondet

This commit has all of the changes required so that the definitions and
rules added in the previous commit work for the trace monad.

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/Fun_Pred_Syntax.thy

@@ -173,6 +173,17 @@ lemmas pred_neg_bot_eq[simp] =
    entirely in the future *)
 
 
+subsection "Simplification Rules for Lifted And/Or"
+
+lemma bipred_disj_op_eq[simp]:
+  "reflp R \<Longrightarrow> ((=) or R) = R"
+  "reflp R \<Longrightarrow> (R or (=)) = R"
+  by (auto simp: reflp_def)
+
+lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
+  by clarsimp
+
+
 section \<open>Examples\<close>
 
 experiment

lib/Monads/Monad_Lib.thy

@@ -69,4 +69,8 @@ lemma sum_all_ex[simp]:
   "(\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)"
   by (metis Inr_not_Inl sum.exhaust)+
 
+lemma context_disjE:
+  "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>\<not>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by auto
+
 end

lib/Monads/trace/Trace_Empty_Fail.thy

@@ -14,14 +14,16 @@ begin
 section \<open>Monads that are wellformed w.r.t. failure\<close>
 
 text \<open>
-  Usually, well-formed monads constructed from the primitives in Nondet_Monad will have the following
-  property: if they return an empty set of results, they will have the failure flag set.\<close>
-definition empty_fail :: "('s,'a) nondet_monad \<Rightarrow> bool" where
-  "empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)"
+  Usually, well-formed monads constructed from the primitives in Trace_Monad will have the following
+  property: if they return an empty set of completed results, there exists a trace corresponding to
+  a failed result.\<close>
+definition empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" where
+  "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> Failed \<in> snd ` (m s)"
 
 text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close>
-definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where
-  "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"
+definition mk_ef ::
+  "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set" where
+  "mk_ef S \<equiv> if mres S = {} then S \<union> {([], Failed)} else S"
 
 
 subsection \<open>WPC setup\<close>
@@ -36,34 +38,36 @@ wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail_final
 subsection \<open>@{const empty_fail} intro/dest rules\<close>
 
 lemma empty_failI:
-  "(\<And>s. fst (m s) = {} \<Longrightarrow> snd (m s)) \<Longrightarrow> empty_fail m"
+  "(\<And>s. mres (m s) = {} \<Longrightarrow> Failed \<in> snd ` (m s)) \<Longrightarrow> empty_fail m"
   by (simp add: empty_fail_def)
 
 lemma empty_failD:
-  "\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> snd (m s)"
+  "\<lbrakk> empty_fail m; mres (m s) = {} \<rbrakk> \<Longrightarrow> Failed \<in> snd ` (m s)"
   by (simp add: empty_fail_def)
 
 lemma empty_fail_not_snd:
-  "\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
+  "\<lbrakk> Failed \<notin> snd ` (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)"
   by (fastforce simp: empty_fail_def)
 
 lemmas empty_failD2 = empty_fail_not_snd[rotated]
 
 lemma empty_failD3:
-  "\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}"
+  "\<lbrakk> empty_fail f; Failed \<notin> snd ` (f s) \<rbrakk> \<Longrightarrow> mres (f s) \<noteq> {}"
   by (drule(1) empty_failD2, clarsimp)
 
 lemma empty_fail_bindD1:
   "empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
   unfolding empty_fail_def bind_def
-  by (fastforce simp: split_def image_image)
+  apply clarsimp
+  apply (drule_tac x=s in spec)
+  by (force simp: split_def mres_def vimage_def split: tmres.splits)
 
 
 subsection \<open>Wellformed monads\<close>
 
 (*
   Collect generic empty_fail lemmas here:
-   - naming convention is emtpy_fail_NAME.
+   - naming convention is empty_fail_NAME.
    - add lemmas with assumptions to [empty_fail_cond] set
    - add lemmas without assumption to [empty_fail_term] set
 *)
@@ -91,32 +95,53 @@ lemma empty_fail_If_applied[empty_fail_cond]:
 
 lemma empty_fail_put[empty_fail_term]:
   "empty_fail (put f)"
-  by (simp add: put_def empty_fail_def)
+  by (simp add: put_def empty_fail_def mres_def vimage_def)
 
 lemma empty_fail_modify[empty_fail_term]:
   "empty_fail (modify f)"
-  by (simp add: empty_fail_def simpler_modify_def)
+  by (simp add: empty_fail_def simpler_modify_def mres_def vimage_def)
 
 lemma empty_fail_gets[empty_fail_term]:
   "empty_fail (gets f)"
-  by (simp add: empty_fail_def simpler_gets_def)
+  by (simp add: empty_fail_def simpler_gets_def mres_def vimage_def)
 
 lemma empty_fail_select[empty_fail_cond]:
   "S \<noteq> {} \<Longrightarrow> empty_fail (select S)"
-  by (simp add: empty_fail_def select_def)
-
-lemma empty_fail_select_f[empty_fail_cond]:
-  assumes ef: "fst S = {} \<Longrightarrow> snd S"
-  shows "empty_fail (select_f S)"
-  by (fastforce simp add: empty_fail_def select_f_def intro: ef)
+  by (simp add: empty_fail_def select_def mres_def image_def)
+
+lemma mres_bind_empty:
+  "mres ((f >>= g) s) = {}
+   \<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {})"
+  apply clarsimp
+  apply (clarsimp simp: mres_def split_def vimage_def bind_def)
+  apply (rename_tac rv s' trace)
+  apply (drule_tac x=rv in spec, drule_tac x=s' in spec)
+  apply (clarsimp simp: image_def)
+  apply fastforce
+  done
+
+lemma bind_FailedI1:
+  "Failed \<in> snd ` f s \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
+  by (force simp: bind_def vimage_def)
+
+lemma bind_FailedI2:
+  "\<lbrakk>\<forall>res\<in>mres (f s). Failed \<in> snd ` (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk>
+   \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
+  by (force simp: bind_def mres_def image_def split_def)
 
 lemma empty_fail_bind[empty_fail_cond]:
   "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
-  by (fastforce simp: bind_def empty_fail_def split_def)
+  unfolding empty_fail_def
+  apply clarsimp
+  apply (drule mres_bind_empty)
+  apply (erule context_disjE)
+   apply (fastforce intro: bind_FailedI1)
+  apply (fastforce intro!: bind_FailedI2)
+  done
 
 lemma empty_fail_return[empty_fail_term]:
   "empty_fail (return x)"
-  by (simp add: empty_fail_def return_def)
+  by (simp add: empty_fail_def return_def mres_def vimage_def)
 
 lemma empty_fail_returnOk[empty_fail_term]:
   "empty_fail (returnOk v)"
@@ -191,7 +216,7 @@ lemma empty_fail_assertE[empty_fail_term]:
 
 lemma empty_fail_get[empty_fail_term]:
   "empty_fail get"
-  by (simp add: empty_fail_def get_def)
+  by (simp add: empty_fail_def get_def mres_def vimage_def)
 
 lemma empty_fail_catch[empty_fail_cond]:
   "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
@@ -203,7 +228,7 @@ lemma empty_fail_guard[empty_fail_term]:
 
 lemma empty_fail_spec[empty_fail_term]:
   "empty_fail (state_select F)"
-  by (clarsimp simp: state_select_def empty_fail_def)
+  by (clarsimp simp: state_select_def empty_fail_def default_elem_def mres_def image_def)
 
 lemma empty_fail_when[empty_fail_cond]:
   "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
@@ -321,7 +346,7 @@ subsection \<open>Equations and legacy names\<close>
 
 lemma empty_fail_select_eq[simp]:
   "empty_fail (select V) = (V \<noteq> {})"
-  by (clarsimp simp: select_def empty_fail_def)
+  by (clarsimp simp: select_def empty_fail_def mres_def image_def)
 
 lemma empty_fail_liftM_eq[simp]:
   "empty_fail (liftM f m) = empty_fail m"
@@ -330,7 +355,7 @@ lemma empty_fail_liftM_eq[simp]:
 
 lemma empty_fail_liftE_eq[simp]:
   "empty_fail (liftE f) = empty_fail f"
-  by (fastforce simp: liftE_def empty_fail_def bind_def)
+  by (auto simp: liftE_def empty_fail_bindD1)
 
 lemma liftME_empty_fail_eq[simp]:
   "empty_fail (liftME f m) = empty_fail m"

lib/Monads/trace/Trace_In_Monad.thy

@@ -55,8 +55,8 @@ lemma inl_whenE:
   by (auto simp add: in_whenE)
 
 lemma inr_in_unlessE_throwError[termination_simp]:
-  "(Inr (), s') \<in> fst (unlessE P (throwError E) s) = (P \<and> s'=s)"
-  by (simp add: unlessE_def returnOk_def throwError_def return_def)
+  "(Inr (), s') \<in> mres (unlessE P (throwError E) s) = (P \<and> s'=s)"
+  by (simp add: unlessE_def returnOk_def throwError_def in_return)
 
 lemma in_fail:
   "r \<in> mres (fail s) = False"
@@ -90,6 +90,18 @@ lemma in_when:
   "(v, s') \<in> mres (when P f s) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))"
   by (simp add: when_def in_return)
 
+lemma in_unless:
+  "(v, s') \<in> mres (unless P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))"
+  by (simp add: unless_def in_when)
+
+lemma in_unlessE:
+  "(v, s') \<in> mres (unlessE P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))"
+  by (simp add: unlessE_def in_returnOk)
+
+lemma inl_unlessE:
+  "((Inl x, s') \<in> mres (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> mres (f s))"
+  by (auto simp add: in_unlessE)
+
 lemma in_modify:
   "(v, s') \<in> mres (modify f s) = (s'=f s \<and> v = ())"
   by (auto simp add: modify_def bind_def get_def put_def mres_def)
@@ -118,8 +130,8 @@ lemma in_bindE:
 lemmas in_monad = inl_whenE in_whenE in_liftE in_bind in_bindE_L
                   in_bindE_R in_returnOk in_throwError in_fail
                   in_assertE in_assert in_return in_assert_opt
-                  in_get in_gets in_put in_when (* unlessE_whenE *)
-                  (* unless_when *) in_modify gets_the_in_monad
+                  in_get in_gets in_put in_when inl_unlessE in_unlessE
+                  in_unless in_modify gets_the_in_monad
                   in_alternative in_liftM
 
 lemma bind_det_exec:

lib/Monads/trace/Trace_Lemmas.thy

@@ -31,15 +31,15 @@ lemma bind_apply_cong':
 lemmas bind_apply_cong = bind_apply_cong'[rule_format, fundef_cong]
 
 lemma bind_cong[fundef_cong]:
-  "\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> fst (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
-  by (auto simp: bind_def Let_def split_def intro: rev_image_eqI)
+  "\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> mres (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
+  by (auto intro!: bind_apply_cong)
 
 lemma bindE_cong[fundef_cong]:
-  "\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> fst (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'"
+  "\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> mres (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'"
   by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_cong)
 
 lemma bindE_apply_cong[fundef_cong]:
-  "\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> fst (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
+  "\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> mres (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
   \<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'"
   by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_apply_cong)
 
@@ -63,11 +63,12 @@ lemma unlessE_apply_cong[fundef_cong]:
   "\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unlessE C m s = unlessE C' m' s'"
   by (simp add: unlessE_def)
 
+
 subsection \<open>Simplifying Monads\<close>
 
 lemma nested_bind[simp]:
   "do x <- do y <- f; return (g y) od; h x od = do y <- f; h (g y) od"
-  by (clarsimp simp: bind_def Let_def split_def return_def)
+  by (fastforce simp: bind_def return_def split: tmres.splits)
 
 lemma bind_dummy_ret_val:
   "do y \<leftarrow> a; b od = do a; b od"