Quelle  Monads.thy

(*****************************************************************************
 * HOL-TestGen --- theorem-prover based test case generation
 *                 http://www.brucker.ch/projects/hol-testgen/
 *                                                                            
 * Monads.thy --- a base testing theory for sequential computations.
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2005-2012 ETH Zurich, Switzerland
 *               2009-2017 Univ. Paris-Sud, France 
 *               2009-2015 Achim D. Brucker, Germany
 *               2015-2017 The University of Sheffield, UK
 *
 * 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.
 ******************************************************************************)

section ‹Basic Monad Theory for Sequential Computations›
theory 
  Monads 
  imports 
    Main
begin 

subsection‹General Framework for Monad-based Sequence-Test›
text‹
 As such, Higher-order Logic as a purely functional specification formalism has no built-in
 mechanism for state and state-transitions. Forms of testing involving state require therefore
 explicit mechanisms for their treatment inside the logic; a well-known technique to model
 states inside purely functional languages are \emph{monads} made popular by Wadler and Moggi
 and extensively used in Haskell. \HOL is powerful enough to represent the most important
 standard monads; however, it is not possible to represent monads as such due to well-known
 limitations of the Hindley-Milner type-system.

 Here is a variant for state-exception monads, that models precisely transition functions with
 preconditions. Next, we declare the state-backtrack-monad. In all of them, our concept of
 i/o-stepping functions can be formulated; these are functions mapping input to a given monad.
 Later on, we will build the usual concepts of:
 \begin{enumerate}
 \item deterministic i/o automata,
 \item non-deterministic i/o automata, and
 \item labelled transition systems (LTS)
 \end{enumerate}
 ›

subsubsection‹State Exception Monads›
type_synonym ('o, 'σ) MON_SE = "'σ ⇀ ('o × 'σ)"        
      
definition bind_SE :: "('o,'σ)MON_SE ==> ('o ==> ('o','σ)MON_SE) ==> ('o','σ)MON_SE" 
where     "bind_SE f g = (λσ. case f σ of None ==> None
                                        | Some (out, σ') ==> g out σ')"

notation bind_SE (‹bind_SE›)
syntax
          "_bind_SE" :: "[pttrn,('o,'σ)MON_SE,('o','σ)MON_SE] ==> ('o','σ)MON_SE"  
                                                                          (‹(2 _ ← _; _)› [5,8,8]8)
syntax_consts
          "_bind_SE" ⇌ bind_SE
translations
          "x ← f; g" ⇌ "CONST bind_SE f (% x . g)"

definition unit_SE :: "'o ==> ('o, 'σ)MON_SE"   (‹(return _)› 8) 
where     "unit_SE e = (λσ. Some(e,σ))"
notation   unit_SE (‹unit_SE›)

definition fail_SE :: "('o, 'σ)MON_SE"
where     "fail_SE = (λσ. None)"
notation   fail_SE (‹fail_SE›)

definition assert_SE :: "('σ ==> bool) ==> (bool, 'σ)MON_SE"
where     "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"
notation   assert_SE (‹assert_SE›)

definition assume_SE :: "('σ ==> bool) ==> (unit, 'σ)MON_SE"
where     "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)"
notation   assume_SE (‹assume_SE›)

definition if_SE :: "['σ ==> bool, ('α, 'σ)MON_SE, ('α, 'σ)MON_SE] ==> ('α, 'σ)MON_SE"
where     "if_SE c E F = (λσ. if c σ then E σ else F σ)" 
notation   if_SE   (‹if_SE›)

text‹
 The standard monad theorems about unit and associativity:
 ›

lemma bind_left_unit : "(x ← return a; k) = k"
  apply (simp add: unit_SE_def bind_SE_def)
  done

lemma bind_right_unit: "(x ← m; return x) = m"
  apply (simp add:  unit_SE_def bind_SE_def)
  apply (rule ext)
  subgoal for "σ"
    apply (case_tac "m σ")
     apply ( simp_all)
    done
  done

lemma bind_assoc: "(y ← (x ← m; k); h) = (x ← m; (y ← k; h))"
  apply (simp add: unit_SE_def bind_SE_def)
  apply (rule ext)
  subgoal for "σ"
    apply (case_tac "m σ", simp_all)
    subgoal for a
      apply (case_tac "a", simp_all)
      done
    done
  done

text‹
 In order to express test-sequences also on the object-level and to make our theory amenable to
 formal reasoning over test-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. 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‹
 In order to express test-sequences also on the object-level and to make our theory amenable to
 formal reasoning over test-sequences, we represent them as lists of input and generalize the
 bind-operator of the state-exception monad accordingly. Thus, the notion of test-sequence
 is mapped to the notion of a \emph{computation}, a semantic notion; at times we will use
 reifications of computations, \ie{} a data-type in order to make computation amenable to
 case-splitting and meta-theoretic reasoning. To this end, we have to encapsulate all input
 and output data into one type. 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
  (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. Note that our primary
  of multiple execution ignores failure and reports failure
  only by missing results ...›


fun    mbind :: "'ι list ==> ('ι ==> ('o,'σ) MON_SE) ==> ('o list,'σ) MON_SE"  
  where "mbind [] iostep σ = Some([], σ)" |
    "mbind (a#H) iostep σ =
                (case iostep a σ of
                     None ==> Some([], σ)
                  | Some (out, σ') ==> (case mbind H iostep σ' of
                                          None ==> Some([out],σ')
                                        | Some(outs,σ'') ==> Some(out#outs,σ'')))"

text‹As mentioned, this definition is fail-safe; in case of an exception,
  current state is maintained, no result is reported.
  alternative is the fail-strict variant ‹mbind'› defined below.›

lemma mbind_unit [simp]: "mbind [] f = (return [])"
  by(rule ext, simp add: unit_SE_def)

    
lemma mbind_nofailure [simp]: "mbind S f σ ≠ None"
  apply (rule_tac x=σ in spec)
  apply (induct S)
  using mbind.simps(1) apply force
  apply(simp add:unit_SE_def)
  apply(safe)[1]
  subgoal for a S x
    apply (case_tac "f a x")
     apply(simp)
    apply(safe)[1]
    subgoal for aa b
      apply (erule_tac x="b" in allE)
      apply (erule exE)+
      apply (simp)
      done 
    done
  done

text‹The fail-strict version of ‹mbind'› looks as follows:›
fun    mbind' :: "'ι list ==> ('ι ==> ('o,'σ) MON_SE) ==> ('o list,'σ) MON_SE"
where "mbind' [] iostep σ = Some([], σ)" |
      "mbind' (a#H) iostep σ =
                (case iostep a σ of
                     None ==> None
                  | Some (out, σ') ==> (case mbind H iostep σ' of
                                          None ==> None ― ‹fail-strict›
                                        | Some(outs,σ'') ==> Some(out#outs,σ'')))"

text‹
 mbind' as failure strict operator can be seen as a foldr on bind---if the types would
 match \ldots
 ›

definition try_SE :: "('o,'σ) MON_SE ==> ('o option,'σ) MON_SE" 
where     "try_SE ioprog = (λσ. case ioprog σ of
                                      None ==> Some(None, σ)
                                    | Some(outs, σ') ==> Some(Some outs, σ'))" 
text‹In contrast @{term mbind} as a failure safe operator can roughly be seen
 as a @{term foldr} on bind - try:
 ‹m1 ; try m2 ; try m3; ...›. Note, that the rough equivalence only holds for
 certain predicates in the sequence - length equivalence modulo None,
 for example. However, if a conditional is added, the equivalence
 can be made precise:›


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)
  subgoal for x 
    apply (case_tac "F a x")
     apply(simp)
    apply (safe)[1]
    apply (simp add: bind_SE_def try_SE_def)
    subgoal for aa b
      apply (case_tac "mbind S F b") 
       apply (auto)
      done
    done 
  done

text‹On this basis, a symbolic evaluation scheme can be established
 that reduces @{term mbind}-code to @{term try_SE}-code and If-cascades.›


definition alt_SE    :: "[('o, 'σ)MON_SE, ('o, 'σ)MON_SE] ==> ('o, 'σ)MON_SE"   (infixl ‹⊓_SE› 10)
where     "(f ⊓_SE g) = (λ σ. case f σ of None ==> g σ
                                      | Some H ==> Some H)"

definition malt_SE   :: "('o, 'σ)MON_SE list ==> ('o, 'σ)MON_SE"
where     "malt_SE S = foldr alt_SE S fail_SE"
notation   malt_SE (‹⊓_SE›)

lemma malt_SE_mt [simp]: "⊓_SE [] = fail_SE"
  by(simp add: malt_SE_def)

lemma malt_SE_cons [simp]: "⊓_SE (a # S) = (a ⊓_SE (⊓_SE S))"
  by(simp add: malt_SE_def)

subsubsection‹State-Backtrack Monads›
text‹This subsection is still rudimentary and as such an interesting
 formal analogue to the previous monad definitions. It is doubtful that it is
 interesting for testing and as a computational structure at all.
 Clearly more relevant is ``sequence'' instead of ``set,'' which would
 rephrase Isabelle's internal tactic concept.
 ›


type_synonym ('o, 'σ) MON_SB = "'σ ==> ('o × 'σ) set"

definition bind_SB :: "('o, 'σ)MON_SB ==> ('o ==> ('o', 'σ)MON_SB) ==> ('o', 'σ)MON_SB"
where     "bind_SB f g σ = ∪ ((λ(out, σ). (g out σ)) ` (f σ))"
notation   bind_SB (‹bind_SB›)

definition unit_SB   :: "'o ==> ('o, 'σ)MON_SB" (‹(returns _)› 8) 
where     "unit_SB e = (λσ. {(e,σ)})"
notation   unit_SB (‹unit_SB›)

syntax "_bind_SB" :: "[pttrn,('o,'σ)MON_SB,('o','σ)MON_SB] ==> ('o','σ)MON_SB" 
                                                                         (‹(2 _ := _; _)› [5,8,8]8)
syntax_consts "_bind_SB" ⇌ bind_SB
translations
          "x := f; g" ⇌ "CONST bind_SB f (% x . g)"

lemma bind_left_unit_SB : "(x := returns a; m) = m"
  apply (rule ext)
  apply (simp add: unit_SB_def bind_SB_def)
  done

lemma bind_right_unit_SB: "(x := m; returns x) = m"
  apply (rule ext)
  apply (simp add: unit_SB_def bind_SB_def)
done

lemma bind_assoc_SB: "(y := (x := m; k); h) = (x := m; (y := k; h))"
  apply (rule ext)
  apply (simp add: unit_SB_def bind_SB_def split_def)
done

subsubsection‹State Backtrack Exception Monad›
text‹
 The following combination of the previous two Monad-Constructions allows for the semantic
 foundation of a simple generic assertion language in the style of Schirmer's Simpl-Language or
 Rustan Leino's Boogie-PL language. The key is to use the exceptional element None for violations
 of the assert-statement.
 ›
type_synonym  ('o, 'σ) MON_SBE = "'σ ==> (('o × 'σ) set) option"
      
definition bind_SBE :: "('o,'σ)MON_SBE ==> ('o ==> ('o','σ)MON_SBE) ==> ('o','σ)MON_SBE" 
where     "bind_SBE f g = (λσ. case f σ of None ==> None
                                         | Some S ==> (let S' = (λ(out, σ'). g out σ') ` S
                                                      in if None ∈ S' then None
                                                          else Some(∪ (the ` S'))))"

syntax "_bind_SBE" :: "[pttrn,('o,'σ)MON_SBE,('o','σ)MON_SBE] ==> ('o','σ)MON_SBE" 
                                                                         (‹(2 _ :≡ _; _)› [5,8,8]8)
syntax_consts "_bind_SBE" ⇌ bind_SBE
translations
          "x :≡ f; g" ⇌ "CONST bind_SBE f (% x . g)"

definition unit_SBE   :: "'o ==> ('o, 'σ)MON_SBE"   (‹(returning _)› 8) 
where     "unit_SBE e = (λσ. Some({(e,σ)}))"

definition assert_SBE   :: "('σ ==> bool) ==> (unit, 'σ)MON_SBE"
where     "assert_SBE e = (λσ. if e σ then Some({((),σ)})
                                      else None)"
notation   assert_SBE (‹assert_SBE›)

definition assume_SBE :: "('σ ==> bool) ==> (unit, 'σ)MON_SBE"
where     "assume_SBE e = (λσ. if e σ then Some({((),σ)})
                                      else Some {})"
notation   assume_SBE (‹assume_SBE›)

definition havoc_SBE :: " (unit, 'σ)MON_SBE"
where     "havoc_SBE = (λσ. Some({x. True}))"
notation   havoc_SBE (‹havoc_SBE›)

lemma bind_left_unit_SBE : "(x :≡ returning a; m) = m"
  apply (rule ext)
  apply (simp add: unit_SBE_def bind_SBE_def)
  done

lemma bind_right_unit_SBE: "(x :≡ m; returning x) = m"
  apply (rule ext)
  apply (simp add: unit_SBE_def bind_SBE_def)
  subgoal for x 
    apply (case_tac "m x")
     apply (simp_all add:Let_def)
    apply (rule HOL.ccontr)
    apply (simp add: Set.image_iff)
    done
  done 
   
lemmas aux = trans[OF HOL.neq_commute,OF Option.not_None_eq]

lemma bind_assoc_SBE: "(y :≡ (x :≡ m; k); h) = (x :≡ m; (y :≡ k; h))"
proof (rule ext, simp add: unit_SBE_def bind_SBE_def, rename_tac x,
    case_tac "m x", simp_all add: Let_def Set.image_iff, safe,goal_cases)
  case (1 x a aa b ab ba a b)
  then show ?case  by(rule_tac x="(a, b)" in bexI, simp_all)
next
  case (2 x a aa b ab ba)
  then show ?case  
    apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def)
    apply (erule_tac x="(aa,b)" in ballE)
     apply (auto simp: aux image_def split_def intro!: rev_bexI)
    done
next
  case (3 x a a b)
  then show ?case  by(rule_tac x="(a, b)" in bexI, simp_all)
next
  case (4 x a aa b)
  then show ?case 
    apply (erule_tac Q="None = X" for X in contrapos_pp)
    apply (erule_tac x="(aa,b)" and P="λ x. None ≠ case_prod (λout. k) x" in ballE)
     apply (auto simp: aux image_def split_def intro!: rev_bexI)
    done
next
  case (5 x a aa b ab ba a b)
  then show ?case  apply simp apply ((erule_tac x="(ab,ba)" in ballE)+)
       apply (simp_all add: aux, (erule exE)+, simp add:split_def)
    apply (erule rev_bexI, case_tac "None∈(λp. h(snd p))`y",auto simp:split_def)
    done
      
next
  case (6 x a aa b a b)
  then show ?case    apply simp apply ((erule_tac x="(a,b)" in ballE)+)
       apply (simp_all add: aux, (erule exE)+, simp add:split_def)
    apply (erule rev_bexI, case_tac "None∈(λp. h(snd p))`y",auto simp:split_def)
    done
qed 
  
  

subsection‹Valid Test Sequences in the State Exception Monad›
text‹
 This is still an unstructured merge of executable monad concepts and specification oriented
 high-level properties initiating test procedures.
 ›

definition valid_SE :: "'σ ==> (bool,'σ) MON_SE ==> bool" (infix ‹⊨› 15)
where "(σ ⊨ m) = (m σ ≠ None ∧ fst(the (m σ)))"
text‹
 This notation consideres failures as valid---a definition inspired by I/O conformance.
 Note that it is not possible to define this concept once and for all in a Hindley-Milner
 type-system. For the moment, we present it only for the state-exception monad, although for
 the same definition, this notion is applicable to other monads as well.
 ›

lemma syntax_test : 
  "σ ⊨ (os ← (mbind ιs ioprog); return(length ιs = length os))"
oops


lemma valid_true[simp]: "(σ ⊨ (s ← return x ; return (P s))) = P x"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def)

text‹Recall mbind\_unit for the base case.›

lemma valid_failure: "ioprog a σ = None ==>
                                   (σ ⊨ (s ← mbind (a#S) ioprog ; M s)) =
                                   (σ ⊨ (M []))"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def)



lemma valid_failure': "A σ = None ==> ¬(σ ⊨ ((s ← A ; M s)))"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def)

lemma valid_successElem: (* atomic boolean Monad "Query Functions" *) 
                         "M σ = Some(f σ,σ) ==> (σ ⊨ M) = f σ"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def )

lemma valid_success:  "ioprog a σ = Some(b,σ') ==>
                                  (σ ⊨ (s ← mbind (a#S) ioprog ; M s)) =
                                  (σ' ⊨ (s ← mbind S ioprog ; M (b#s)))"
  apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
  apply (cases "mbind S ioprog σ'", auto)
  done

lemma valid_success'': "ioprog a σ = Some(b,σ') ==>
                                    (σ ⊨ (s ← mbind (a#S) ioprog ; return (P s))) =
                                    (σ' ⊨ (s ← mbind S ioprog ; return (P (b#s))))"
  apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
  apply (cases "mbind S ioprog σ'")
   apply (simp_all)
  apply (auto)
  done

lemma valid_success':  "A σ = Some(b,σ') ==> (σ ⊨ ((s ← A ; M s))) = (σ' ⊨ (M b))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )

lemma valid_both: "(σ ⊨ (s ← mbind (a#S) ioprog ; return (P s))) =
                         (case ioprog a σ of
                               None ==> (σ ⊨ (return (P [])))
                             | Some(b,σ') ==> (σ' ⊨ (s ← mbind S ioprog ; return (P (b#s)))))"
  apply (case_tac "ioprog a σ")
   apply (simp_all add: valid_failure valid_success'' split: prod.splits)
  done

lemma valid_propagate_1 [simp]: "(σ ⊨ (return P)) = (P)"
  by(auto simp: valid_SE_def unit_SE_def)
    
lemma valid_propagate_2: "σ ⊨ ((s ← A ; M s)) ==> ∃ v σ'. the(A σ) = (v,σ') ∧ σ' ⊨ (M v)"
  apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
  apply (cases "A σ")
   apply (simp_all)
  apply (drule_tac x="A σ" and f=the in arg_cong)
  apply (simp) 
  apply (rename_tac a b aa )
  apply (rule_tac x="fst aa" in exI)
  apply (rule_tac x="snd aa" in exI)
  by (auto)          
       
lemma valid_propagate_2': "σ ⊨ ((s ← A ; M s)) ==> ∃ a. (A σ) = Some a ∧ (snd a) ⊨ (M (fst a))"
  apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
  apply (cases "A σ")
   apply (simp_all)
  apply (simp_all split: prod.splits)
  apply (drule_tac x="A σ" and f=the in arg_cong)
  apply (simp)
  apply (rename_tac a b aa x1 x2)
  apply (rule_tac x="fst aa" in exI)
  apply (rule_tac x="snd aa" in exI)
  apply (auto)
  done

lemma valid_propagate_2'': "σ ⊨ ((s ← A ; M s)) ==> ∃ v σ'. A σ = Some(v,σ') ∧ σ' ⊨ (M v)"
  apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
  apply (cases "A σ")
   apply (simp_all)
  apply (drule_tac x="A σ" and f=the in arg_cong)
  apply (simp)
  apply (rename_tac a b aa )
  apply (rule_tac x="fst aa" in exI)
  apply (rule_tac x="snd aa" in exI)
  apply (auto)
  done

lemma valid_propoagate_3[simp]: "(σ₀ ⊨ (λσ. Some (f σ, σ))) = (f σ₀)"
  by(simp add: valid_SE_def )

lemma valid_propoagate_3'[simp]: "¬(σ₀ ⊨ (λσ. None))"
  by(simp add: valid_SE_def )

lemma assert_disch1 :" P σ ==> (σ ⊨ (x ← assert_SE P; M x)) = (σ ⊨ (M True))"
  by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch2 :" ¬ P σ ==> ¬ (σ ⊨ (x ← assert_SE P ; M s))"
  by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch3 :" ¬ P σ ==> ¬ (σ ⊨ (assert_SE P))"
  by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_D : "(σ ⊨ (x ← assert_SE P; M x)) ==> P σ ∧ (σ ⊨ (M True))"
  by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)
    
lemma assume_D : "(σ ⊨ (x ← assume_SE P; M x)) ==> ∃ σ. (P σ ∧ σ ⊨ (M ()))"
  apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm)
  apply (rule_tac x="Eps P" in exI)
  apply (auto)[1]
  subgoal for x a b 
    apply (rule_tac x="True" in exI, rule_tac x="b" in exI)
    apply (subst Hilbert_Choice.someI)
     apply (assumption)
    apply (simp)
    done
  apply (subst Hilbert_Choice.someI,assumption)
  apply (simp)
  done

text‹
 These two rule prove that the SE Monad in connection with the notion of valid sequence is
 actually sufficient for a representation of a Boogie-like language. The SBE monad with explicit
 sets of states---to be shown below---is strictly speaking not necessary (and will therefore
 be discontinued in the development).
 ›
  
lemma if_SE_D1 : "P σ ==> (σ ⊨ if_SE P B₁ B₂) = (σ ⊨ B₁)"
  by(auto simp: if_SE_def valid_SE_def)
    
lemma if_SE_D2 : "¬ P σ ==> (σ ⊨ if_SE P B₁ B₂) = (σ ⊨ B₂)"
  by(auto simp: if_SE_def valid_SE_def)
    
lemma if_SE_split_asm : " (σ ⊨ if_SE P B₁ B₂) = ((P σ ∧ (σ ⊨ B₁)) ∨ (¬ P σ ∧ (σ ⊨ B₂)))"
  by(cases "P σ",auto simp: if_SE_D1 if_SE_D2)
    
lemma if_SE_split : " (σ ⊨ if_SE P B₁ B₂) = ((P σ ⟶ (σ ⊨ B₁)) ∧ (¬ P σ ⟶ (σ ⊨ B₂)))"
  by(cases "P σ", auto simp: if_SE_D1 if_SE_D2)
    
lemma [code]: "(σ ⊨ m) = (case (m σ) of None ==> False | (Some (x,y)) ==> x)"
  apply (simp add: valid_SE_def)
  apply (cases "m σ = None")
   apply (simp_all)
  apply (insert not_None_eq)
  apply (auto)
  done
    
subsection‹Valid Test Sequences in the State Exception Backtrack Monad›
text‹
 This is still an unstructured merge of executable monad concepts and specification oriented
 high-level properties initiating test procedures.
 ›
  
definition valid_SBE :: "'σ ==> ('a,'σ) MON_SBE ==> bool" (infix ‹⊨_SBE› 15)
  where "σ ⊨_SBE m ≡ (m σ ≠ None)"
text‹
 This notation considers all non-failures as valid.
 ›
  
lemma assume_assert: "(σ ⊨_SBE ( _ :≡ assume_SBE P ; assert_SBE Q)) = (P σ ⟶ Q σ)" 
  by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
    
lemma assert_intro: "Q σ ==> σ ⊨_SBE (assert_SBE Q)"
  by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
    
    
end