Quelle  Seq_MonadSE.thy

(******************************************************************************
 * 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
  arguing over a certain pattern of terms on the meta-level --- and
  order to make our theory amenable to formal reasoning over execution sequences,
  represent them as lists of input and generalize the bind-operator
  the state-exception monad accordingly. The approach is straightforward,
  comes with a price: we have to encapsulate all input and output data
  one type, and restrict ourselves to a uniform step function.
  that we have a typed interface to a module with
  operations $op_1$, $op_2$, \ldots, $op_n$ with the inputs
 \iota_1$, $\iota_2$, \ldots, $\iota_n$ (outputs are treated analogously).
  we can encode for this interface the general input - type:
 begin{displaymath}
 texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
 end{displaymath}
 , we loose some type-safety in this approach; we have to express
  in traces only \emph{corresponding} input and output belonging to the
  operation will occur; this form of side-conditions have to be expressed
  \HOL. From the user perspective, this will not make much difference,
  junk-data resulting from too weak typing can be ruled out by adopted
 -ends.
 ›

text‹ Note that the subsequent notion of a test-sequence allows the io stepping
  (and the special case of a program under test) to stop execution
 emph{within} the sequence; such premature terminations are characterized by an
  list which is shorter than the input list.

 , ‹mbind› corresponds to a sequence of operation calls, separated by
 ;", in Java. The operation calls may fail (raising an exception), which means that
  state is maintained and the exception can still be caught at the end of the
  sequence.

 ›

fun    mbind :: "'ι list ==> ('ι ==> ('o,'σ) MON_SE) ==> ('o list,'σ) MON_SE"  
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_FailSave›) (* future name: mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>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.
  has more the characteristic to fail globally whenever one of its operation
  fails.

  speaking, ‹mbind'› corresponds to an execution of operations
  a results in a System-Halt. Another interpretation of ‹mbind'› is to
  it as a kind of @{term foldl} foldl over lists via @{term bind_SE}.›
 
fun    mbind' :: "'ι list ==> ('ι ==> ('o,'σ) MON_SE) ==> ('o list,'σ) MON_SE"
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' (‹mbind_FailStop›) (* future name: mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>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] (* use only more abstract definitions *)

text‹The next ‹mbind› sequential execution operator is called
 -Purge. He has more the characteristic to never fail, just "stuttering"
  operation steps that fail. Another alternative in modeling.›

fun    mbind'' :: "'ι list ==> ('ι ==> ('o,'σ) MON_SE) ==> ('o list,'σ) MON_SE"
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'' (‹mbind_FailPurge›) (* future name: mbind\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e\<^sub>F\<^sub>a\<^sub>i\<^sub>l *)
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' ← try_SE(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