Theory Seq_MonadSE
theory Seq_MonadSE
imports MonadSE
begin
subsection‹ Chaining Monadic Computations : Definitions of Multi-bind Operators ›
text‹ In order to express execution sequences inside \HOL --- rather
than arguing over a certain pattern of terms on the meta-level --- and
in order to make our theory amenable to formal reasoning over execution sequences,
we represent them as lists of input and generalize the bind-operator
of the state-exception monad accordingly. The approach is straightforward,
but comes with a price: we have to encapsulate all input and output data
into one type, and restrict ourselves to a uniform step function.
Assume that we have a typed interface to a module with
the operations $op_1$, $op_2$, \ldots, $op_n$ with the inputs
$\iota_1$, $\iota_2$, \ldots, $\iota_n$ (outputs are treated analogously).
Then we can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express
that in traces only \emph{corresponding} input and output belonging to the
same operation will occur; this form of side-conditions have to be expressed
inside \HOL. From the user perspective, this will not make much difference,
since junk-data resulting from too weak typing can be ruled out by adopted
front-ends.
›
text‹ Note that the subsequent notion of a test-sequence allows the io stepping
function (and the special case of a program under test) to stop execution
\emph{within} the sequence; such premature terminations are characterized by an
output list which is shorter than the input list.
Intuitively, ‹mbind› corresponds to a sequence of operation calls, separated by
";", in Java. The operation calls may fail (raising an exception), which means that
the state is maintained and the exception can still be caught at the end of the
execution sequence.
›
fun mbind :: "'ι list ⇒ ('ι ⇒ ('o,'σ) MON⇩S⇩E) ⇒ ('o list,'σ) MON⇩S⇩E"
where "mbind [] iostep σ = Some([], σ)"
| "mbind (a#S) iostep σ =
(case iostep a σ of
None ⇒ Some([], σ)
| Some (out, σ') ⇒ (case mbind S iostep σ' of
None ⇒ Some([out],σ')
| Some(outs,σ'') ⇒ Some(out#outs,σ'')))"
notation mbind ("mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e")
text‹This definition is fail-safe; in case of an exception, the current state is maintained,
the computation as a whole is marked as success.
Compare to the fail-strict variant ‹mbind'›:›
lemma mbind_unit [simp]:
"mbind [] f = (result [])"
by(rule ext, simp add: unit_SE_def)
text‹The characteristic property of @{term mbind} --- which distinguishes it from
‹mbind› defined in the sequel --- is that it never fails; it ``swallows'' internal
errors occuring during the computation.›
lemma mbind_nofailure [simp]:
"mbind S f σ ≠ None"
apply(rule_tac x=σ in spec)
apply(induct S, auto simp:unit_SE_def)
apply(case_tac "f a x", auto)
apply(erule_tac x="b" in allE)
apply(erule exE, erule exE, simp)
done
text‹In contrast, we define a fail-strict sequential execution operator.
He has more the characteristic to fail globally whenever one of its operation
steps fails.
Intuitively speaking, ‹mbind'› corresponds to an execution of operations
where a results in a System-Halt. Another interpretation of ‹mbind'› is to
view it as a kind of @{term foldl} foldl over lists via @{term bind⇩S⇩E}.›
fun mbind' :: "'ι list ⇒ ('ι ⇒ ('o,'σ) MON⇩S⇩E) ⇒ ('o list,'σ) MON⇩S⇩E"
where "mbind' [] iostep σ = Some([], σ)" |
"mbind' (a#S) iostep σ =
(case iostep a σ of
None ⇒ None
| Some (out, σ') ⇒ (case mbind' S iostep σ' of
None ⇒ None
| Some(outs,σ'') ⇒ Some(out#outs,σ'')))"
notation mbind' ("mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p")
lemma mbind'_unit [simp]:
"mbind' [] f = (result [])"
by(rule ext, simp add: unit_SE_def)
lemma mbind'_bind [simp]:
"(x ← mbind' (a#S) F; M x) = (a ← (F a); (x ← mbind' S F; M (a # x)))"
by(rule ext, rename_tac "z",simp add: bind_SE_def split: option.split)
declare mbind'.simps[simp del]
text‹The next ‹mbind› sequential execution operator is called
Fail-Purge. He has more the characteristic to never fail, just "stuttering"
above operation steps that fail. Another alternative in modeling.›
fun mbind'' :: "'ι list ⇒ ('ι ⇒ ('o,'σ) MON⇩S⇩E) ⇒ ('o list,'σ) MON⇩S⇩E"
where "mbind'' [] iostep σ = Some([], σ)" |
"mbind'' (a#S) iostep σ =
(case iostep a σ of
None ⇒ mbind'' S iostep σ
| Some (out, σ') ⇒ (case mbind'' S iostep σ' of
None ⇒ None
| Some(outs,σ'') ⇒ Some(out#outs,σ'')))"
notation mbind'' ("mbind⇩F⇩a⇩i⇩l⇩P⇩u⇩r⇩g⇩e")
declare mbind''.simps[simp del]
text‹mbind' as failure strict operator can be seen as a foldr on bind -
if the types would match \ldots›
subsubsection‹Definition : Miscellaneous Operators and their Properties›
lemma mbind_try:
"(x ← mbind (a#S) F; M x) =
(a' ← try⇩S⇩E(F a);
if a' = None
then (M [])
else (x ← mbind S F; M (the a' # x)))"
apply(rule ext)
apply(simp add: bind_SE_def try_SE_def)
apply(case_tac "F a x", auto)
apply(simp add: bind_SE_def try_SE_def)
apply(case_tac "mbind S F b", auto)
done
end