lib/monads: restyle and reorder trace files

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

lib/Monads/trace/Trace_Monad.thy

@@ -41,9 +41,9 @@ abbreviation map_tmres_rv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a) tmres
 section "The Monad"
 
 text \<open>
-  tmonad returns a set of non-deterministic  computations, including
+  tmonad returns a set of non-deterministic computations, including
   a trace as a list of "thread identifier" \<times> state, and an optional
-  pair result, state when the computation did not fail.\<close>
+  pair of result and state when the computation did not fail.\<close>
 type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set"
 
 text \<open>
@@ -104,10 +104,12 @@ abbreviation(input) bind_rev ::
   "g =<< f \<equiv> f >>= g"
 
 text \<open>
-  The basic accessor functions of the state monad. @{text get} returns
-  the current state as result, does not fail, and does not change the state.
-  @{text "put s"} returns nothing (@{typ unit}), changes the current state
-  to @{text s} and does not fail.\<close>
+  The basic accessor functions of the state monad. @{text get} returns the
+  current state as result, does not change the state, and does not add to the
+  trace. @{text "put s"} returns nothing (@{typ unit}), changes the current
+  state to @{text s}, and does not add to the trace. @{text "put_trace xs"}
+  returns nothing (@{typ unit}), does not change the state, and adds @{text xs}
+  to the trace.\<close>
 definition get :: "('s,'s) tmonad" where
   "get \<equiv> \<lambda>s. {([], Result (s, s))}"
 
@@ -125,10 +127,10 @@ subsection "Nondeterminism"
 
 text \<open>
   Basic nondeterministic functions. @{text "select A"} chooses an element
-  of the set @{text A}, does not change the state, and does not fail
-  (even if the set is empty). @{text "f \<sqinter> g"} executes @{text f} or
-  executes @{text g}. It retuns the union of results of @{text f} and
-  @{text g}, and may have failed if either may have failed.\<close>
+  of the set @{text A} as the result, does not change the state, does not add
+  to the trace, and does not fail (even if the set is empty). @{text "f \<sqinter> g"}
+  executes @{text f} or executes @{text g}. It returns the union of results and
+  traces of @{text f} and @{text g}.\<close>
 definition select :: "'a set \<Rightarrow> ('s, 'a) tmonad" where
   "select A \<equiv> \<lambda>s. (Pair [] ` Result ` (A \<times> {s}))"
 
@@ -137,13 +139,13 @@ definition alternative :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightar
   "f \<sqinter> g \<equiv> \<lambda>s. (f s \<union> g s)"
 
 text \<open>
-  The @{text select_f} function was left out here until we figure
+  FIXME: The @{text select_f} function was left out here until we figure
   out what variant we actually need.\<close>
 
 subsection "Failure"
 
 text \<open>
-  The monad function that always fails. Returns an empty set of results and sets the failure flag.\<close>
+  The monad function that always fails. Returns an empty trace with a Failed result.\<close>
 definition fail :: "('s, 'a) tmonad" where
   "fail \<equiv> \<lambda>s. {([], Failed)}"
 
@@ -233,6 +235,7 @@ lemma elem_bindE:
 
 text \<open>Each monad satisfies at least the following three laws.\<close>
 
+\<comment> \<open>FIXME: is this necessary? If it is, move it\<close>
 declare map_option.identity[simp]
 
 text \<open>@{term return} is absorbed at the left of a @{term bind}, applying the return value directly:\<close>
@@ -470,6 +473,7 @@ text \<open>
 definition last_st_tr :: "(tmid * 's) list \<Rightarrow> 's \<Rightarrow> 's" where
   "last_st_tr tr s0 \<equiv> hd (map snd tr @ [s0])"
 
+text \<open>Nondeterministically add all possible environment events to the trace.\<close>
 definition env_steps :: "('s,unit) tmonad" where
   "env_steps \<equiv>
   do
@@ -482,13 +486,17 @@ definition env_steps :: "('s,unit) tmonad" where
     put (last_st_tr tr s)
   od"
 
+text \<open>Add the current state to the trace, tagged as a self action.\<close>
 definition commit_step :: "('s,unit) tmonad" where
   "commit_step \<equiv>
   do
     s \<leftarrow> get;
     put_trace [(Me,s)]
   od"
 
+text \<open>
+  Record the action taken by the current thread since the last interference point and
+  then add unfiltered environment events.\<close>
 definition interference :: "('s,unit) tmonad" where
   "interference \<equiv>
   do
@@ -645,7 +653,8 @@ subsection "Loops"
 text \<open>
   Loops are handled using the following inductive predicate;
   non-termination is represented using the failure flag of the
-  monad.\<close>
+  monad.
+FIXME: update comment about non-termination\<close>
 
 inductive_set whileLoop_results ::
   "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> (('r \<times> 's) \<times> ((tmid \<times> 's) list \<times> ('s, 'r) tmres)) set"

lib/Monads/trace/Trace_Monad_Equations.thy

@@ -45,38 +45,40 @@ lemma fail_bind[simp]:
   by (simp add: bind_def fail_def)
 
 
+subsection \<open>Alternative env_steps with repeat\<close>
+
 lemma mapM_Cons:
   "mapM f (x # xs) = do
-    y \<leftarrow> f x;
-    ys \<leftarrow> mapM f xs;
-    return (y # ys)
-  od"
+     y \<leftarrow> f x;
+     ys \<leftarrow> mapM f xs;
+     return (y # ys)
+   od"
   and mapM_Nil:
   "mapM f [] = return []"
   by (simp_all add: mapM_def sequence_def)
 
 lemma mapM_x_Cons:
   "mapM_x f (x # xs) = do
-    y \<leftarrow> f x;
-    mapM_x f xs
-  od"
+     y \<leftarrow> f x;
+     mapM_x f xs
+   od"
   and mapM_x_Nil:
   "mapM_x f [] = return ()"
   by (simp_all add: mapM_x_def sequence_x_def)
 
 lemma mapM_append:
   "mapM f (xs @ ys) = (do
-    fxs \<leftarrow> mapM f xs;
-    fys \<leftarrow> mapM f ys;
-    return (fxs @ fys)
-  od)"
+     fxs \<leftarrow> mapM f xs;
+     fys \<leftarrow> mapM f ys;
+     return (fxs @ fys)
+   od)"
   by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc)
 
 lemma mapM_x_append:
   "mapM_x f (xs @ ys) = (do
-    x \<leftarrow> mapM_x f xs;
-    mapM_x f ys
-  od)"
+     x \<leftarrow> mapM_x f xs;
+     mapM_x f ys
+   od)"
   by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc)
 
 lemma mapM_map:
@@ -87,24 +89,18 @@ lemma mapM_x_map:
   "mapM_x f (map g xs) = mapM_x (f o g) xs"
   by (induct xs; simp add: mapM_x_Nil mapM_x_Cons)
 
-primrec
-  repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
-where
+primrec repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
     "repeat_n 0 f = return ()"
   | "repeat_n (Suc n) f = do f; repeat_n n f od"
 
 lemma repeat_n_mapM_x:
   "repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())"
   by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil)
 
-definition
-  repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
-where
+definition repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
   "repeat f = do n \<leftarrow> select UNIV; repeat_n n f od"
 
-definition
-  env_step :: "('s,unit) tmonad"
-where
+definition env_step :: "('s,unit) tmonad" where
   "env_step =
   (do
     s' \<leftarrow> select UNIV;
@@ -117,7 +113,7 @@ abbreviation
 
 lemma elem_select_bind:
   "(tr, res) \<in> (do x \<leftarrow> select S; f x od) s
-    = (\<exists>x \<in> S. (tr, res) \<in> f x s)"
+   = (\<exists>x \<in> S. (tr, res) \<in> f x s)"
   by (simp add: bind_def select_def)
 
 lemma select_bind_UN:
@@ -126,17 +122,17 @@ lemma select_bind_UN:
 
 lemma select_early:
   "S \<noteq> {}
-    \<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
-        = do y \<leftarrow> select S; x \<leftarrow> f; g x y od"
+   \<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
+       = do y \<leftarrow> select S; x \<leftarrow> f; g x y od"
   apply (simp add: bind_def select_def Sigma_def)
   apply (rule ext)
   apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm)
   done
 
 lemma repeat_n_choice:
   "S \<noteq> {}
-    \<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
-        = (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)"
+   \<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
+       = (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)"
   apply (induct n; simp?)
    apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong)
   apply (simp add: select_early bind_assoc)
@@ -151,8 +147,8 @@ lemma repeat_n_choice:
 
 lemma repeat_choice:
   "S \<noteq> {}
-    \<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
-        = (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)"
+   \<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
+       = (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)"
   apply (simp add: repeat_def repeat_n_choice)
   apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind)
   done
@@ -163,27 +159,27 @@ lemma put_trace_append:
 
 lemma put_trace_elem_put_comm:
   "do y \<leftarrow> put_trace_elem x; put s od
-    = do y \<leftarrow> put s; put_trace_elem x od"
+   = do y \<leftarrow> put s; put_trace_elem x od"
   by (simp add: put_def put_trace_elem_def bind_def insert_commute)
 
 lemma put_trace_put_comm:
   "do y \<leftarrow> put_trace xs; put s od
-    = do y \<leftarrow> put s; put_trace xs od"
+   = do y \<leftarrow> put s; put_trace xs od"
   apply (rule sym; induct xs; simp)
   apply (simp add: bind_assoc put_trace_elem_put_comm)
   apply (simp add: bind_assoc[symmetric])
   done
 
 lemma mapM_x_comm:
   "(\<forall>x \<in> set xs. do y \<leftarrow> g; f x od = do y \<leftarrow> f x; g od)
-    \<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od"
+   \<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od"
   apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons)
   apply (simp add: bind_assoc[symmetric], simp add: bind_assoc)
   done
 
 lemma mapM_x_split:
   "(\<forall>x \<in> set xs. \<forall>y \<in> set xs. do z \<leftarrow> g y; f x od = do (z :: unit) \<leftarrow> f x; g y od)
-    \<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od"
+   \<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od"
   apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc)
   apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x])
    apply simp
@@ -236,15 +232,15 @@ lemma repeat_eq_twice[simp]:
   apply (rule ext, fastforce intro: exI[where x=0])
   done
 
-lemmas repeat_eq_twice_then[simp]
-    = repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc]
+lemmas repeat_eq_twice_then[simp] =
+  repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc]
 
-lemmas env_steps_eq_twice[simp]
-    = repeat_eq_twice[where f=env_step, folded env_steps_repeat]
-lemmas env_steps_eq_twice_then[simp]
-    = env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc]
+lemmas env_steps_eq_twice[simp] =
+  repeat_eq_twice[where f=env_step, folded env_steps_repeat]
+lemmas env_steps_eq_twice_then[simp] =
+  env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc]
 
-lemmas mapM_collapse_append = mapM_append[symmetric, THEN bind_then_eq,
-    simplified bind_assoc, simplified]
+lemmas mapM_collapse_append =
+  mapM_append[symmetric, THEN bind_then_eq, simplified bind_assoc, simplified]
 
 end

lib/Monads/trace/Trace_No_Fail.thy

@@ -17,9 +17,9 @@ begin
 subsection "Non-Failure"
 
 text \<open>
-  With the failure flag, we can formulate non-failure separately from validity.
+  With the failure result, we can formulate non-failure separately from validity.
   A monad @{text m} does not fail under precondition @{text P}, if for no start
-  state that satisfies the precondition it sets the failure flag.
+  state that satisfies the precondition it returns a @{term Failed} result.
 \<close>
 definition no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> bool" where
   "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> Failed \<notin> snd ` (m s)"

lib/Monads/trace/Trace_No_Trace.thy

@@ -11,32 +11,39 @@ imports
   WPSimp
 begin
 
-definition
-  no_trace :: "('s,'a) tmonad  \<Rightarrow> bool"
-where
+subsection "No Trace"
+
+text \<open>
+  A monad of type @{text tmonad} does not have a trace iff for all starting
+  states, all of the potential outcomes have the empty list as a trace and do
+  not return an @{term Incomplete} result.\<close>
+definition no_trace :: "('s,'a) tmonad  \<Rightarrow> bool" where
   "no_trace f = (\<forall>tr res s. (tr, res) \<in> f s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete)"
 
 lemmas no_traceD = no_trace_def[THEN iffD1, rule_format]
 
 lemma no_trace_emp:
-  "no_trace f \<Longrightarrow> (tr, r) \<in> f s \<Longrightarrow> tr = []"
+  "\<lbrakk>no_trace f; (tr, r) \<in> f s\<rbrakk> \<Longrightarrow> tr = []"
   by (simp add: no_traceD)
 
 lemma no_trace_Incomplete_mem:
   "no_trace f \<Longrightarrow> (tr, Incomplete) \<notin> f s"
   by (auto dest: no_traceD)
 
 lemma no_trace_Incomplete_eq:
-  "no_trace f \<Longrightarrow> (tr, res) \<in> f s \<Longrightarrow> res \<noteq> Incomplete"
+  "\<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> res \<noteq> Incomplete"
   by (auto dest: no_traceD)
 
-lemma no_trace_is_triple:
+
+subsection \<open>Set up for @{method wp}\<close>
+
+lemma no_trace_is_triple[wp_trip]:
   "no_trace f = triple_judgement \<top> f (\<lambda>() f. id no_trace f)"
   by (simp add: triple_judgement_def split: unit.split)
 
-lemmas [wp_trip] = no_trace_is_triple
 
-(* Since valid_validI_wp in wp_comb doesn't work, we add the rules directly in the wp set *)
+subsection \<open>Rules\<close>
+
 lemma no_trace_prim:
   "no_trace get"
   "no_trace (put s)"