Theory Seq_MonadSE

(******************************************************************************
 * Clean
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

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,) MONSE)  ('o list,) MONSE"  
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 ("mbindFailSave") (* future name: mbindFailSave *)

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 bindSE}.› 
 
fun    mbind' :: " list    (  ('o,) MONSE)  ('o list,) MONSE"
where "mbind' [] iostep σ = Some([], σ)" |
      "mbind' (a#S) iostep σ = 
                (case iostep a σ of 
                     None    None
                  |  Some (out, σ')  (case mbind' S iostep σ' of 
                                          None     None   ― ‹fail-strict› 
                                        | Some(outs,σ'')  Some(out#outs,σ'')))"
notation mbind' ("mbindFailStop") (* future name: mbindFailStop *)

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] (* use only more abstract definitions *)

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,) MONSE)  ('o list,) MONSE"
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   ― ‹does not occur› 
                                        | Some(outs,σ'')  Some(out#outs,σ'')))"

notation mbind'' ("mbindFailPurge") (* future name: mbindPurgeFail *)
declare  mbind''.simps[simp del] (* use only more abstract definitions *)


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'  trySE(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