Theory HoarePartialProps

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2004-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.

*)

section ‹Properties of Partial Correctness Hoare Logic›

theory HoarePartialProps imports HoarePartialDef begin

subsection ‹Soundness›

lemma hoare_cnvalid:
 assumes hoare: "Γ,Θ⊢⇘/F⇙ P c Q,A"
 shows "⋀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
using hoare
proof (induct)
  case (Skip Θ F P A)
  show "Γ,Θ ⊨n:⇘/F⇙ P Skip P,A"
  proof (rule cnvalidI)
    fix s t
    assume "Γ⊢⟨Skip,Normal s⟩ =n⇒ t" "s ∈ P"
    thus "t ∈ Normal ` P ∪ Abrupt ` A"
      by cases auto
  qed
next
  case (Basic Θ F f P A)
  show "Γ,Θ ⊨n:⇘/F⇙ {s. f s ∈ P} (Basic f) P,A"
  proof (rule cnvalidI)
    fix s t
    assume "Γ⊢⟨Basic f,Normal s⟩ =n⇒ t" "s ∈ {s. f s ∈ P}"
    thus "t ∈ Normal ` P ∪ Abrupt ` A"
      by cases auto
  qed
next
  case (Spec Θ F r Q A)
  show "Γ,Θ⊨n:⇘/F⇙ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A"
  proof (rule cnvalidI)
    fix s t
    assume exec: "Γ⊢⟨Spec r,Normal s⟩ =n⇒ t"
    assume P: "s ∈ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)}"
    from exec P
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by cases auto
  qed
next
  case (Seq Θ F P c1 R A c2 Q)
  have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P c1 R,A" by fact
  have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ R c2 Q,A" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P Seq c1 c2 Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Seq c1 c2,Normal s⟩ =n⇒ t"
    assume t_notin_F: "t ∉ Fault ` F"
    assume P: "s ∈ P"
    from exec P obtain r where
      exec_c1: "Γ⊢⟨c1,Normal s⟩ =n⇒ r" and exec_c2:  "Γ⊢⟨c2,r⟩ =n⇒ t"
      by cases auto
    with t_notin_F have "r ∉ Fault ` F"
      by (auto dest: execn_Fault_end)
    with valid_c1 ctxt exec_c1 P
    have r: "r∈Normal ` R ∪ Abrupt ` A"
      by (rule cnvalidD)
    show "t∈Normal ` Q ∪ Abrupt ` A"
    proof (cases r)
      case (Normal r')
      with exec_c2 r
      show "t∈Normal ` Q ∪ Abrupt ` A"
        apply -
        apply (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F])
        apply auto
        done
    next
      case (Abrupt r')
      with exec_c2 have "t=Abrupt r'"
        by (auto elim: execn_elim_cases)
      with Abrupt r show ?thesis
        by auto
    next
      case Fault with r show ?thesis by blast
    next
      case Stuck with r show ?thesis by blast
    qed
  qed
next
  case (Cond Θ F P b c1 Q A c2)
  have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ b) c1 Q,A" by fact
  have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ - b) c2 Q,A" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P Cond b c1 c2 Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Cond b c1 c2,Normal s⟩ =n⇒ t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases "s∈b")
      case True
      with exec have "Γ⊢⟨c1,Normal s⟩ =n⇒ t"
        by cases auto
      with P True
      show ?thesis
        by - (rule cnvalidD [OF valid_c1 ctxt _ _ t_notin_F],auto)
    next
      case False
      with exec P have "Γ⊢⟨c2,Normal s⟩ =n⇒ t"
        by cases auto
      with P False
      show ?thesis
        by - (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F],auto)
    qed
  qed
next
  case (While Θ F P b c A n)
  have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ b) c P,A" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P While b c (P ∩ - b),A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨While b c,Normal s⟩ =n⇒ t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
    proof (cases "s ∈ b")
      case True
      {
        fix d::"('b,'a,'c) com" fix s t
        assume exec: "Γ⊢⟨d,s⟩ =n⇒ t"
        assume d: "d=While b c"
        assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
        from exec d ctxt
        have "⟦s ∈ Normal ` P; t ∉ Fault ` F⟧
               ⟹ t ∈ Normal ` (P ∩ - b) ∪ Abrupt`A"
        proof (induct)
          case (WhileTrue s b' c' n r t)
          have t_notin_F: "t ∉ Fault ` F" by fact
          have eqs: "While b' c' = While b c" by fact
          note valid_c
          moreover have ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A" by fact
          moreover from WhileTrue
          obtain "Γ⊢⟨c,Normal s⟩ =n⇒ r" and
            "Γ⊢⟨While b c,r⟩ =n⇒ t" and
            "Normal s ∈ Normal `(P ∩ b)" by auto
          moreover with t_notin_F have "r ∉ Fault ` F"
            by (auto dest: execn_Fault_end)
          ultimately
          have r: "r ∈ Normal ` P ∪ Abrupt ` A"
            by - (rule cnvalidD,auto)
          from this _ ctxt
          show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A "
          proof (cases r)
            case (Normal r')
            with r ctxt eqs t_notin_F
            show ?thesis
              by - (rule WhileTrue.hyps,auto)
          next
            case (Abrupt r')
            have "Γ⊢⟨While b' c',r⟩ =n⇒ t" by fact
            with Abrupt have "t=r"
              by (auto dest: execn_Abrupt_end)
            with r Abrupt show ?thesis
              by blast
          next
            case Fault with r show ?thesis by blast
          next
            case Stuck with r show ?thesis by blast
          qed
        qed auto
      }
      with exec ctxt P t_notin_F
      show ?thesis
        by auto
    next
      case False
      with exec P have "t=Normal s"
        by cases auto
      with P False
      show ?thesis
        by auto
    qed
  qed
next
  case (Guard Θ F g P c Q A f)
  have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) c Q,A" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) Guard f g c  Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ t"
    assume t_notin_F: "t ∉ Fault ` F"
    assume P:"s ∈ (g ∩ P)"
    from exec P have "Γ⊢⟨c,Normal s⟩ =n⇒ t"
      by cases auto
    from valid_c ctxt this P t_notin_F
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by (rule cnvalidD)
  qed
next
  case (Guarantee f F Θ g P c Q A)
  have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) c Q,A" by fact
  have f_F: "f ∈ F" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P Guard f g c  Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ t"
    assume t_notin_F: "t ∉ Fault ` F"
    assume P:"s ∈ P"
    from exec f_F t_notin_F have g: "s ∈ g"
      by cases auto
    with P have P': "s ∈ g ∩ P"
      by blast
    from exec P g have "Γ⊢⟨c,Normal s⟩ =n⇒ t"
      by cases auto
    from valid_c ctxt this P' t_notin_F
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by (rule cnvalidD)
  qed
next
  case (CallRec P p Q A Specs Θ F)
  have p: "(P,p,Q,A) ∈ Specs" by fact
  have valid_body:
    "∀(P,p,Q,A) ∈ Specs. p ∈ dom Γ ∧ (∀n. Γ,Θ ∪ Specs ⊨n:⇘/F⇙ P (the (Γ p)) Q,A)"
    using CallRec.hyps by blast
  show "Γ,Θ⊨n:⇘/F⇙ P Call p Q,A"
  proof -
    {
      fix n
      have "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A
        ⟹ ∀(P,p,Q,A) ∈Specs. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
      proof (induct n)
        case 0
        show "∀(P,p,Q,A) ∈Specs. Γ⊨0:⇘/F⇙ P (Call p) Q,A"
          by (fastforce elim!: execn_elim_cases simp add: nvalid_def)
      next
        case (Suc m)
        have hyp: "∀(P, p, Q, A)∈Θ. Γ ⊨m:⇘/F⇙ P (Call p) Q,A
              ⟹ ∀(P,p,Q,A) ∈Specs. Γ⊨m:⇘/F⇙ P (Call p) Q,A" by fact
        have "∀(P, p, Q, A)∈Θ. Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A" by fact
        hence ctxt_m: "∀(P, p, Q, A)∈Θ. Γ ⊨m:⇘/F⇙ P (Call p) Q,A"
          by (fastforce simp add: nvalid_def intro: execn_Suc)
        hence valid_Proc:
          "∀(P,p,Q,A) ∈Specs. Γ⊨m:⇘/F⇙ P (Call p) Q,A"
          by (rule hyp)
        let ?Θ'= "Θ ∪ Specs"
        from valid_Proc ctxt_m
        have "∀(P, p, Q, A)∈?Θ'. Γ ⊨m:⇘/F⇙ P (Call p) Q,A"
          by fastforce
        with valid_body
        have valid_body_m:
          "∀(P,p,Q,A) ∈Specs. ∀n. Γ ⊨m:⇘/F⇙ P (the (Γ p)) Q,A"
          by (fastforce simp add: cnvalid_def)
        show "∀(P,p,Q,A) ∈Specs. Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A"
        proof (clarify)
          fix P p Q A assume p: "(P,p,Q,A) ∈ Specs"
          show "Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A"
          proof (rule nvalidI)
            fix s t
            assume exec_call:
              "Γ⊢⟨Call p,Normal s⟩ =Suc m⇒ t"
            assume Pre: "s ∈ P"
            assume t_notin_F: "t ∉ Fault ` F"
            from exec_call
            show "t ∈ Normal ` Q ∪ Abrupt ` A"
            proof (cases)
              fix bdy m'
              assume m: "Suc m = Suc m'"
              assume bdy: "Γ p = Some bdy"
              assume exec_body: "Γ⊢⟨bdy,Normal s⟩ =m'⇒ t"
              from Pre valid_body_m exec_body bdy m p t_notin_F
              show ?thesis
                by (fastforce simp add: nvalid_def)
            next
              assume "Γ p = None"
              with valid_body p have False by auto
              thus ?thesis ..
            qed
          qed
        qed
      qed
    }
    with p show ?thesis
      by (fastforce simp add: cnvalid_def)
  qed
next
  case (DynCom P Θ F c Q A)
  hence valid_c: "∀s∈P. (∀n. Γ,Θ⊨n:⇘/F⇙ P (c s) Q,A)" by auto
  show "Γ,Θ⊨n:⇘/F⇙ P DynCom c Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨DynCom c,Normal s⟩ =n⇒ t"
    assume P: "s ∈ P"
    assume t_notin_Fault: "t ∉ Fault ` F"
    from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases)
      assume "Γ⊢⟨c s,Normal s⟩ =n⇒ t"
      from cnvalidD [OF valid_c [rule_format, OF P] ctxt this P t_notin_Fault]
      show ?thesis .
    qed
  qed
next
  case (Throw Θ F A Q)
  show "Γ,Θ ⊨n:⇘/F⇙ A Throw Q,A"
  proof (rule cnvalidI)
    fix s t
    assume "Γ⊢⟨Throw,Normal s⟩ =n⇒ t" "s ∈ A"
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by cases simp
  qed
next
  case (Catch Θ F P c⇩1 Q R c⇩2 A)
  have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P c⇩1 Q,R" by fact
  have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ R c⇩2 Q,A" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ =n⇒ t"
    assume P: "s ∈ P"
    assume t_notin_Fault: "t ∉ Fault ` F"
    from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases)
      fix s'
      assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Abrupt s'"
      assume exec_c2: "Γ⊢⟨c⇩2,Normal s'⟩ =n⇒ t"
      from cnvalidD [OF valid_c1 ctxt exec_c1 P ]
      have "Abrupt s' ∈ Abrupt ` R"
        by auto
      with cnvalidD [OF valid_c2 ctxt _ _ t_notin_Fault] exec_c2
      show ?thesis
        by fastforce
    next
      assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t"
      assume notAbr: "¬ isAbr t"
      from cnvalidD [OF valid_c1 ctxt exec_c1 P t_notin_Fault]
      have "t ∈ Normal ` Q ∪ Abrupt ` R" .
      with notAbr
      show ?thesis
        by auto
    qed
  qed
next
  case (Conseq P Θ F c Q A)
  hence adapt: "∀s ∈ P. (∃P' Q' A'. Γ,Θ ⊨n:⇘/F⇙ P' c Q',A'  ∧
                          s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A)"
    by blast
  show "Γ,Θ ⊨n:⇘/F⇙ P c Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof -
      from P adapt obtain P' Q' A' Z  where
        spec: "Γ,Θ⊨n:⇘/F⇙ P' c Q',A'" and
        P': "s ∈ P'"  and  strengthen: "Q' ⊆ Q ∧ A' ⊆ A"
        by auto
      from spec [rule_format] ctxt exec P' t_notin_F
      have "t ∈ Normal ` Q' ∪ Abrupt ` A'"
        by (rule cnvalidD)
      with strengthen show ?thesis
        by blast
    qed
  qed
next
  case (Asm P p Q A Θ F)
  have asm: "(P, p, Q, A) ∈ Θ" by fact
  show "Γ,Θ ⊨n:⇘/F⇙ P (Call p) Q,A"
  proof (rule cnvalidI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    assume exec: "Γ⊢⟨Call p,Normal s⟩ =n⇒ t"
    from asm ctxt have "Γ ⊨n:⇘/F⇙ P Call p Q,A" by auto
    moreover
    assume "s ∈ P" "t ∉ Fault ` F"
    ultimately
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      using exec
      by (auto simp add: nvalid_def)
  qed
next
  case ExFalso thus ?case by iprover
qed

theorem hoare_sound: "Γ,Θ⊢⇘/F⇙ P c Q,A ⟹ Γ,Θ⊨⇘/F⇙ P c Q,A"
  by (iprover intro: cnvalid_to_cvalid hoare_cnvalid)

subsection ‹Completeness›

lemma MGT_valid:
"Γ⊨⇘/F⇙{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪  Fault ` (-F))} c
   {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t}, {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule validI)
  fix s t
  assume "Γ⊢⟨c,Normal s⟩ ⇒ t"
         "s ∈ {s. s = Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪  Fault ` (-F))}"
         "t ∉ Fault ` F"
  thus "t ∈ Normal ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t} ∪
            Abrupt ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
    by (cases t) (auto simp add: final_notin_def)
qed

text ‹The consequence rule where the existential @{term Z} is instantiated
to @{term s}. Usefull in proof of ‹MGT_lemma›.›
lemma ConseqMGT:
  assumes modif: "∀Z. Γ,Θ ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
  assumes impl: "⋀s. s ∈ P ⟹ s ∈ P' s ∧ (∀t. t ∈ Q' s ⟶ t ∈ Q) ∧
                                            (∀t. t ∈ A' s ⟶ t ∈ A)"
  shows "Γ,Θ ⊢⇘/F⇙ P c Q,A"
using impl
by -  (rule conseq [OF modif],blast)


lemma Seq_NoFaultStuckD1:
  assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault `  F)"
  shows "Γ⊢⟨c1,s⟩ ⇒∉({Stuck} ∪ Fault `  F)"
proof (rule final_notinI)
  fix t
  assume exec_c1: "Γ⊢⟨c1,s⟩ ⇒ t"
  show "t ∉ {Stuck} ∪ Fault `  F"
  proof
    assume "t ∈ {Stuck} ∪ Fault `  F"
    moreover
    {
      assume "t = Stuck"
      with exec_c1
      have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Stuck"
        by (auto intro: exec_Seq')
      with noabort have False
        by (auto simp add: final_notin_def)
      hence False ..
    }
    moreover
    {
      assume "t ∈ Fault ` F"
      then obtain f where
      t: "t=Fault f" and f: "f ∈ F"
        by auto
      from t exec_c1
      have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Fault f"
        by (auto intro: exec_Seq')
      with noabort f have False
        by (auto simp add: final_notin_def)
      hence False ..
    }
    ultimately show False by auto
  qed
qed

lemma Seq_NoFaultStuckD2:
  assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault `  F)"
  shows "∀t. Γ⊢⟨c1,s⟩ ⇒ t ⟶ t∉ ({Stuck} ∪ Fault `  F) ⟶
             Γ⊢⟨c2,t⟩ ⇒∉({Stuck} ∪ Fault `  F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq')


lemma MGT_implies_complete:
  assumes MGT: "∀Z. Γ,{}⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪  Fault ` (-F))} c
                           {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
                           {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
  assumes valid: "Γ ⊨⇘/F⇙ P c Q,A"
  shows "Γ,{} ⊢⇘/F⇙ P c Q,A"
  using MGT
  apply (rule ConseqMGT)
  apply (insert valid)
  apply (auto simp add: valid_def intro!: final_notinI)
  done

text ‹Equipped only with the classic consequence rule @{thm "conseqPrePost"}
        we can only derive this syntactically more involved version
        of completeness. But semantically it is equivalent to the "real" one
        (see below)›
lemma MGT_implies_complete':
  assumes MGT: "∀Z. Γ,{}⊢⇘/F⇙
                       {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪  Fault ` (-F))} c
                           {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
                           {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
  assumes valid: "Γ ⊨⇘/F⇙ P c Q,A"
  shows "Γ,{} ⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
  using MGT [rule_format, of Z]
  apply (rule conseqPrePost)
  apply (insert valid)
  apply   (fastforce simp add: valid_def final_notin_def)
  apply  (fastforce simp add: valid_def)
  apply (fastforce simp add: valid_def)
  done

text ‹Semantic equivalence of both kind of formulations›
lemma valid_involved_to_valid:
  assumes valid:
    "∀Z. Γ⊨⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
  shows "Γ ⊨⇘/F⇙ P c Q,A"
  using valid
  apply (simp add: valid_def)
  apply clarsimp
  apply (erule_tac x="x" in allE)
  apply (erule_tac x="Normal x" in allE)
  apply (erule_tac x=t in allE)
  apply fastforce
  done

text ‹The sophisticated consequence rule allow us to do this
        semantical transformation on the hoare-level, too.
        The magic is, that it allow us to
        choose the instance of @{term Z} under the assumption of an state @{term "s ∈ P"}›
lemma
  assumes deriv:
    "∀Z. Γ,{}⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
  shows "Γ,{} ⊢⇘/F⇙ P c Q,A"
  apply (rule ConseqMGT [OF deriv])
  apply auto
  done

lemma valid_to_valid_involved:
  "Γ ⊨⇘/F⇙ P c Q,A ⟹
   Γ⊨⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
by (simp add: valid_def Collect_conv_if)

lemma
  assumes deriv: "Γ,{} ⊢⇘/F⇙ P c Q,A"
  shows "Γ,{}⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
  apply (rule conseqPrePost [OF deriv])
  apply auto
  done

lemma conseq_extract_state_indep_prop:
  assumes state_indep_prop:"∀s ∈ P. R"
  assumes to_show: "R ⟹ Γ,Θ⊢⇘/F⇙ P c Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
  apply (rule Conseq)
  apply (clarify)
  apply (rule_tac x="P" in exI)
  apply (rule_tac x="Q" in exI)
  apply (rule_tac x="A" in exI)
  using state_indep_prop to_show
  by blast


lemma MGT_lemma:
  assumes MGT_Calls:
    "∀p∈dom Γ. ∀Z. Γ,Θ ⊢⇘/F⇙
       {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
        (Call p)
       {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
       {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
  shows "⋀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
             {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (induct c)
  case Skip
  show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Skip,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Skip
           {t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Abrupt t}"
    by (rule hoarep.Skip [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
  case (Basic f)
  show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Basic f,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Basic f
           {t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Normal t},
           {t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Abrupt t}"
    by (rule hoarep.Basic [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
  case (Spec r)
  show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Spec r,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Spec r
           {t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Normal t},
           {t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Abrupt t}"
    apply (rule hoarep.Spec [THEN conseqPre])
    apply (clarsimp simp add: final_notin_def)
    apply (case_tac "∃t. (Z,t) ∈ r")
    apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
    done
next
  case (Seq c1 c2)
  have hyp_c1: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
                           {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
                           {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
    using Seq.hyps by iprover
  have hyp_c2: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c2
                          {t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
                          {t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
    using Seq.hyps by iprover
  from hyp_c1
  have "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
              {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
                  Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))},
              {t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule ConseqMGT)
       (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
             intro: exec.Seq)
  thus "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                   Seq c1 c2
              {t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
              {t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
  proof (rule hoarep.Seq )
    show "Γ,Θ⊢⇘/F⇙ {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
                      Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                   c2
                 {t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
                 {t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
    proof (rule ConseqMGT [OF hyp_c2],safe)
      fix r t
      assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal r" "Γ⊢⟨c2,Normal r⟩ ⇒ Normal t"
      then show "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t"
        by (iprover intro: exec.intros)
    next
      fix r t
      assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal r" "Γ⊢⟨c2,Normal r⟩ ⇒ Abrupt t"
      then show "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t"
        by (iprover intro: exec.intros)
    qed
  qed
next
  case (Cond b c1 c2)
  have "∀Z. Γ,Θ⊢⇘/F⇙{s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
                 {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
                 {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ⊢⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}∩b)
                   c1
                {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
                {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule ConseqMGT)
       (fastforce intro: exec.CondTrue simp add: final_notin_def)
  moreover
  have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c2
                    {t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
                    {t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ⊢⇘/F⇙({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}∩-b)
                  c2
                {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
                {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule ConseqMGT)
       (fastforce intro: exec.CondFalse simp add: final_notin_def)
  ultimately
  show "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                 Cond b c1 c2
              {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
              {t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule hoarep.Cond)
next
  case (While b c)
  let ?unroll = "({(s,t). s∈b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t})⇧*"
  let ?P' = "λZ. {t. (Z,t)∈?unroll ∧
                    (∀e. (Z,e)∈?unroll ⟶ e∈b
                         ⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
                             (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                                  Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}"
  let ?A' = "λZ. {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
  show "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                While b c
              {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t},
              {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
  proof (rule ConseqMGT [where ?P'="?P'"
                         and ?Q'="λZ. ?P' Z ∩ - b" and ?A'="?A'"])
    show "∀Z. Γ,Θ⊢⇘/F⇙ (?P' Z) (While b c) (?P' Z ∩ - b),(?A' Z)"
    proof (rule allI, rule hoarep.While)
      fix Z
      from While
      have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
                        {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
                        {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}" by iprover
      then show "Γ,Θ⊢⇘/F⇙ (?P' Z  ∩ b) c (?P' Z),(?A' Z)"
      proof (rule ConseqMGT)
        fix s
        assume  "s∈ {t. (Z, t) ∈ ?unroll ∧
                      (∀e. (Z,e)∈?unroll ⟶ e∈b
                           ⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
                               (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                                    Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}
                   ∩ b"
        then obtain
          Z_s_unroll: "(Z,s) ∈ ?unroll" and
          noabort:"∀e. (Z,e)∈?unroll ⟶ e∈b
                        ⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
                            (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                                  Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" and
          s_in_b: "s∈b"
          by blast
        show "s ∈ {t. t = s ∧ Γ⊢⟨c,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} ∧
        (∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Normal t} ⟶
             t ∈ {t. (Z, t) ∈ ?unroll ∧
                  (∀e. (Z,e)∈?unroll ⟶  e∈b
                       ⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
                           (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                                  Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}) ∧
         (∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t} ⟶
             t ∈ {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t})"
          (is "?C1 ∧ ?C2 ∧ ?C3")
        proof (intro conjI)
          from Z_s_unroll noabort s_in_b show ?C1 by blast
        next
          {
            fix t
            assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Normal t"
            moreover
            from Z_s_unroll s_t s_in_b
            have "(Z, t) ∈ ?unroll"
              by (blast intro: rtrancl_into_rtrancl)
            moreover note noabort
            ultimately
            have "(Z, t) ∈ ?unroll ∧
                  (∀e. (Z,e)∈?unroll ⟶ e∈b
                        ⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
                            (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                                  Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))"
              by iprover
          }
          then show ?C2 by blast
        next
          {
            fix t
            assume s_t:  "Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t"
            from Z_s_unroll noabort s_t s_in_b
            have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t"
              by blast
          } thus ?C3 by simp
        qed
      qed
    qed
  next
    fix s
    assume P: "s ∈ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
    hence WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
      by auto
    show "s ∈ ?P' s ∧
    (∀t. t∈(?P' s ∩ - b)⟶
         t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t})∧
    (∀t. t∈?A' s ⟶ t∈?A' Z)"
    proof (intro conjI)
      {
        fix e
        assume "(Z,e) ∈ ?unroll" "e ∈ b"
        from this WhileNoFault
        have "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
               (∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
                    Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" (is "?Prop Z e")
        proof (induct rule: converse_rtrancl_induct [consumes 1])
          assume e_in_b: "e ∈ b"
          assume WhileNoFault: "Γ⊢⟨While b c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
          with e_in_b WhileNoFault
          have cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
            by (auto simp add: final_notin_def intro: exec.intros)
          moreover
          {
            fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
            with e_in_b have "Γ⊢⟨While b c,Normal e⟩ ⇒ Abrupt u"
              by (blast intro: exec.intros)
          }
          ultimately
          show "?Prop e e"
            by iprover
        next
          fix Z r
          assume e_in_b: "e∈b"
          assume WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
          assume hyp: "⟦e∈b;Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))⟧
                       ⟹ ?Prop r e"
          assume Z_r:
            "(Z, r) ∈ {(Z, r). Z ∈ b ∧ Γ⊢⟨c,Normal Z⟩ ⇒ Normal r}"
          with WhileNoFault
          have "Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
            by (auto simp add: final_notin_def intro: exec.intros)
          from hyp [OF e_in_b this] obtain
            cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))" and
            Abrupt_r: "∀u. Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u ⟶
                            Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u"
            by simp

           {
            fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
            with Abrupt_r have "Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u" by simp
            moreover from  Z_r obtain
              "Z ∈ b"  "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
              by simp
            ultimately have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u"
              by (blast intro: exec.intros)
          }
          with cNoFault show "?Prop Z e"
            by iprover
        qed
      }
      with P show "s ∈ ?P' s"
        by blast
    next
      {
        fix t
        assume "termination": "t ∉ b"
        assume "(Z, t) ∈ ?unroll"
        hence "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
        proof (induct rule: converse_rtrancl_induct [consumes 1])
          from "termination"
          show "Γ⊢⟨While b c,Normal t⟩ ⇒ Normal t"
            by (blast intro: exec.WhileFalse)
        next
          fix Z r
          assume first_body:
                 "(Z, r) ∈ {(s, t). s ∈ b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
          assume "(r, t) ∈ ?unroll"
          assume rest_loop: "Γ⊢⟨While b c, Normal r⟩ ⇒ Normal t"
          show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
          proof -
            from first_body obtain
              "Z ∈ b" "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
              by fast
            moreover
            from rest_loop have
              "Γ⊢⟨While b c,Normal r⟩ ⇒ Normal t"
              by fast
            ultimately show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
              by (rule exec.WhileTrue)
          qed
        qed
      }
      with P
      show "(∀t. t∈(?P' s ∩ - b)
            ⟶t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t})"
        by blast
    next
      from P show "∀t. t∈?A' s ⟶ t∈?A' Z" by simp
    qed
  qed
next
  case (Call p)
  let ?P = "{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
  from noStuck_Call have "∀s ∈ ?P. p ∈ dom Γ"
    by (fastforce simp add: final_notin_def )
  then show "Γ,Θ⊢⇘/F⇙ ?P (Call p)
               {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
               {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
  proof (rule conseq_extract_state_indep_prop)
    assume p_definied: "p ∈ dom Γ"
    with MGT_Calls show
      "Γ,Θ⊢⇘/F⇙{s. s=Z ∧
                 Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                  (Call p)
                 {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
                 {t. Γ⊢⟨Call  p,Normal Z⟩ ⇒ Abrupt t}"
      by (auto)
  qed
next
  case (DynCom c)
  have hyp:
    "⋀s'. ∀Z. Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨c s',Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c s'
      {t. Γ⊢⟨c s',Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Abrupt t}"
    using DynCom by simp
  have hyp':
  "Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c Z
        {t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
    by (rule ConseqMGT [OF hyp])
       (fastforce simp add: final_notin_def intro: exec.intros)
  show "Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
               DynCom c
             {t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},
             {t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
    apply (rule hoarep.DynCom)
    apply (clarsimp)
    apply (rule hyp' [simplified])
    done
next
  case (Guard f g c)
  have hyp_c: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
                    {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
                    {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
    using Guard by iprover
  show ?case
  proof (cases "f ∈ F")
    case True
    from hyp_c
    have "Γ,Θ⊢⇘/F ⇙(g ∩ {s. s = Z ∧
                    Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (- F))})
             c
           {t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Normal t},
           {t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Abrupt t}"
      apply (rule ConseqMGT)
      apply (insert True)
      apply (auto simp add: final_notin_def intro: exec.intros)
      done
    from True this
    show ?thesis
      by (rule conseqPre [OF Guarantee]) auto
  next
    case False
    from hyp_c
    have "Γ,Θ⊢⇘/F⇙
           (g ∩ {s. s=Z ∧ Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))})
           c
           {t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Normal t},
           {t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Abrupt t}"
      apply (rule ConseqMGT)
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply (auto simp add: final_notin_def intro: exec.intros)
      done
    then show ?thesis
      apply (rule conseqPre [OF hoarep.Guard])
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply auto
      done
  qed
next
  case Throw
  show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Throw,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Throw
              {t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Normal t},
              {t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Abrupt t}"
    by (rule conseqPre [OF hoarep.Throw]) (blast intro: exec.intros)
next
  case (Catch c⇩1 c⇩2)
  have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨c⇩1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩1
                  {t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t},
                  {t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩1
               {t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
               {t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
                   Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
    by (rule ConseqMGT)
       (fastforce intro: exec.intros simp add: final_notin_def)
  moreover
  have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩2
                  {t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Normal t},
                  {t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊢⇘/F⇙{s. Γ⊢⟨c⇩1,Normal Z⟩ ⇒Abrupt s ∧
                   Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
               c⇩2
               {t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
               {t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule ConseqMGT)
       (fastforce intro: exec.intros  simp add: final_notin_def)
  ultimately
  show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
                   Catch c⇩1 c⇩2
              {t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
              {t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Abrupt t}"
    by (rule hoarep.Catch)
qed

lemma MGT_Calls:
 "∀p∈dom Γ. ∀Z.
     Γ,{}⊢⇘/F⇙{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
            (Call p)
          {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
          {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
proof -
  {
    fix p Z
    assume defined: "p ∈ dom Γ"
    have
      "Γ,(⋃p∈dom Γ. ⋃Z.
          {({s. s=Z ∧
             Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))},
             p,
             {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
             {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})
       ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
          (the (Γ p))
          {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
          {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
      (is "Γ,?Θ ⊢⇘/F⇙ (?Pre p Z) (the (Γ p)) (?Post p Z),(?Abr p Z)")
    proof -
      have MGT_Calls:
       "∀p∈dom Γ. ∀Z. Γ,?Θ ⊢⇘/F⇙
        {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
         (Call p)
        {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
        {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
        by (intro ballI allI, rule HoarePartialDef.Asm,auto)
      have "∀Z. Γ,?Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨the (Γ p) ,Normal s⟩ ⇒∉({Stuck} ∪ Fault`(-F))}
                        (the (Γ p))
                        {t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
                        {t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
        by (iprover intro: MGT_lemma [OF MGT_Calls])
      thus "Γ,?Θ⊢⇘/F⇙ (?Pre p Z) (the (Γ p)) (?Post p Z),(?Abr p Z)"
        apply (rule ConseqMGT)
        apply (clarify,safe)
      proof -
        assume "Γ⊢⟨Call p,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
        with defined show "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
          by (fastforce simp add: final_notin_def
                intro: exec.intros)
      next
        fix t
        assume "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t"
        with defined
        show "Γ⊢⟨Call p,Normal Z⟩ ⇒Normal t"
          by  (auto intro: exec.Call)
      next
        fix t
        assume "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t"
        with defined
        show "Γ⊢⟨Call p,Normal Z⟩ ⇒Abrupt t"
          by  (auto intro: exec.Call)
      qed
    qed
  }
  then show ?thesis
    apply -
    apply (intro ballI allI)
    apply (rule CallRec' [where Procs="dom Γ"  and
      P="λp Z. {s. s=Z ∧
                  Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"and
      Q="λp Z.
        {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t}" and
      A="λp Z.
        {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"] )
    apply simp+
    done
qed

theorem hoare_complete: "Γ⊨⇘/F⇙ P c Q,A ⟹ Γ,{}⊢⇘/F⇙ P c Q,A"
  by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Calls])

lemma hoare_complete':
  assumes cvalid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  shows  "Γ,Θ⊢⇘/F⇙ P c Q,A"
proof (cases "Γ⊨⇘/F⇙ P c Q,A")
  case True
  hence "Γ,{}⊢⇘/F⇙ P c Q,A"
    by (rule hoare_complete)
  thus "Γ,Θ⊢⇘/F ⇙P c Q,A"
    by (rule hoare_augment_context) simp
next
  case False
  with cvalid
  show ?thesis
    by (rule ExFalso)
qed


lemma hoare_strip_Γ:
  assumes deriv: "Γ,{}⊢⇘/F⇙ P p Q,A"
  assumes F': "F' ⊆ -F"
  shows "strip F' Γ,{}⊢⇘/F⇙ P p Q,A"
proof (rule hoare_complete)
  from hoare_sound [OF deriv] have "Γ⊨⇘/F⇙ P p Q,A"
    by (simp add: cvalid_def)
  from this F'
  show "strip F' Γ⊨⇘/F⇙ P p Q,A"
    by (rule valid_to_valid_strip)
qed


subsection ‹And Now: Some Useful Rules›

subsubsection ‹Consequence›


lemma LiberalConseq_sound:
fixes F::"'f set"
assumes cons: "∀s ∈ P. ∀(t::('s,'f) xstate). ∃P' Q' A'. (∀n. Γ,Θ⊨n:⇘/F⇙ P' c Q',A') ∧
                ((s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
                              ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A "
proof (rule cnvalidI)
  fix s t
  assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from P cons obtain P' Q' A' where
      spec: "∀n. Γ,Θ⊨n:⇘/F⇙ P' c Q',A'" and
      adapt: "(s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
                              ⟶ t ∈ Normal ` Q ∪ Abrupt ` A"
      apply -
      apply (drule (1) bspec)
      apply (erule_tac x=t in allE)
      apply (elim exE conjE)
      apply iprover
      done
    from exec spec ctxt t_notin_F
    have "s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'"
      by (simp add: cnvalid_def nvalid_def)
    with adapt show ?thesis
      by simp
  qed
qed

lemma LiberalConseq:
fixes F:: "'f set"
assumes cons: "∀s ∈ P.  ∀(t::('s,'f) xstate). ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
                ((s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
                              ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule hoare_complete')
apply (rule allI)
apply (rule LiberalConseq_sound)
using cons
apply (clarify)
apply (drule (1) bspec)
apply (erule_tac x=t in allE)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply (rule conjI)
apply (blast intro: hoare_cnvalid)
apply assumption
done

lemma "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A
           ⟹ Γ,Θ⊢⇘/F⇙ P c Q,A"
  apply (rule LiberalConseq)
  apply (rule ballI)
  apply (drule (1) bspec)
  apply clarify
  apply (rule_tac x=P' in exI)
  apply (rule_tac x=Q' in exI)
  apply (rule_tac x=A' in exI)
  apply auto
  done

lemma
fixes F:: "'f set"
assumes cons: "∀s ∈ P.  ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
                (∀(t::('s,'f) xstate). (s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
                              ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
  apply (rule Conseq)
  apply (rule ballI)
  apply (insert cons)
  apply (drule (1) bspec)
  apply clarify
  apply (rule_tac x=P' in exI)
  apply (rule_tac x=Q' in exI)
  apply (rule_tac x=A' in exI)
  apply (rule conjI)
  apply  assumption
  (* no way to get s ∈ P' *)
  oops

lemma LiberalConseq':
fixes F:: "'f set"
assumes cons: "∀s ∈ P.  ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
                (∀(t::('s,'f) xstate). (s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
                              ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule LiberalConseq)
apply (rule ballI)
apply (rule allI)
apply (insert cons)
apply (drule (1) bspec)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply iprover
done

lemma LiberalConseq'':
fixes F:: "'f set"
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s (t::('s,'f) xstate).
                 (∀Z. s ∈ P' Z ⟶ t ∈ Normal ` Q' Z ∪ Abrupt ` A' Z)
                  ⟶ (s ∈ P ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule LiberalConseq)
apply (rule ballI)
apply (rule allI)
apply (insert cons)
apply (erule_tac x=s in allE)
apply (erule_tac x=t in allE)
apply (case_tac "t ∈ Normal ` Q ∪ Abrupt ` A")
apply (insert spec)
apply  iprover
apply auto
done

primrec procs:: "('s,'p,'f) com ⇒ 'p set"
where
"procs Skip = {}" |
"procs (Basic f) = {}" |
"procs (Seq c⇩1 c⇩2)  = (procs c⇩1 ∪ procs c⇩2)" |
"procs (Cond b c⇩1 c⇩2) = (procs c⇩1 ∪ procs c⇩2)" |
"procs (While b c) = procs c" |
"procs (Call p) = {p}" |
"procs (DynCom c) = (⋃s. procs (c s))" |
"procs (Guard f g c) = procs c" |
"procs Throw = {}" |
"procs (Catch c⇩1 c⇩2) = (procs c⇩1 ∪ procs c⇩2)"

primrec noSpec:: "('s,'p,'f) com ⇒ bool"
where
"noSpec Skip = True" |
"noSpec (Basic f) = True" |
"noSpec (Spec r) = False" |
"noSpec (Seq c⇩1 c⇩2)  = (noSpec c⇩1 ∧ noSpec c⇩2)" |
"noSpec (Cond b c⇩1 c⇩2) = (noSpec c⇩1 ∧ noSpec c⇩2)" |
"noSpec (While b c) = noSpec c" |
"noSpec (Call p) = True" |
"noSpec (DynCom c) = (∀s. noSpec (c s))" |
"noSpec (Guard f g c) = noSpec c" |
"noSpec Throw = True" |
"noSpec (Catch c⇩1 c⇩2) = (noSpec c⇩1 ∧ noSpec c⇩2)"

lemma exec_noSpec_no_Stuck:
 assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
 assumes noSpec_c: "noSpec c"
 assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
 assumes procs_subset: "procs c ⊆ dom Γ"
 assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
 assumes s_no_Stuck: "s≠Stuck"
 shows "t≠Stuck"
using exec noSpec_c procs_subset s_no_Stuck proof induct
  case (Call p bdy s t) with noSpec_Γ procs_subset_Γ show ?case
    by (auto dest!: bspec [of _ _ p])
next
  case (DynCom c s t) then show ?case
   by auto blast
qed auto

lemma execn_noSpec_no_Stuck:
 assumes exec: "Γ⊢⟨c,s⟩ =n⇒ t"
 assumes noSpec_c: "noSpec c"
 assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
 assumes procs_subset: "procs c ⊆ dom Γ"
 assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
 assumes s_no_Stuck: "s≠Stuck"
 shows "t≠Stuck"
using exec noSpec_c procs_subset s_no_Stuck proof induct
  case (Call p bdy n s t) with noSpec_Γ procs_subset_Γ show ?case
    by (auto dest!: bspec [of _ _ p])
next
  case (DynCom c s t) then show ?case
    by auto blast
qed auto

lemma LiberalConseq_noguards_nothrows_sound:
assumes spec: "∀Z. ∀n. Γ,Θ⊨n:⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s t. (∀Z. s ∈ P' Z ⟶ t ∈  Q' Z )
                  ⟶ (s ∈ P ⟶ t ∈ Q )"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A "
proof (rule cnvalidI)
  fix s t
  assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from execn_noguards_no_Fault [OF exec noguards_c noguards_Γ]
     execn_nothrows_no_Abrupt [OF exec nothrows_c nothrows_Γ ]
     execn_noSpec_no_Stuck [OF exec
              noSpec_c  noSpec_Γ procs_subset
      procs_subset_Γ]
    obtain t' where t: "t=Normal t'"
      by (cases t) auto
    with exec spec ctxt
    have "(∀Z. s ∈ P' Z ⟶ t' ∈  Q' Z)"
      by (unfold  cnvalid_def nvalid_def) blast
    with cons P t show ?thesis
      by simp
  qed
qed


lemma LiberalConseq_noguards_nothrows:
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s t. (∀Z. s ∈ P' Z ⟶ t ∈  Q' Z )
                  ⟶ (s ∈ P ⟶ t ∈ Q )"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule hoare_complete')
apply (rule allI)
apply (rule LiberalConseq_noguards_nothrows_sound
             [OF _ cons noguards_c noguards_Γ nothrows_c nothrows_Γ
                 noSpec_c noSpec_Γ
                 procs_subset procs_subset_Γ])
apply (insert spec)
apply (intro allI)
apply (erule_tac x=Z in allE)
by (rule hoare_cnvalid)

lemma
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙{s. s=fst Z ∧ P s (snd Z)} c {t. Q (fst Z) (snd Z) t},{}"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "∀σ. Γ,Θ⊢⇘/F⇙{s. s=σ} c {t. ∀l. P σ l ⟶ Q σ l t},{}"
apply (rule allI)
apply (rule LiberalConseq_noguards_nothrows
              [OF spec _ noguards_c noguards_Γ nothrows_c nothrows_Γ
                  noSpec_c noSpec_Γ
                  procs_subset procs_subset_Γ])
apply auto
done

subsubsection ‹Modify Return›

lemma Proc_exnModifyReturn_sound:
  assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call_exn init p return' result_exn c Q,A"
  assumes valid_modif:
    "∀σ. ∀n. Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
  assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ result_exn (return' s t) t = result_exn (return s t) t"
  shows "Γ,Θ ⊨n:⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/UNIV⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  assume exec: "Γ⊢⟨call_exn init p return result_exn c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from exec
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: execn_call_exn_Normal_elim)
    fix bdy m t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
    assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
    assume n: "n = Suc m"
    from exec_body n bdy
    have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Normal t'"
      by (auto simp add: intro: execn.Call)
    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
    have "t' ∈ Modif (init s)"
      by auto
    with ret_modif have "Normal (return' s t') =
      Normal (return s t')"
      by simp
    with exec_body exec_c bdy n
    have "Γ⊢⟨call_exn init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exn)
    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy m t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
    assume n: "n = Suc m"
    assume t: "t = Abrupt (result_exn (return s t') t')"
    also from exec_body n bdy
    have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Abrupt t'"
      by (auto simp add: intro: execn.intros)
    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
    have "t' ∈ ModifAbr (init s)"
      by auto
    with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
      by simp
    finally have "t = Abrupt (result_exn (return' s t') t')"  .
    with exec_body bdy n
    have "Γ⊢⟨call_exn init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnAbrupt)
    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy m f
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m"
      "t = Fault f"
    with bdy have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnFault)
    from valid_call [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  next
    fix bdy m
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
      "t = Stuck"
    with bdy have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnStuck)
    from valid_call [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  next
    fix m
    assume "Γ p = None"
    and  "n = Suc m" "t = Stuck"
    then have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnUndefined)
    from valid_call [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  qed
qed

lemma ProcModifyReturn_sound:
  assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call init p return' c Q,A"
  assumes valid_modif:
    "∀σ. ∀n. Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
  assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ return' s t = return s t"
  shows "Γ,Θ ⊨n:⇘/F⇙ P (call init p return c) Q,A"
  using valid_call valid_modif ret_modif ret_modifAbr
  unfolding call_call_exn
  by (rule Proc_exnModifyReturn_sound)

lemma Proc_exnModifyReturn:
  assumes spec: "Γ,Θ⊢⇘/F⇙ P (call_exn init p return' result_exn c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes return_conform:
      "∀s t. t ∈ ModifAbr (init s)
             ⟶ (result_exn (return' s t) t) = (result_exn (return s t) t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊢⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊢⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Proc_exnModifyReturn_sound
          [where Modif=Modif and ModifAbr=ModifAbr,
            OF _ _ result_conform return_conform] )
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done

lemma ProcModifyReturn:
  assumes spec: "Γ,Θ⊢⇘/F⇙ P (call init p return' c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes return_conform:
      "∀s t. t ∈ ModifAbr (init s)
             ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊢⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (call init p return c) Q,A"
  using spec result_conform return_conform modifies_spec
  unfolding call_call_exn
  by (rule Proc_exnModifyReturn)

lemma Proc_exnModifyReturnSameFaults_sound:
  assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call_exn init p return' result_exn c Q,A"
  assumes valid_modif:
    "∀σ. ∀n. Γ,Θ⊨n:⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
  assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ result_exn (return' s t) t = result_exn (return s t) t"
  shows "Γ,Θ ⊨n:⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨call_exn init p return result_exn c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from exec
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: execn_call_exn_Normal_elim)
    fix bdy m t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
    assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
    assume n: "n = Suc m"
    from exec_body n bdy
    have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Normal t'"
      by (auto simp add: intro: execn.intros)
    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
    have "t' ∈ Modif (init s)"
      by auto
    with ret_modif have "Normal (return' s t') =
      Normal (return s t')"
      by simp
    with exec_body exec_c bdy n
    have "Γ⊢⟨call_exn init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exn)
    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy m t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
    assume n: "n = Suc m"
    assume t: "t = Abrupt (result_exn (return s t') t')"
    also
    from exec_body n bdy
    have "Γ⊢⟨Call p,Normal (init s)⟩ =n ⇒ Abrupt t'"
      by (auto simp add: intro: execn.intros)
    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
    have "t' ∈ ModifAbr (init s)"
      by auto
    with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
      by simp
    finally have "t = Abrupt (result_exn (return' s t') t')" .
    with exec_body bdy n
    have "Γ⊢⟨call_exn init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnAbrupt)
    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy m f
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m"  and
      t: "t = Fault f"
    with bdy have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnFault)
    from cnvalidD [OF valid_call [rule_format] ctxt this P] t t_notin_F
    show ?thesis
      by simp
  next
    fix bdy m
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
      "t = Stuck"
    with bdy have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnStuck)
    from valid_call [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  next
    fix m
    assume "Γ p = None"
    and  "n = Suc m" "t = Stuck"
    then have "Γ⊢⟨call_exn init p return' result_exn c ,Normal s⟩ =n⇒ t"
      by (auto intro: execn_call_exnUndefined)
    from valid_call [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  qed
qed

lemma ProcModifyReturnSameFaults_sound:
  assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call init p return' c Q,A"
  assumes valid_modif:
    "∀σ. ∀n. Γ,Θ⊨n:⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
  assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ return' s t = return s t"
  shows "Γ,Θ ⊨n:⇘/F⇙ P (call init p return c) Q,A"
  using valid_call valid_modif ret_modif ret_modifAbr
  unfolding call_call_exn
  by (rule Proc_exnModifyReturnSameFaults_sound)


lemma Proc_exnModifyReturnSameFaults:
  assumes spec: "Γ,Θ⊢⇘/F⇙ P (call_exn init p return' result_exn c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes return_conform:
  "∀s t. t ∈ ModifAbr (init s) ⟶ (result_exn (return' s t) t) = (result_exn (return s t) t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊢⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Proc_exnModifyReturnSameFaults_sound
          [where Modif=Modif and ModifAbr=ModifAbr,
         OF _ _ result_conform return_conform])
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done


lemma ProcModifyReturnSameFaults:
  assumes spec: "Γ,Θ⊢⇘/F⇙ P (call init p return' c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes return_conform:
  "∀s t. t ∈ ModifAbr (init s) ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (call init p return c) Q,A"
  using spec result_conform return_conform modifies_spec
  unfolding call_call_exn
  by (rule Proc_exnModifyReturnSameFaults)


subsubsection ‹DynCall›



lemma dynProc_exnModifyReturn_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "∀s ∈ P. ∀σ. ∀n.
       Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ result_exn (return' s t) t = result_exn (return s t) t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/UNIV⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  assume exec: "Γ⊢⟨dynCall_exn f g init p return result_exn c,Normal s⟩ =n⇒ t"
  assume t_notin_F: "t ∉ Fault ` F"
  assume P: "s ∈ P"
  with valid_modif
  have valid_modif': "∀σ. ∀n.
       Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
    by blast
  from exec thm execn_Normal_elim_cases
  have exec_call: "Γ⊢⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ =n⇒ t"
    by (cases rule: execn_dynCall_exn_Normal_elim)
  then show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: execn_maybe_guard_Normal_elim_cases)
    case noFault
    from noFault have guards_ok: "s ∈ g" by simp
    from noFault have "Γ⊢ ⟨call_exn init (p s) return result_exn c,Normal s⟩ =n⇒ t" by simp
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases rule: execn_call_exn_Normal_elim)
      fix bdy m t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
      assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
      assume n: "n = Suc m"
      from exec_body n bdy
      have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n⇒ Normal t'"
        by (auto simp add: intro: execn.intros)
      from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
      have "t' ∈ Modif (init s)"
        by auto
      with ret_modif have "Normal (return' s t') = Normal (return s t')"
        by simp
      with exec_body exec_c bdy n
      have "Γ⊢⟨call_exn init (p s) return' result_exn c,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exn)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from cnvalidD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy m t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
      assume n: "n = Suc m"
      assume t: "t = Abrupt (result_exn (return s t') t')"
      also from exec_body n bdy
      have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n⇒ Abrupt t'"
        by (auto simp add: intro: execn.intros)
      from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
      have "t' ∈ ModifAbr (init s)"
        by auto
      with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
        by simp
      finally have "t = Abrupt (result_exn (return' s t') t')" .
      with exec_body bdy n
      have "Γ⊢⟨call_exn init (p s) return' result_exn c,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnAbrupt)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from cnvalidD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy m f'
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f'" "n = Suc m"
        "t = Fault f'"
      with bdy have "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnFault)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cnvalidD)
    next
      fix bdy m
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
        "t = Stuck"
      with bdy have "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnStuck)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cnvalidD)
    next
      fix m
      assume "Γ (p s) = None"
      and  "n = Suc m" "t = Stuck"
      hence "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnUndefined)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cnvalidD)
    qed
  next
    case (someFault)
    then obtain guards_fail:"s ∉ g"
      and t: "t = Fault f" by simp
    from execn_maybe_guard_Fault [OF guards_fail] t
    have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
    from cnvalidD [OF valid_call ctxt this] P t_notin_F
    show ?thesis by simp
  qed
qed

lemma dynProcModifyReturn_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
    "∀s ∈ P. ∀σ. ∀n.
       Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall init p return c) Q,A"
  using valid_call valid_modif ret_modif ret_modifAbr
  unfolding dynCall_dynCall_exn
  by (rule dynProc_exnModifyReturn_sound)


lemma dynProc_exnModifyReturn:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall_exn f g init p return' result_exn c Q,A"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ result_exn (return' s t) t = result_exn (return s t) t"
assumes modif:
    "∀s ∈ P. ∀σ.
       Γ,Θ⊢⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
          OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done

lemma dynProcModifyReturn:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall init p return' c Q,A"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ return' s t = return s t"
assumes modif:
    "∀s ∈ P. ∀σ.
       Γ,Θ⊢⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊢⇘/F⇙ P (dynCall init p return c) Q,A"
  using dyn_call ret_modif ret_modifAbr modif
  unfolding dynCall_dynCall_exn
  by (rule dynProc_exnModifyReturn)

lemma dynProc_exnModifyReturnSameFaults_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "∀s ∈ P. ∀σ. ∀n.
       Γ,Θ⊨n:⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ result_exn (return' s t) t = result_exn (return s t) t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨dynCall_exn f g init p return result_exn c,Normal s⟩ =n⇒ t"
  assume t_notin_F: "t ∉ Fault ` F"
  assume P: "s ∈ P"
  with valid_modif
  have valid_modif': "∀σ. ∀n.
    Γ,Θ⊨n:⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
    by blast
  from exec
  have exec_call: "Γ⊢⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ =n⇒ t"
    by (cases rule: execn_dynCall_exn_Normal_elim)
  then show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: execn_maybe_guard_Normal_elim_cases)
    case noFault
    from noFault have guards_ok: "s ∈ g" by simp
    from noFault have "Γ⊢ ⟨call_exn init (p s) return result_exn c,Normal s⟩ =n⇒ t" by simp
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"

    proof (cases rule: execn_call_exn_Normal_elim)
      fix bdy m t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
      assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
      assume n: "n = Suc m"
      from exec_body n bdy
      have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n ⇒ Normal t'"
        by (auto simp add: intro: execn.Call)
      from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
      have "t' ∈ Modif (init s)"
        by auto
      with ret_modif have "Normal (return' s t') = Normal (return s t')"
        by simp
      with exec_body exec_c bdy n
      have "Γ⊢⟨call_exn init (p s) return' result_exn c,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exn)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from cnvalidD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy m t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
      assume n: "n = Suc m"
      assume t: "t = Abrupt (result_exn (return s t') t')"
      also from exec_body n bdy
      have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n ⇒ Abrupt t'"
        by (auto simp add: intro: execn.intros)
      from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
      have "t' ∈ ModifAbr (init s)"
        by auto
      with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
        by simp
      finally have "t = Abrupt (result_exn (return' s t') t')" .
      with exec_body bdy n
      have "Γ⊢⟨call_exn init (p s) return' result_exn c,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnAbrupt)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from cnvalidD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy m f'
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f'" "n = Suc m"  and
        t: "t = Fault f'"
      with bdy have "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnFault)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from cnvalidD [OF valid_call ctxt this P] t t_notin_F
      show ?thesis
        by simp
    next
      fix bdy m
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
        "t = Stuck"
      with bdy have "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnStuck)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cnvalidD)
    next
      fix m
      assume "Γ (p s) = None"
      and  "n = Suc m" "t = Stuck"
      hence "Γ⊢⟨call_exn init (p s) return' result_exn c ,Normal s⟩ =n⇒ t"
        by (auto intro: execn_call_exnUndefined)
      from execn_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
        by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cnvalidD)
    qed
  next
    case (someFault)
    then obtain guards_fail:"s ∉ g"
      and t: "t = Fault f" by simp
    from execn_maybe_guard_Fault [OF guards_fail] t
    have "Γ⊢⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ =n⇒ t"
      by (simp add: dynCall_exn_def execn_guards_DynCom)
    from cnvalidD [OF valid_call ctxt this] P t_notin_F
    show ?thesis by simp
  qed
qed


lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
    "∀s ∈ P. ∀σ. ∀n.
       Γ,Θ⊨n:⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall init p return c) Q,A"
  using valid_call valid_modif ret_modif ret_modifAbr
  unfolding dynCall_dynCall_exn
  by (rule dynProc_exnModifyReturnSameFaults_sound)

lemma dynProc_exnModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall_exn f g init p return' result_exn c Q,A"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ result_exn (return' s t) t = result_exn (return s t) t"
assumes modif:
    "∀s ∈ P. ∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturnSameFaults_sound
        [where Modif=Modif and ModifAbr=ModifAbr,
           OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
  done

lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall init p return' c Q,A"
assumes ret_modif:
    "∀s t. t ∈ Modif (init s)
           ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
                             ⟶ return' s t = return s t"
assumes modif:
    "∀s ∈ P. ∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊢⇘/F⇙ P (dynCall init p return c) Q,A"
  using dyn_call ret_modif ret_modifAbr modif
  unfolding dynCall_dynCall_exn
  by (rule dynProc_exnModifyReturnSameFaults)


subsubsection ‹Conjunction of Postcondition›

lemma PostConjI_sound:
assumes valid_Q: "∀n. Γ,Θ ⊨n:⇘/F⇙ P c Q,A"
assumes valid_R: "∀n. Γ,Θ ⊨n:⇘/F⇙ P c R,B"
shows "Γ,Θ ⊨n:⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from valid_Q [rule_format] ctxt exec P t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` A"
    by (rule cnvalidD)
  moreover
  from valid_R [rule_format] ctxt exec P t_notin_F have "t ∈ Normal ` R ∪ Abrupt ` B"
    by (rule cnvalidD)
  ultimately show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ B)"
    by blast
qed

lemma PostConjI:
  assumes deriv_Q: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  assumes deriv_R: "Γ,Θ⊢⇘/F⇙ P c R,B"
  shows "Γ,Θ⊢⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
apply (rule hoare_complete')
apply (rule allI)
apply (rule PostConjI_sound)
using deriv_Q
apply (blast intro: hoare_cnvalid)
using deriv_R
apply (blast intro: hoare_cnvalid)
done

lemma Merge_PostConj_sound:
  assumes validF: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  assumes validG: "∀n. Γ,Θ⊨n:⇘/G⇙ P' c R,X"
  assumes F_G: "F ⊆ G"
  assumes P_P': "P ⊆ P'"
  shows "Γ,Θ⊨n:⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  with F_G have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/G⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  with P_P' have P': "s ∈ P'"
    by auto
  assume t_noFault: "t ∉ Fault ` F"
  show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ X)"
  proof -
    from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault]
    have *: "t ∈ Normal ` Q ∪ Abrupt ` A".
    then have "t ∉ Fault ` G"
      by auto
    from cnvalidD [OF validG [rule_format] ctxt' exec P' this]
    have "t ∈ Normal ` R ∪ Abrupt ` X" .
    with * show ?thesis by auto
  qed
qed

lemma Merge_PostConj:
  assumes validF: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  assumes validG: "Γ,Θ⊢⇘/G⇙ P' c R,X"
  assumes F_G: "F ⊆ G"
  assumes P_P': "P ⊆ P'"
  shows "Γ,Θ⊢⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
using validF apply (blast intro:hoare_cnvalid)
using validG apply (blast intro:hoare_cnvalid)
done

subsubsection ‹Weaken Context›


lemma WeakenContext_sound:
  assumes valid_c: "∀n. Γ,Θ'⊨n:⇘/F⇙ P c Q,A"
  assumes valid_ctxt: "∀(P, p, Q, A)∈Θ'. Γ,Θ⊨n:⇘/F⇙ P (Call p) Q,A"
  shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  with valid_ctxt
  have ctxt': "∀(P, p, Q, A)∈Θ'. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
    by (simp add: cnvalid_def)
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from valid_c [rule_format] ctxt' exec P t_notin_F
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by (rule cnvalidD)
qed

lemma WeakenContext:
  assumes deriv_c: "Γ,Θ'⊢⇘/F⇙ P c Q,A"
  assumes deriv_ctxt: "∀(P,p,Q,A)∈Θ'. Γ,Θ⊢⇘/F⇙ P (Call p) Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule WeakenContext_sound)
using deriv_c
apply (blast intro: hoare_cnvalid)
using deriv_ctxt
apply (blast intro: hoare_cnvalid)
done

subsubsection ‹Guards and Guarantees›

lemma SplitGuards_sound:
assumes valid_c1: "∀n. Γ,Θ⊨n:⇘/F⇙ P c⇩1 Q,A"
assumes valid_c2: "∀n. Γ,Θ⊨n:⇘/F⇙ P c⇩2 UNIV,UNIV"
assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases t)
    case Normal
    with inter_guards_execn_noFault [OF c exec]
    have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
    from valid_c1 [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  next
    case Abrupt
    with inter_guards_execn_noFault [OF c exec]
    have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
    from valid_c1 [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  next
    case (Fault f)
    with exec inter_guards_execn_Fault [OF c]
    have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Fault f ∨ Γ⊢⟨c⇩2,Normal s⟩ =n⇒ Fault f"
      by auto
    then show ?thesis
    proof (cases rule: disjE [consumes 1])
      assume "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Fault f"
      from Fault cnvalidD [OF valid_c1 [rule_format] ctxt this P] t_notin_F
      show ?thesis
        by blast
    next
      assume "Γ⊢⟨c⇩2,Normal s⟩ =n⇒ Fault f"
      from Fault cnvalidD [OF valid_c2 [rule_format] ctxt this P] t_notin_F
      show ?thesis
        by blast
    qed
  next
    case Stuck
    with inter_guards_execn_noFault [OF c exec]
    have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
    from valid_c1 [rule_format] ctxt this P t_notin_F
    show ?thesis
      by (rule cnvalidD)
  qed
qed

lemma SplitGuards:
  assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
  assumes deriv_c1: "Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A"
  assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P c⇩2 UNIV,UNIV"
  shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule SplitGuards_sound [OF _ _ c])
using deriv_c1
apply (blast intro: hoare_cnvalid)
using deriv_c2
apply (blast intro: hoare_cnvalid)
done

lemma CombineStrip_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  assumes valid_strip: "∀n. Γ,Θ⊨n:⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
  shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases t)
    case (Normal t')
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
    show ?thesis
      by auto
  next
    case (Abrupt t')
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
    show ?thesis
      by auto
  next
    case (Fault f)
    show ?thesis
    proof (cases "f ∈ F")
      case True
      hence "f ∉ -F" by simp
      with exec Fault
      have "Γ⊢⟨strip_guards (-F) c,Normal s⟩ =n⇒ Fault f"
        by (auto intro: execn_to_execn_strip_guards_Fault)
      from cnvalidD [OF valid_strip [rule_format] ctxt this P] Fault
      have False
        by auto
      thus ?thesis ..
    next
      case False
      with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
      show ?thesis
        by auto
    qed
  next
    case Stuck
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
    show ?thesis
      by auto
  qed
qed

lemma CombineStrip:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  assumes deriv_strip: "Γ,Θ⊢⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
  shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule CombineStrip_sound)
apply  (iprover intro: hoare_cnvalid [OF deriv])
apply (iprover intro: hoare_cnvalid [OF deriv_strip])
done

lemma GuardsFlip_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  assumes validFlip: "∀n. Γ,Θ⊨n:⇘/-F⇙ P c UNIV,UNIV"
  shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  from ctxt have ctxtFlip: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/-F⇙ P (Call p) Q,A"
    by (auto intro: nvalid_augment_Faults)
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases t)
    case (Normal t')
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
    show ?thesis
      by auto
  next
    case (Abrupt t')
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
    show ?thesis
      by auto
  next
    case (Fault f)
    show ?thesis
    proof (cases "f ∈ F")
      case True
      hence "f ∉ -F" by simp
      with cnvalidD [OF validFlip [rule_format] ctxtFlip exec P] Fault
      have False
        by auto
      thus ?thesis ..
    next
      case False
      with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
      show ?thesis
        by auto
    qed
  next
    case Stuck
    from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
    show ?thesis
      by auto
  qed
qed

lemma GuardsFlip:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  assumes derivFlip: "Γ,Θ⊢⇘/-F⇙ P c UNIV,UNIV"
  shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule GuardsFlip_sound)
apply  (iprover intro: hoare_cnvalid [OF deriv])
apply (iprover intro: hoare_cnvalid [OF derivFlip])
done

lemma MarkGuardsI_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
  shows "Γ,Θ⊨n:⇘/{}⇙ P mark_guards f c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ t"
  from execn_mark_guards_to_execn [OF exec] obtain t' where
    exec_c: "Γ⊢⟨c,Normal s⟩ =n⇒ t'" and
    t'_noFault: "¬ isFault t' ⟶ t' = t"
    by blast
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from cnvalidD [OF valid [rule_format] ctxt exec_c P]
    have "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by blast
    with t'_noFault
    show ?thesis
      by auto
  qed
qed

lemma MarkGuardsI:
  assumes deriv: "Γ,Θ⊢⇘/{}⇙ P c Q,A"
  shows "Γ,Θ⊢⇘/{}⇙ P mark_guards f c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MarkGuardsI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done

lemma MarkGuardsD_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P mark_guards f c Q,A"
  shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases "isFault t")
    case True
    with execn_to_execn_mark_guards_Fault [OF exec ]
    obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ Fault f'"
      by (fastforce elim: isFaultE)
    from cnvalidD [OF valid [rule_format] ctxt this P]
    have False
      by auto
    thus ?thesis ..
  next
    case False
    from execn_to_execn_mark_guards [OF exec False]
    obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ t"
      by auto
    from cnvalidD [OF valid [rule_format] ctxt this P]
    show ?thesis
      by auto
  qed
qed

lemma MarkGuardsD:
  assumes deriv: "Γ,Θ⊢⇘/{}⇙ P mark_guards f c Q,A"
  shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MarkGuardsD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done

lemma MergeGuardsI_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  shows "Γ,Θ⊨n:⇘/F⇙ P merge_guards c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ =n⇒ t"
  from execn_merge_guards_to_execn [OF exec_merge]
  have exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t" .
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from cnvalidD [OF valid [rule_format] ctxt exec P t_notin_F]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed

lemma MergeGuardsI:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P merge_guards c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MergeGuardsI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done

lemma MergeGuardsD_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P merge_guards c Q,A"
  shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  from execn_to_execn_merge_guards [OF exec]
  have exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ =n⇒ t".
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from cnvalidD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed

lemma MergeGuardsD:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P merge_guards c Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MergeGuardsD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done


lemma SubsetGuards_sound:
  assumes c_c': "c ⊆⇩g c'"
  assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P c' Q,A"
  shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  from execn_to_execn_subseteq_guards [OF c_c' exec] obtain t' where
    exec_c': "Γ⊢⟨c',Normal s⟩ =n⇒ t'" and
    t'_noFault: "¬ isFault t' ⟶ t' = t"
    by blast
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  from cnvalidD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by auto
qed

lemma SubsetGuards:
  assumes c_c': "c ⊆⇩g c'"
  assumes deriv: "Γ,Θ⊢⇘/{}⇙ P c' Q,A"
  shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule SubsetGuards_sound [OF c_c'])
apply (iprover intro: hoare_cnvalid [OF deriv])
done

lemma NormalizeD_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P (normalize c) Q,A"
  shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  hence exec_norm: "Γ⊢⟨normalize c,Normal s⟩ =n⇒ t"
    by (rule execn_to_execn_normalize)
  assume P: "s ∈ P"
  assume noFault: "t ∉ Fault ` F"
  from cnvalidD [OF valid [rule_format] ctxt exec_norm P noFault]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed

lemma NormalizeD:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P (normalize c) Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule NormalizeD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done

lemma NormalizeI_sound:
  assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
  shows "Γ,Θ⊨n:⇘/F⇙ P (normalize c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
  assume "Γ⊢⟨normalize c,Normal s⟩ =n⇒ t"
  hence exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
    by (rule execn_normalize_to_execn)
  assume P: "s ∈ P"
  assume noFault: "t ∉ Fault ` F"
  from cnvalidD [OF valid [rule_format] ctxt exec P noFault]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed

lemma NormalizeI:
  assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P (normalize c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule NormalizeI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done


subsubsection ‹Restricting the Procedure Environment›

lemma nvalid_restrict_to_nvalid:
assumes valid_c: "Γ|⇘M⇙⊨n:⇘/F⇙ P c Q,A"
shows "Γ⊨n:⇘/F⇙ P c Q,A"
proof (rule nvalidI)
  fix s t
  assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from execn_to_execn_restrict [OF exec]
    obtain t' where
      exec_res: "Γ|⇘M⇙⊢⟨c,Normal s⟩ =n⇒ t'" and
      t_Fault: "∀f. t = Fault f ⟶ t' ∈ {Fault f, Stuck}" and
      t'_notStuck: "t'≠Stuck ⟶ t'=t"
      by blast
    from t_Fault t_notin_F t'_notStuck have "t' ∉ Fault ` F"
      by (cases t') auto
    with valid_c exec_res P
    have "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by (auto simp add: nvalid_def)
    with t'_notStuck
    show ?thesis
      by auto
  qed
qed

lemma valid_restrict_to_valid:
assumes valid_c: "Γ|⇘M⇙⊨⇘/F⇙ P c Q,A"
shows "Γ⊨⇘/F⇙ P c Q,A"
proof (rule validI)
  fix s t
  assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from exec_to_exec_restrict [OF exec]
    obtain t' where
      exec_res: "Γ|⇘M⇙⊢⟨c,Normal s⟩ ⇒ t'" and
      t_Fault: "∀f. t = Fault f ⟶ t' ∈ {Fault f, Stuck}" and
      t'_notStuck: "t'≠Stuck ⟶ t'=t"
      by blast
    from t_Fault t_notin_F t'_notStuck have "t' ∉ Fault ` F"
      by (cases t') auto
    with valid_c exec_res P
    have "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by (auto simp add: valid_def)
    with t'_notStuck
    show ?thesis
      by auto
  qed
qed

lemma augment_procs:
assumes deriv_c: "Γ|⇘M⇙,{}⊢⇘/F⇙ P c Q,A"
shows "Γ,{}⊢⇘/F⇙ P c Q,A"
  apply (rule hoare_complete)
  apply (rule valid_restrict_to_valid)
  apply (insert hoare_sound [OF deriv_c])
  by (simp add: cvalid_def)

lemma augment_Faults:
assumes deriv_c: "Γ,{}⊢⇘/F⇙ P c Q,A"
assumes F: "F ⊆ F'"
shows "Γ,{}⊢⇘/F'⇙ P c Q,A"
  apply (rule hoare_complete)
  apply (rule valid_augment_Faults [OF _ F])
  apply (insert hoare_sound [OF deriv_c])
  by (simp add: cvalid_def)

end