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]: "(σ⇩0 ⊨ (λσ. Some (f σ, σ))) = (f σ⇩0)"
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]: "¬(σ⇩0 ⊨ (λσ. 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)

text‹versions suited for rewriting› 
lemma exec_mbindFStop_success':‹ioprog a σ ≠ None ⟹ 
        (σ  ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (a#S) ioprog ; M s)) = 
        ((snd o the)(ioprog a σ) ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p S ioprog ; M ((fst o the)(ioprog a σ)#s)))›
  using exec_mbindFStop_success by fastforce

lemma exec_mbindFSave_success': ‹ioprog a σ ≠ None ⟹ 
   (σ  ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e (a#S) ioprog ; M s)) = 
   ((snd o the)(ioprog a σ) ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e S ioprog ; M ((fst o the)(ioprog a σ)#s)))›
  using exec_mbindFSave_success by fastforce

lemma exec_mbindFPurge_success' : 
"ioprog a σ  ≠ None ⟹ 
   (σ  ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩P⇩u⇩r⇩g⇩e (a#S) ioprog ; M s)) = 
   ((snd o the)(ioprog a σ) ⊨ (s ← mbind⇩F⇩a⇩i⇩l⇩P⇩u⇩r⇩g⇩e S ioprog ; M ((fst o the)(ioprog a σ)#s)))"
  using exec_mbindFPurge_success by fastforce

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⇩1 else B⇩2 fi"

lemma if_SE_D1 : "P σ ⟹ (σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi)) = (σ ⊨ B⇩1)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D1' : "P σ ⟹ (σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi);-M) = (σ ⊨ (B⇩1;-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⇩1 else B⇩2 fi)) = (σ ⊨ B⇩2)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D2' : "¬ P σ ⟹ (σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi);-M) = (σ ⊨ B⇩2;-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⇩1 else B⇩2 fi)) = ((P σ ∧ (σ ⊨ B⇩1)) ∨ (¬ P σ ∧ (σ ⊨ B⇩2)))"
by(cases "P σ",auto simp: if_SE_D1 if_SE_D2)

lemma if_SE_split_asm': 
"(σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi);-M) = ((P σ ∧ (σ ⊨ B⇩1;-M)) ∨ (¬ P σ ∧ (σ ⊨ B⇩2;-M)))"
by(cases "P σ",auto simp: if_SE_D1' if_SE_D2')


lemma if_SE_split: 
"(σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi)) = ((P σ ⟶ (σ ⊨ B⇩1)) ∧ (¬ P σ ⟶ (σ ⊨ B⇩2)))"
by(cases "P σ", auto simp: if_SE_D1 if_SE_D2)


lemma if_SE_split': 
"(σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 fi);-M) = ((P σ ⟶ (σ ⊨ B⇩1;-M)) ∧ (¬ P σ ⟶ (σ ⊨ B⇩2;-M)))"
by(cases "P σ", auto simp: if_SE_D1' if_SE_D2')

lemma if_SE_execE:
  assumes A: "σ ⊨ ((if⇩S⇩E P then B⇩1 else B⇩2 fi))"
   and   B: "P σ  ⟹ σ ⊨ (B⇩1) ⟹ Q"
   and   C: "¬ P σ⟹ σ ⊨ (B⇩2) ⟹ 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⇩1 else B⇩2 fi);-M)"
   and   B: "P σ  ⟹ σ ⊨ (B⇩1;-M) ⟹ Q"
   and   C: "¬ P σ⟹ σ ⊨ (B⇩2;-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⇩1 else B⇩2 fi) ;- M 
⟹ (P σ ⟹ σ ⊨ B⇩1 ;- M ⟹ Q) 
⟹ (¬ P σ ⟹ σ ⊨ B⇩2 ;- 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⇩1 else B⇩2 fi) ;- M 
⟹ (P σ ⟹ σ ⊨ B⇩1 ;- M ⟹ Q) 
⟹ (opaque (σ ⊨ (if⇩S⇩E P then B⇩1 else B⇩2 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 σ⇩1. (σ ⊨ (_  ← assume⇩S⇩E (λσ'. (σ=σ') ∧  P σ) ; x  ← M; 
                      assert⇩S⇩E (λσ.  (x=X) ∧ (σ=σ⇩1) ∧ Q x σ)))
               ∧ 
               (σ⇩1 ⊨ (_  ← assume⇩S⇩E (λσ.  (σ=σ⇩1) ∧ 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  by (meson C exec_mbindFSave_success' exec_mbindFStop_success' 
                             list.set_intros(1) list.set_intros(2) valid_bind_cong)
qed


text‹Symbolic execution rules for assertions.›
lemma assert_suffix_seq : 
              "σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p xs iostep; assert⇩S⇩E (P)) 
               ⟹ ∀σ. P σ ⟶ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p ys iostep; assert⇩S⇩E (Q))) 
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (xs @ ys) iostep; assert⇩S⇩E (Q))"
apply(subst mbind'_concat)
unfolding bind_SE_def assert_SE_def valid_SE_def
  apply(auto split: option.split option.split_asm, rename_tac "aa" "ba" "ab" "bb" )
  apply (metis option.distinct(1))
  by (meson option.distinct(1))

lemma assert_suffix_seq2 : 
              "σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p xs iostep; assert⇩S⇩E (P)) 
               ⟹ (⋀ σ. P σ ⟹ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p ys iostep; assert⇩S⇩E (Q))))
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (xs @ ys) iostep; assert⇩S⇩E (Q))"
  by (simp add: assert_suffix_seq)

lemma assert_suffix_seq_map : 
              "σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (map f xs) iostep; assert⇩S⇩E (P)) 
               ⟹ (⋀ σ. P σ ⟹ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (map f ys) iostep; assert⇩S⇩E (Q))))
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (map f (xs @ ys)) iostep; assert⇩S⇩E (Q))"
  by (simp add: assert_suffix_seq)


lemma assert_suffix_seq_tot : 
              "∀x σ. iostep x σ ≠ None 
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e xs iostep; assert⇩S⇩E (P)) 
               ⟹ ∀σ. P σ ⟶ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p ys iostep; assert⇩S⇩E (Q)))
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e (xs @ ys) iostep; assert⇩S⇩E (Q))"
  apply(subst Symbex_MonadSE.mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e_vs_mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p, simp)
  apply(subst (asm) Symbex_MonadSE.mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e_vs_mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p, simp)
  by (simp add: assert_suffix_seq)

lemma assert_suffix_seq_tot2 : 
              "(⋀ x σ. iostep x σ ≠ None)
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e xs iostep; assert⇩S⇩E (P)) 
               ⟹ (⋀σ. P σ ⟹ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p ys iostep; assert⇩S⇩E (Q))))
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e (xs @ ys) iostep; assert⇩S⇩E (Q))"
  by (simp add: assert_suffix_seq_tot)


lemma assert_suffix_seq_tot3 : 
              "(⋀ x σ. iostep x σ ≠ None)
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e (map f xs) iostep; assert⇩S⇩E (P)) 
               ⟹ (⋀σ. P σ ⟹ (σ ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (map f ys) iostep; assert⇩S⇩E (Q))))
               ⟹ σ ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩a⇩v⇩e (map f (xs @ ys)) iostep; assert⇩S⇩E (Q))"
  by (simp add: assert_suffix_seq_tot)


lemma assert_disch : 
   "(σ ⊨ (_ ← iostep x; assert⇩S⇩E (Q))) = 
    (case iostep x σ of None ⇒ False | Some(_,σ') ⇒ Q σ')"
  by (smt (verit, best) assert_simp bind_SE_def option.case_eq_if split_def valid_SE_def)

lemma assert_disch_tot :
   "∀x σ. iostep x σ ≠ None ⟹ (σ ⊨ (_ ← iostep x; assert⇩S⇩E (Q))) = (Q (snd(the(iostep x σ))))"
  apply(subst assert_disch)
  by (metis option.case_eq_if split_beta')

lemma assert_disch_tot2 :
   "(⋀x σ. iostep x σ ≠ None) ⟹ (σ ⊨ (_ ← iostep x; assert⇩S⇩E (Q))) = (Q (snd(the(iostep x σ))))"
  apply(subst assert_disch)
  by (metis option.case_eq_if split_beta')

lemma mbind_total_if_step_total  :
   "(⋀x σ. x ∈ set S ⟹ iostep x σ ≠ None) ⟹  (⋀σ. mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p S iostep σ ≠ None)"
proof(induct S)
  case Nil
  then show ?case by (simp add: unit_SE_def) 
next
  case (Cons a S σ)
  have 1 : "∀ x σ. x ∈ set S ⟶ iostep x σ ≠ None" 
    by (simp add: Cons.prems)
  have 2 : "⋀σ. mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p S iostep σ ≠ None" 
    using Cons.hyps Cons.prems by fastforce
  then show ?case  
    apply(simp add : mbind'.simps(2) 1 2) 
    by (simp add: "2" Cons.prems option.case_eq_if split_beta')
qed

subsection‹Miscellaneous›

no_notation unit_SE (‹(result _)› 8)

end