Theory Symbex_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 Symbex_MonadSE
  imports Seq_MonadSE
begin
  


subsection‹Definition and Properties of Valid Execution Sequences›

text‹A key-notion in our framework is the \emph{valid} execution
sequence, \ie{} a sequence that:
\begin{enumerate}
\item terminates (not obvious since while),
\item results in a final @{term True},
\item does not fail globally (but recall the FailSave and FailPurge
      variants of @{term mbind}-operators, that handle local exceptions in
      one or another way).
\end{enumerate}
Seen from an automata perspective (where the monad - operations correspond to
the step function), valid execution sequences can be used to model ``feasible paths''
across an automaton.›

definition valid_SE :: "'σ ⇒ (bool,'σ) MON⇩_S⇩_E ⇒ bool" (infix "⊨" 9)
where "(σ ⊨ m) = (m σ ≠ None ∧ fst(the (m σ)))"
text‹This notation consideres failures as valid -- a definition
inspired by I/O conformance.›

subsubsection‹Valid Execution Sequences and their Symbolic Execution›
lemma exec_unit_SE [simp]: "(σ ⊨ (result P)) = (P)"
by(auto simp: valid_SE_def unit_SE_def)

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

lemma exec_fail_SE [simp]: "(σ ⊨ fail⇩_S⇩_E) = False"
by(auto simp: valid_SE_def fail_SE_def)

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

text‹The following the rules are in a sense the heart of the entire symbolic execution approach›
lemma  exec_bind_SE_failure:
"A σ = None ⟹ ¬(σ ⊨ ((s ← A ; M s)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)

lemma  exec_bind_SE_failure2:
"A σ = None ⟹ ¬(σ ⊨ ((A ;- M)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def)
  
  
lemma exec_bind_SE_success: 
"A σ = Some(b,σ') ⟹ (σ ⊨ ((s ← A ; M s))) = (σ' ⊨ (M b))"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def )
    
lemma exec_bind_SE_success2: 
"A σ = Some(b,σ') ⟹ (σ ⊨ ((A ;- M))) = (σ' ⊨ M)"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def )
    

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




lemma exec_bind_SE_success'':
"σ ⊨ ((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 σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma exec_bind_SE_success''':
"σ ⊨ ((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 σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma  exec_bind_SE_success'''' :
"σ ⊨ ((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 σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma valid_bind_cong : " f σ = g σ ⟹ (σ ⊨ (x ← f ; M x)) = (σ ⊨ (x ← g ; M x))"
  unfolding bind_SE'_def bind_SE_def valid_SE_def
    by simp
  
lemma valid_bind'_cong : " f σ = g σ ⟹ (σ ⊨ f ;- M) = (σ ⊨ g ;- M)"
  unfolding bind_SE'_def bind_SE_def valid_SE_def
    by simp


text‹Recall \verb+mbind_unit+ for the base case.›

lemma valid_mbind_mt : "(σ ⊨ ( s ←  mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e [] f; unit⇩_S⇩_E (P s))) = P [] " by simp
lemma valid_mbind_mtE: "σ ⊨ ( s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e [] f; unit⇩_S⇩_E (P s)) ⟹ (P [] ⟹ Q) ⟹ Q"
by(auto simp: valid_mbind_mt)

lemma valid_mbind'_mt : "(σ ⊨ ( s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p [] f; unit⇩_S⇩_E (P s))) = P [] " by simp
lemma valid_mbind'_mtE: "σ ⊨ ( s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p [] f; unit⇩_S⇩_E (P s)) ⟹ (P [] ⟹ Q) ⟹ Q"
by(auto simp: valid_mbind'_mt)

lemma valid_mbind''_mt : "(σ ⊨ ( s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e [] f; unit⇩_S⇩_E (P s))) = P [] " 
by(simp add: mbind''.simps valid_SE_def bind_SE_def unit_SE_def)
lemma valid_mbind''_mtE: "σ ⊨ ( s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e [] f; unit⇩_S⇩_E (P s)) ⟹ (P [] ⟹ Q) ⟹ Q"
by(auto simp: valid_mbind''_mt)


lemma exec_mbindFSave_failure: 
"ioprog a σ = None ⟹ 
   (σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e (a#S) ioprog ; M s)) =  (σ ⊨ (M []))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)

lemma exec_mbindFStop_failure: 
"ioprog a σ = None ⟹ 
   (σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p (a#S) ioprog ; M s)) =  (False)"
by(simp add: exec_bind_SE_failure)

lemma exec_mbindFPurge_failure: 
"ioprog a σ = None ⟹ 
   (σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e (a#S) ioprog ; M s)) = 
   (σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e (S) ioprog ; M s))" 
by(simp add: valid_SE_def unit_SE_def bind_SE_def mbind''.simps)


lemma exec_mbindFSave_success : 
"ioprog a σ = Some(b,σ') ⟹ 
   (σ  ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e (a#S) ioprog ; M s)) = 
   (σ' ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e S ioprog σ'", auto)

lemma exec_mbindFStop_success : 
"ioprog a σ = Some(b,σ') ⟹ 
   (σ  ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p (a#S) ioprog ; M s)) = 
   (σ' ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S ioprog σ'", auto simp:  mbind'.simps)

lemma exec_mbindFPurge_success : 
"ioprog a σ = Some(b,σ') ⟹ 
   (σ  ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e (a#S) ioprog ; M s)) = 
   (σ' ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e S ioprog σ'", auto simp:  mbind''.simps)

lemma exec_mbindFSave:
"(σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e  (a#S) ioprog ; return (P s))) =
    (case ioprog a σ of
       None ⇒ (σ  ⊨ (return (P [])))
     | Some(b,σ') ⇒ (σ'  ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e  S ioprog ; return (P (b#s)))))"
apply(case_tac "ioprog a σ")
apply(auto simp: exec_mbindFSave_failure  exec_mbindFSave_success split: prod.splits)
done

lemma mbind_eq_sexec: 
assumes * : "⋀b σ'. f a σ = Some(b,σ') ⟹ 
             (os ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S f; P (b#os)) = (os ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S f; P' (b#os))"
shows       "( a ← f a;  x ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S f; P (a # x)) σ = 
             ( a ← f a;  x ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S f; P'(a # x)) σ"
  apply(cases "f a σ = None")
  apply(subst bind_SE_def, simp)
 apply(subst bind_SE_def, simp)
 apply auto
 apply(subst bind_SE_def, simp)
 apply(subst bind_SE_def, simp)
apply(simp add: *)
done


lemma mbind_eq_sexec': 
assumes * : "⋀b σ'. f a σ = Some(b,σ') ⟹ 
             (P (b))σ' = (P' (b))σ'"
shows       "( a ← f a;  P (a)) σ = 
             ( a ← f a;  P'(a)) σ"
 apply(cases "f a σ = None")
   apply(subst bind_SE_def, simp)
  apply(subst bind_SE_def, simp)
  apply auto
  apply(subst bind_SE_def, simp)
  apply(subst bind_SE_def, simp)
 apply(simp add: *)
done

lemma mbind'_concat:
"(os ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p (S@T) f; P os) = (os ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S f; os' ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p T f; P (os @ os'))"
proof (rule ext, rename_tac "σ", induct S arbitrary: σ P) 
   case Nil show ?case by simp
next
   case (Cons a S) show ?case 
        apply(insert Cons.hyps, simp)
        by(rule mbind_eq_sexec',simp)
qed

lemma assert_suffix_inv : 
              "σ ⊨ ( _ ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p xs istep; assert⇩_S⇩_E (P)) 
               ⟹ ∀σ. P σ ⟶ (σ ⊨ (_ ← istep x; assert⇩_S⇩_E (P)))
               ⟹ σ ⊨ ( _ ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p (xs @ [x]) istep; assert⇩_S⇩_E (P))"
apply(subst mbind'_concat, simp)
unfolding bind_SE_def assert_SE_def valid_SE_def
apply(auto split: option.split option.split_asm)
apply(case_tac "aa",simp_all)
apply(case_tac "P bb",simp_all)
apply (metis option.distinct(1))
apply(case_tac "aa",simp_all)
apply(case_tac "P bb",simp_all)
by (metis option.distinct(1))



text‹Universal splitting and symbolic execution rule›
lemma exec_mbindFSave_E:
assumes seq : "(σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e (a#S) ioprog ;  (P s)))"
  and   none: "ioprog a σ = None ⟹ (σ ⊨ (P [])) ⟹ Q"
  and   some: "⋀ b σ'. ioprog a σ = Some(b,σ') ⟹ (σ' ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e S ioprog;(P (b#s)))) ⟹ Q "
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(rule none[OF ass])
        apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFSave_failure[THEN iffD1],rule seq)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFSave_success[THEN iffD1],rule seq)
        done
qed

text‹The next rule reveals the particular interest in deduction;
       as an elimination rule, it allows for a linear conversion of a validity judgement
       @{term "mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p"} over an input list @{term "S"} into a constraint system; without any 
       branching ... Symbolic execution can even be stopped tactically whenever 
       @{term "ioprog a σ = Some(b,σ')"} comes to a contradiction.›
lemma exec_mbindFStop_E:
assumes seq : "(σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p (a#S) ioprog ; (P s)))"
  and   some: "⋀b σ'. ioprog a σ = Some(b,σ') ⟹ (σ'⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p S ioprog;(P(b#s)))) ⟹ Q"
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(insert ass seq)
        apply(drule_tac σ=σ and S=S and M=P in exec_mbindFStop_failure, simp)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFStop_success[THEN iffD1],rule seq)
        done
qed


lemma exec_mbindFPurge_E:
assumes seq : "(σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e (a#S) ioprog ;  (P s)))"
  and   none: "ioprog a σ = None ⟹ (σ ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e S ioprog;(P (s)))) ⟹ Q"
  and   some: "⋀ b σ'. ioprog a σ = Some(b,σ') ⟹ (σ' ⊨ (s ← mbind⇩_F⇩_a⇩_i⇩_l⇩_P⇩_u⇩_r⇩_g⇩_e S ioprog;(P (b#s)))) ⟹ Q "
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(rule none[OF ass])
        apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFPurge_failure[THEN iffD1],rule seq)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFPurge_success[THEN iffD1],rule seq)
        done
qed


lemma assert_disch1 :" P σ ⟹ (σ ⊨ (x ← assert⇩_S⇩_E P; M x)) = (σ ⊨ (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch2 :" ¬ P σ ⟹ ¬ (σ ⊨ (x ← assert⇩_S⇩_E P ; M s))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch3 :" ¬ P σ ⟹ ¬ (σ ⊨ (assert⇩_S⇩_E P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch4 :" P σ ⟹  (σ ⊨ (assert⇩_S⇩_E P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_simp : "(σ ⊨ assert⇩_S⇩_E P) = P σ"
by (meson assert_disch3 assert_disch4)

lemmas assert_D = assert_simp[THEN iffD1]  (* legacy *)

lemma assert_bind_simp : "(σ ⊨ (x ← assert⇩_S⇩_E P; M x)) = (P σ ∧ (σ ⊨ (M True)))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)

lemmas assert_bindD = assert_bind_simp[THEN iffD1]  (* legacy *)


lemma assume_D : "(σ ⊨ (_ ← assume⇩_S⇩_E P; M)) ⟹ ∃ σ. (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, auto)
apply(subst Hilbert_Choice.someI,assumption,simp)
done


lemma assume_E :
assumes *  : "σ ⊨ ( _ ← assume⇩_S⇩_E P; M) "
and     ** : "⋀ σ. P σ ⟹ σ ⊨ M  ⟹ Q"
shows  "Q"
apply(insert *)
by(insert *[THEN assume_D], auto intro: **)

lemma assume_E' :
assumes *  : "σ ⊨ assume⇩_S⇩_E P ;- M"
and     ** : "⋀ σ. P σ ⟹ σ ⊨ M  ⟹ Q"
shows  "Q"
by(insert *[simplified "bind_SE'_def", THEN assume_D], auto intro: **)


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).›

term "if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi"

lemma if_SE_D1 : "P σ ⟹ (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi)) = (σ ⊨ B⇩₁)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D1' : "P σ ⟹ (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M) = (σ ⊨ (B⇩₁;-M))"
by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def)


lemma if_SE_D2 : "¬ P σ ⟹ (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi)) = (σ ⊨ B⇩₂)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D2' : "¬ P σ ⟹ (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M) = (σ ⊨ B⇩₂;-M)"
by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def)


lemma if_SE_split_asm : 
"(σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi)) = ((P σ ∧ (σ ⊨ B⇩₁)) ∨ (¬ P σ ∧ (σ ⊨ B⇩₂)))"
by(cases "P σ",auto simp: if_SE_D1 if_SE_D2)

lemma if_SE_split_asm': 
"(σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M) = ((P σ ∧ (σ ⊨ B⇩₁;-M)) ∨ (¬ P σ ∧ (σ ⊨ B⇩₂;-M)))"
by(cases "P σ",auto simp: if_SE_D1' if_SE_D2')


lemma if_SE_split: 
"(σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi)) = ((P σ ⟶ (σ ⊨ B⇩₁)) ∧ (¬ P σ ⟶ (σ ⊨ B⇩₂)))"
by(cases "P σ", auto simp: if_SE_D1 if_SE_D2)


lemma if_SE_split': 
"(σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M) = ((P σ ⟶ (σ ⊨ B⇩₁;-M)) ∧ (¬ P σ ⟶ (σ ⊨ B⇩₂;-M)))"
by(cases "P σ", auto simp: if_SE_D1' if_SE_D2')

lemma if_SE_execE:
  assumes A: "σ ⊨ ((if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi))"
   and   B: "P σ  ⟹ σ ⊨ (B⇩₁) ⟹ Q"
   and   C: "¬ P σ⟹ σ ⊨ (B⇩₂) ⟹ Q"
  shows  "Q"
by(insert A [simplified if_SE_split],cases  "P σ", simp_all, auto elim: B C)


lemma if_SE_execE':
  assumes A: "σ ⊨ ((if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M)"
   and   B: "P σ  ⟹ σ ⊨ (B⇩₁;-M) ⟹ Q"
   and   C: "¬ P σ⟹ σ ⊨ (B⇩₂;-M) ⟹ Q"
  shows  "Q"
by(insert A [simplified if_SE_split'],cases  "P σ", simp_all, auto elim: B C)


lemma exec_while : 
"(σ ⊨ ((while⇩_S⇩_E b do c od) ;- M)) = 
 (σ ⊨ ((if⇩_S⇩_E b then c ;- (while⇩_S⇩_E b do c od) else unit⇩_S⇩_E ()fi) ;- M))"
apply(subst while_SE_unfold)
by(simp add: bind_SE'_def )

lemmas exec_whileD = exec_while[THEN iffD1]

lemma if_SE_execE'':
"σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi) ;- M 
⟹ (P σ ⟹ σ ⊨ B⇩₁ ;- M ⟹ Q) 
⟹ (¬ P σ ⟹ σ ⊨ B⇩₂ ;- M ⟹ Q) 
⟹ Q"
by(auto elim: if_SE_execE')

definition "opaque (x::bool) = x"
lemma if_SE_execE''_pos:
"σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi) ;- M 
⟹ (P σ ⟹ σ ⊨ B⇩₁ ;- M ⟹ Q) 
⟹ (opaque (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi) ;- M) ⟹ Q) 
⟹ Q"
using opaque_def by auto


lemma [code]:
  "(σ ⊨ m) = (case (m σ) of None  ⇒ False | (Some (x,y))  ⇒ x)"
  apply(simp add: valid_SE_def)
  apply(cases "m σ = None", simp_all) 
  apply(insert not_None_eq, auto)
done

    
(* for the moment no good idea to state the case where the body eventually crashes. *)
lemma "P  σ ⊨ (_  ← assume⇩_S⇩_E P ; x  ← M; assert⇩_S⇩_E (λσ.  (x=X) ∧ Q x σ))"
oops

lemma "∀σ. ∃ X. σ ⊨ (_  ← assume⇩_S⇩_E P ; x  ← M; assert⇩_S⇩_E (λσ.  x=X ∧ Q x σ))"
oops


lemma monadic_sequence_rule:
      "⋀ X σ⇩₁. (σ ⊨ (_  ← assume⇩_S⇩_E (λσ'. (σ=σ') ∧  P σ) ; x  ← M; assert⇩_S⇩_E (λσ.  (x=X) ∧ (σ=σ⇩₁) ∧ Q x σ)))
               ∧ 
               (σ⇩₁ ⊨ (_  ← assume⇩_S⇩_E (λσ.  (σ=σ⇩₁) ∧ Q x σ) ; y  ← M'; assert⇩_S⇩_E (λσ.  R x y σ)))
       ⟹
               σ ⊨ (_  ← assume⇩_S⇩_E (λσ'. (σ=σ') ∧  P σ) ; x  ← M; y  ← M'; assert⇩_S⇩_E (R x y))"
apply(elim exE impE conjE)
apply(drule assume_D) 
apply(elim exE impE conjE)
unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def
apply(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm)
apply (metis (mono_tags, lifting) option.simps(3) someI_ex)
oops


  
lemma "∃ X. σ ⊨ (_  ← assume⇩_S⇩_E P ; x  ← M; assert⇩_S⇩_E (λσ.  x=X ∧ Q x σ))
       ⟹ 
            σ ⊨ (_  ← assume⇩_S⇩_E P ; x  ← M; assert⇩_S⇩_E (λσ. Q x σ))"
unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def
by(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm)


lemma exec_skip:
"(σ ⊨ skip⇩_S⇩_E ;- M) = (σ ⊨ M)"
by (simp add: skip⇩_S⇩_E_def)

lemmas exec_skipD = exec_skip[THEN iffD1]


text‹Test-Refinements will be stated in terms of the failsave @{term mbind}, opting 
       more generality. The following lemma allows for an  optimization both in 
       test execution as well as in symbolic execution for an important special case of
       the post-codition: Whenever the latter has the constraint that the length of input and 
       output sequence equal each other (that is to say: no failure occured), failsave mbind
       can be reduced to failstop mbind ...›
lemma mbindFSave_vs_mbindFStop : 
  "(σ ⊨ (os ← (mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e ιs ioprog); result(length ιs = length os ∧ P ιs os))) = 
   (σ ⊨ (os ← (mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p ιs ioprog); result(P ιs os)))"
  apply(rule_tac x=P in spec)
  apply(rule_tac x=σ in spec)
  proof(induct "ιs") 
     case Nil show ?case by(simp_all add: mbind_try try_SE_def del: Seq_MonadSE.mbind.simps)
     case (Cons a ιs) show ?case
          apply(rule allI, rename_tac "σ",rule allI, rename_tac "P")
          apply(insert Cons.hyps)
          apply(case_tac "ioprog a σ")
          apply(simp only: exec_mbindFSave_failure exec_mbindFStop_failure, simp)
          apply(simp add:  split_paired_all del: Seq_MonadSE.mbind.simps )
          apply(rename_tac "σ'") 
          apply(subst exec_mbindFSave_success, assumption)
          apply(subst (2) exec_bind_SE_success, assumption)
          apply(erule_tac x="σ'" in allE)
          apply(erule_tac x="λιs s. P (a # ιs) (aa # s)" in allE) (* heureka ! *)
          apply(simp)
      done
  qed


lemma mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e_vs_mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p:
assumes A: "∀ ι∈set ιs. ∀ σ. ioprog ι σ ≠ None"
shows      "(σ ⊨ (os ← (mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e ιs ioprog); P os)) = 
            (σ ⊨ (os ← (mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p ιs ioprog); P os))" 
proof(insert A, erule rev_mp, induct "ιs") 
  case Nil show ?case by simp
next 
  case (Cons a ιs) 
       from Cons.hyps                           
       have B:"∀ S f σ. mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e S f σ ≠ None " by simp

       have C:"(∀ ι∈set ιs. ∀ σ. ioprog ι σ ≠ None) 
               ⟶ (∀σ. mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_t⇩_o⇩_p ιs ioprog σ = mbind⇩_F⇩_a⇩_i⇩_l⇩_S⇩_a⇩_v⇩_e ιs ioprog σ)" 
               apply(induct ιs, simp)
               apply(intro impI allI,rename_tac "σ")
               apply(simp add: Seq_MonadSE.mbind'.simps(2))
               apply(insert A, erule_tac x="a" in ballE)
               apply(erule_tac x="σ" and P="λσ . ioprog a σ ≠ None" in allE)
               apply(auto split:option.split)
               done
      show ?case 
        apply(intro impI) 
        by (smt (verit, best) C exec_mbindFSave_E exec_mbindFSave_success exec_mbindFStop_E 
                exec_mbindFStop_success list.set_intros(1) list.set_intros(2) valid_bind_cong)
qed

subsection‹Miscellaneous›

no_notation unit_SE ("(result _)" 8)

end