(*
    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 Total Correctness Hoare Logic›

theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin

subsection ‹Soundness›

lemma hoaret_sound:
 assumes hoare: "Γ,Θ⊨_tF P c Q,A"
 shows "Γ,Θ⊨_tF P c Q,A"
using hoare
proof (induct)
  case (Skip Θ F P A)
  show "Γ,Θ ⊨_tF P Skip P,A"
  proof (rule cvalidtI)
    fix s t
    assume "Γ⊨⟨Skip,Normal s⟩ → t" "s ∈ P"
    thus "t ∈ Normal ` P ∪ Abrupt ` A"
      by cases auto
  next
    fix s show "Γ⊨Skip ↓ Normal s"
      by (rule terminates.intros)
  qed
next
  case (Basic Θ F f P A)
  show "Γ,Θ ⊨_tF {s. f s ∈ P} (Basic f) P,A"
  proof (rule cvalidtI)
    fix s t
    assume "Γ⊨⟨Basic f,Normal s⟩ → t" "s ∈ {s. f s ∈ P}"
    thus "t ∈ Normal ` P ∪ Abrupt ` A"
      by cases auto
  next
    fix s show "Γ⊨Basic f ↓ Normal s"
      by (rule terminates.intros)
  qed
next
  case (Spec Θ F r Q A)
  show "Γ,Θ⊨_tF {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A"
  proof (rule cvalidtI)
    fix s t
    assume "Γ⊨⟨Spec r ,Normal s⟩ → t"
           "s ∈ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)}"
    thus "t ∈ Normal ` Q ∪ Abrupt ` A"
      by cases auto
  next
    fix s show "Γ⊨Spec r ↓ Normal s"
      by (rule terminates.intros)
  qed
next
  case (Seq Θ F P c1 R A c2 Q)
  have valid_c1: "Γ,Θ ⊨_tF P c1 R,A" by fact
  have valid_c2: "Γ,Θ ⊨_tF R c2 Q,A" by fact
  show "Γ,Θ ⊨_tF P Seq c1 c2 Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume exec: "Γ⊨⟨Seq c1 c2,Normal s⟩ → t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    from exec P obtain r where
      exec_c1: "Γ⊨⟨c1,Normal s⟩ → r" and exec_c2:  "Γ⊨⟨c2,r⟩ → t"
      by cases auto
    with t_notin_F have "r ∉ Fault ` F"
      by (auto dest: Fault_end)
    from valid_c1 ctxt exec_c1 P this
    have r: "r ∈ Normal ` R ∪ Abrupt ` A"
      by (rule cvalidt_postD)
    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 cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F])
        apply auto
        done
    next
      case (Abrupt r')
      with exec_c2 have "t=Abrupt r'"
        by (auto elim: exec_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
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume P: "s∈P"
    show "Γ⊨Seq c1 c2 ↓ Normal s"
    proof -
      from valid_c1 ctxt P
      have "Γ⊨c1↓ Normal s"
        by (rule cvalidt_termD)
      moreover
      {
        fix r assume exec_c1: "Γ⊨⟨c1,Normal s⟩ → r"
        have "Γ⊨c2 ↓ r"
        proof (cases r)
          case (Normal r')
          with cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
          have r: "r∈Normal ` R"
            by auto
          with cvalidt_termD [OF valid_c2 ctxt] exec_c1
          show "Γ⊨c2 ↓ r"
            by auto
        qed auto
      }
      ultimately show ?thesis
        by (iprover intro: terminates.intros)
    qed
  qed
next
  case (Cond Θ F P b c1 Q A c2)
  have valid_c1: "Γ,Θ ⊨<sub>tF</sub> (P ∩ b) c1 Q,A" by fact
  have valid_c2: "Γ,Θ ⊨<sub>tF</sub> (P ∩ - b) c2 Q,A" by fact
  show "Γ,Θ ⊨<sub>tF</sub> P Cond b c1 c2 Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨<sub>tF</sub> P (Call p) Q,A"
    assume exec: "Γ⊨⟨Cond b c1 c2,Normal s⟩ → 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⟩ → t"
        by cases auto
      with P True
      show ?thesis
        by - (rule cvalidt_postD [OF valid_c1 ctxt _ _ t_notin_F],auto)
    next
      case False
      with exec P have "Γ⊨⟨c2,Normal s⟩ → t"
        by cases auto
      with P False
      show ?thesis
        by - (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F],auto)
    qed
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume P: "s ∈ P"
    thus "Γ⊨Cond b c1 c2 ↓ Normal s"
      using cvalidt_termD [OF valid_c1 ctxt] cvalidt_termD [OF valid_c2 ctxt]
      by (cases "s ∈ b") (auto intro: terminates.intros)
  qed
next
  case (While r Θ F P b c A)
  assume wf: "wf r"
  have valid_c: "∀σ. Γ,Θ⊨_tF ({σ} ∩ P ∩ b) c ({t. (t, σ) ∈ r} ∩ P),A"
    using While.hyps by iprover
  show "Γ,Θ ⊨_tF P (While b c) (P ∩ - b),A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    assume wprems: "Γ⊨⟨While b c,Normal s⟩ → t" "s ∈ P" "t ∉ Fault ` F"
    from wf
    have "∧t. [Γ⊨⟨While b c,Normal s⟩ → t; s ∈ P; t ∉ Fault ` F]
                 ==> t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
    proof (induct)
      fix s t
      assume hyp:
        "∧s' t. [(s',s)∈r; Γ⊨⟨While b c,Normal s'⟩ → t; s' ∈ P; t ∉ Fault ` F]
                 ==> t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
      assume exec: "Γ⊨⟨While b c,Normal s⟩ → t"
      assume P: "s ∈ P"
      assume t_notin_F: "t ∉ Fault ` F"
      from exec
      show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
      proof (cases)
        fix s'
        assume b: "s∈b"
        assume exec_c: "Γ⊨⟨c,Normal s⟩ → s'"
        assume exec_w: "Γ⊨⟨While b c,s'⟩ → t"
        from exec_w t_notin_F have "s' ∉ Fault ` F"
          by (auto dest: Fault_end)
        from exec_c P b valid_c ctxt this
        have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P) ∪ Abrupt ` A"
          by (auto simp add: cvalidt_def validt_def valid_def)
        show ?thesis
        proof (cases s')
          case Normal
          with exec_w s' t_notin_F
          show ?thesis
            by - (rule hyp,auto)
        next
          case Abrupt
          with exec_w have "t=s'"
            by (auto dest: Abrupt_end)
          with Abrupt s' show ?thesis
            by blast
        next
          case Fault
          with exec_w have "t=s'"
            by (auto dest: Fault_end)
          with Fault s' show ?thesis
            by blast
        next
          case Stuck
          with exec_w have "t=s'"
            by (auto dest: Stuck_end)
          with Stuck s' show ?thesis
            by blast
        qed
      next
        assume "s∉b" "t=Normal s" with P show ?thesis by simp
      qed
    qed
    with wprems show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" by blast
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨<sub>tF</sub> P (Call p) Q,A"
    assume "s ∈ P"
    with wf
    show "Γ⊨While b c ↓ Normal s"
    proof (induct)
      fix s
      assume hyp: "∧s'. [(s',s)∈r; s' ∈ P]
                         ==> Γ⊨While b c ↓ Normal s'"
      assume P: "s ∈ P"
      show "Γ⊨While b c ↓ Normal s"
      proof (cases "s ∈ b")
        case False with P show ?thesis
          by (blast intro: terminates.intros)
      next
        case True
        with valid_c P ctxt
        have "Γ⊨c ↓ Normal s"
          by (simp add: cvalidt_def validt_def)
        moreover
        {
          fix s'
          assume exec_c: "Γ⊨⟨c,Normal s⟩ → s'"
          have "Γ⊨While b c ↓ s'"
          proof (cases s')
            case (Normal s'')
            with exec_c P True valid_c ctxt
            have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P)"
              by (fastforce simp add: cvalidt_def validt_def valid_def)
            then show ?thesis
              by (blast intro: hyp)
          qed auto
        }
        ultimately
        show ?thesis
          by (blast intro: terminates.intros)
      qed
    qed
  qed
next
  case (Guard Θ F g P c Q A  f)
  have valid_c: "Γ,Θ ⊨_tF (g ∩ P) c Q,A" by fact
  show "Γ,Θ ⊨_tF (g ∩ P) Guard f g c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume exec: "Γ⊨⟨Guard f g c,Normal s⟩ → t"
    assume t_notin_F: "t ∉ Fault ` F"
    assume P:"s ∈ (g ∩ P)"
    from exec P have "Γ⊨⟨c,Normal s⟩ → t"
      by cases auto
    from valid_c ctxt this P t_notin_F
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by (rule cvalidt_postD)
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨<sub>tF</sub> P (Call p) Q,A"
    assume P:"s ∈ (g ∩ P)"
    thus "Γ⊨Guard f g c ↓ Normal s"
      by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
  qed
next
  case (Guarantee f F Θ g P c Q A)
  have valid_c: "Γ,Θ ⊨<sub>tF</sub> (g ∩ P) c Q,A" by fact
  have f_F: "f ∈ F" by fact
  show "Γ,Θ ⊨<sub>tF</sub> P Guard f g c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨<sub>tF</sub> P (Call p) Q,A"
    assume exec: "Γ⊨⟨Guard f g c,Normal s⟩ → 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 g have "Γ⊨⟨c,Normal s⟩ → t"
      by cases auto
    from valid_c ctxt this P' t_notin_F
    show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by (rule cvalidt_postD)
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume P:"s ∈ P"
    thus "Γ⊨Guard f g c ↓ Normal s"
      by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
  qed
next
  case (CallRec P p Q A Specs r Specs_wf Θ  F)
  have p: "(P,p,Q,A) ∈ Specs"  by fact
  have wf: "wf r" by fact
  have Specs_wf:
    "Specs_wf = (λp τ. (λ(P,q,Q,A). (P ∩ {s. ((s, q),τ,p) ∈ r},q,Q,A)) ` Specs)" by fact
  from CallRec.hyps
  have valid_body:
    "∀(P, p, Q, A)∈Specs. p ∈ dom Γ ∧
        (∀τ. Γ,Θ ∪ Specs_wf p τ⊨<sub>tF</sub> ({τ} ∩ P) the (Γ p) Q,A)" by auto
  show "Γ,Θ ⊨<sub>tF</sub> P (Call p) Q,A"
  proof -
    {
      fix τp
      assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨<sub>tF</sub> P (Call p) Q,A"
      from wf
      have "∧τ p P Q A. [τp = (τ,p); (P,p,Q,A) ∈ Specs] ==>
                  Γ⊨<sub>tF</sub> ({τ} ∩ P) (the (Γ (p))) Q,A"
      proof (induct τp rule: wf_induct [rule_format, consumes 1, case_names WF])
        case (WF τp τ p P Q A)
        have τp: "τp = (τ, p)" by fact
        have p: "(P, p, Q, A) ∈ Specs" by fact
        {
          fix q P' Q' A'
          assume q: "(P',q,Q',A') ∈ Specs"
          have "Γ⊨<sub>tF</sub> (P' ∩ {s. ((s,q), τ,p) ∈ r}) (Call q) Q',A'"
          proof (rule validtI)
            fix s t
            assume exec_q:
              "Γ⊨⟨Call q,Normal s⟩ → t"
            assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}"
            assume t_notin_F: "t ∉ Fault ` F"
            from Pre q τp
            have valid_bdy:
              "Γ⊨_tF ({s} ∩ P') the (Γ q) Q',A'"
              by - (rule WF.hyps, auto)
            from Pre q
            have Pre': "s ∈ {s} ∩ P'"
              by auto
            from exec_q show "t ∈ Normal ` Q' ∪ Abrupt ` A'"
            proof (cases)
              fix bdy
              assume bdy: "Γ q = Some bdy"
              assume exec_bdy: "Γ⊨⟨bdy,Normal s⟩ → t"
              from valid_bdy [simplified bdy option.sel]  t_notin_F exec_bdy Pre'
              have "t ∈ Normal ` Q' ∪ Abrupt ` A'"
                by (auto simp add: validt_def valid_def)
              with Pre q
              show ?thesis
                by auto
            next
              assume "Γ q = None"
              with q valid_body have False by auto
              thus ?thesis ..
            qed
          next
            fix s
            assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}"
            from Pre q τp
            have valid_bdy:
              "Γ ⊨_tF ({s} ∩ P') (the (Γ q)) Q',A'"
              by - (rule WF.hyps, auto)
            from Pre q
            have Pre': "s ∈ {s} ∩ P'"
              by auto
            from valid_bdy ctxt Pre'
            have "Γ⊨the (Γ q) ↓ Normal s"
              by (auto simp add: validt_def)
            with valid_body q
            show "Γ⊨Call q↓ Normal s"
              by (fastforce intro: terminates.Call)
          qed
        }
        hence "∀(P, p, Q, A)∈Specs_wf p τ. Γ⊨_tF P Call p Q,A"
          by (auto simp add: cvalidt_def Specs_wf)
        with ctxt have "∀(P, p, Q, A)∈Θ ∪ Specs_wf p τ. Γ⊨_tF P Call p Q,A"
          by auto
        with p valid_body
        show "Γ ⊨_tF ({τ} ∩ P) (the (Γ p)) Q,A"
          by (simp add: cvalidt_def) blast
      qed
    }
    note lem = this
    have valid_body':
      "∧τ. ∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A ==>
      ∀(P,p,Q,A)∈Specs. Γ⊨_tF ({τ} ∩ P) (the (Γ p)) Q,A"
      by (auto intro: lem)
    show "Γ,Θ ⊨_tF P (Call p) Q,A"
    proof (rule cvalidtI)
      fix s t
      assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
      assume exec_call: "Γ⊨⟨Call p,Normal s⟩ → t"
      assume P: "s ∈ P"
      assume t_notin_F: "t ∉ Fault ` F"
      from exec_call show "t ∈ Normal ` Q ∪ Abrupt ` A"
      proof (cases)
        fix bdy
        assume bdy: "Γ p = Some bdy"
        assume exec_body: "Γ⊨⟨bdy,Normal s⟩ → t"
        from exec_body bdy p P t_notin_F
          valid_body' [of "s", OF ctxt]
          ctxt
        have "t ∈ Normal ` Q ∪ Abrupt ` A"
          apply (simp only: cvalidt_def validt_def valid_def)
          apply (drule (1) bspec)
          apply auto
          done
        with p P
        show ?thesis
          by simp
      next
        assume "Γ p = None"
        with p valid_body have False by auto
        thus ?thesis by simp
      qed
    next
      fix s
      assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨<sub>tF</sub> P (Call p) Q,A"
      assume P: "s ∈ P"
      show "Γ⊨Call p ↓ Normal s"
      proof -
        from ctxt P p valid_body' [of "s",OF ctxt]
        have "Γ⊨(the (Γ p)) ↓ Normal s"
          by (auto simp add: cvalidt_def validt_def)
        with valid_body p show ?thesis
          by (fastforce intro: terminates.Call)
      qed
    qed
  qed
next
  case (DynCom P Θ F c Q A)
  hence valid_c: "∀s∈P. Γ,Θ⊨<sub>tF</sub> P (c s) Q,A" by simp
  show "Γ,Θ⊨<sub>tF</sub> P DynCom c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨<sub>tF</sub> P (Call p) Q,A"
    assume exec: "Γ⊨⟨DynCom c,Normal s⟩ → t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases)
      assume "Γ⊨⟨c s,Normal s⟩ → t"
      from cvalidt_postD [OF valid_c [rule_format, OF P] ctxt this P t_notin_F]
      show ?thesis .
    qed
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    assume P: "s ∈ P"
    show "Γ⊨DynCom c ↓ Normal s"
    proof -
      from cvalidt_termD [OF valid_c [rule_format, OF P] ctxt P]
      have "Γ⊨c s ↓ Normal s" .
      thus ?thesis
        by (rule terminates.intros)
    qed
  qed
next
  case (Throw Θ F A Q)
  show "Γ,Θ ⊨_tF A Throw Q,A"
  proof (rule cvalidtI)
    fix s t
    assume "Γ⊨⟨Throw,Normal s⟩ → t" "s ∈ A"
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"
      by cases simp
  next
    fix s
    show "Γ⊨Throw ↓ Normal s"
      by (rule terminates.intros)
  qed
next
  case (Catch Θ F P c₁ Q R c₂ A)
  have valid_c1: "Γ,Θ ⊨_tF P c₁ Q,R" by fact
  have valid_c2: "Γ,Θ ⊨_tF R c₂ Q,A" by fact
  show "Γ,Θ ⊨_tF P Catch c₁ c₂ Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume exec: "Γ⊨⟨Catch c₁ c₂,Normal s⟩ → t"
    assume P: "s ∈ P"
    assume t_notin_F: "t ∉ Fault ` F"
    from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases)
      fix s'
      assume exec_c1: "Γ⊨⟨c<sub>1</sub>,Normal s⟩ → Abrupt s'"
      assume exec_c2: "Γ⊨⟨c<sub>2</sub>,Normal s'⟩ → t"
      from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
      have "Abrupt s' ∈ Abrupt ` R"
        by auto
      with cvalidt_postD [OF valid_c2 ctxt] exec_c2 t_notin_F
      show ?thesis
        by fastforce
    next
      assume exec_c1: "Γ⊨⟨c₁,Normal s⟩ → t"
      assume notAbr: "¬ isAbr t"
      from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] t_notin_F
      have "t ∈ Normal ` Q ∪ Abrupt ` R" .
      with notAbr
      show ?thesis
        by auto
    qed
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume P: "s ∈ P"
    show "Γ⊨Catch c₁ c₂ ↓ Normal s"
    proof -
      from valid_c1 ctxt P
      have "Γ⊨c₁↓ Normal s"
        by (rule cvalidt_termD)
      moreover
      {
        fix r assume exec_c1: "Γ⊨⟨c₁,Normal s⟩ → Abrupt r"
        from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
        have r: "Abrupt r∈Normal ` Q ∪ Abrupt ` R"
          by auto
        hence "Abrupt r∈Abrupt ` R" by fast
        with cvalidt_termD [OF valid_c2 ctxt] exec_c1
        have "Γ⊨c<sub>2</sub> ↓ Normal r"
          by fast
      }
      ultimately show ?thesis
        by (iprover intro: terminates.intros)
    qed
  qed
next
  case (Conseq P Θ F c Q A)
  hence adapt:
    "∀s ∈ P. (∃P' Q' A'. (Γ,Θ ⊨<sub>tF</sub> P' c Q',A') ∧ s ∈ P'∧ Q' ⊆ Q ∧ A' ⊆ A)" by blast
  show "Γ,Θ ⊨<sub>tF</sub> P c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨<sub>tF</sub> P (Call p) Q,A"
    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 adapt [rule_format, OF P]
      obtain P' and Q' and A' where
        valid_P'_Q': "Γ,Θ ⊨_tF P' c Q',A'"
        and weaken: "s ∈ P'" "Q' ⊆ Q" "A'⊆ A"
        by blast
      from exec valid_P'_Q' ctxt t_notin_F
      have P'_Q': "Normal s ∈ Normal ` P' ⟶
        t ∈ Normal ` Q' ∪ Abrupt ` A'"
        by (unfold cvalidt_def validt_def valid_def) blast
      hence "s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'"
        by blast
      with weaken
      show ?thesis
        by blast
    qed
  next
    fix s
    assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
    assume P: "s ∈ P"
    show "Γ⊨c ↓ Normal s"
    proof -
      from P adapt
      obtain P' and Q' and  A' where
        "Γ,Θ ⊨_tF P' c Q',A'"
        "s ∈ P'"
        by blast
      with ctxt
      show ?thesis
        by (simp add: cvalidt_def validt_def)
    qed
  qed
next
  case (Asm P p Q A Θ F)
  assume "(P, p, Q, A) ∈ Θ"
  then show "Γ,Θ ⊨_tF P (Call p) Q,A"
    by (auto simp add: cvalidt_def )
next
  case ExFalso thus ?case by iprover
qed

lemma hoaret_sound':
"Γ,{}⊨_tF P c Q,A ==> Γ⊨_tF P c Q,A"
  apply (drule hoaret_sound)
  apply (simp add: cvalidt_def)
  done

theorem total_to_partial:
 assumes total: "Γ,{}⊨_tF P c Q,A" shows "Γ,{}⊨_F P c Q,A"
proof -
  from total have "Γ,{}⊨_tF P c Q,A"
    by (rule hoaret_sound)
  hence "Γ⊨_F P c Q,A"
    by (simp add: cvalidt_def validt_def cvalid_def)
  thus ?thesis
    by (rule hoare_complete)
qed

subsection ‹Completeness›

lemma MGT_valid:
"Γ⊨_tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c
    {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
proof (rule validtI)
  fix s t
  assume "Γ⊨⟨c,Normal s⟩ → t"
         "s ∈ {s. s = Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s}"
         "t ∉ Fault ` F"
  thus "t ∈ Normal ` {t. Γ⊨⟨c,Normal Z⟩ → Normal t} ∪
            Abrupt ` {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
    apply (cases t)
    apply (auto simp add: final_notin_def)
    done
next
  fix s
  assume "s ∈ {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s}"
  thus "Γ⊨c↓Normal s"
    by blast
qed

text ‹The consequence rule where the existential @{term Z} is instantiated
  @{term s}. Usefull in proof of ‹MGT_lemma›.›
lemma ConseqMGT:
  assumes modif: "∀Z::'a. Γ,Θ ⊨_tF (P' Z::'a assn) 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 "Γ,Θ ⊨_tF P c Q,A"
using impl
by - (rule conseq [OF modif],blast)

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

lemma conseq_extract_state_indep_prop:
  assumes state_indep_prop:"∀s ∈ P. R"
  assumes to_show: "R ==> Γ,Θ⊨_tF P c Q,A"
  shows "Γ,Θ⊨_tF 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. Γ,Θ ⊨_tF
       {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
           Γ⊨(Call p)↓Normal s}
             (Call p)
       {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
       {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}"
  shows "∧Z. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                          Γ⊨c↓Normal s}
               c
             {t. Γ⊨⟨c,Normal Z⟩ → Normal t},{t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
proof (induct c)
  case Skip
  show "Γ,Θ⊨_tF {s. s = Z ∧ Γ⊨⟨Skip,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Skip ↓ Normal s}
               Skip
            {t. Γ⊨⟨Skip,Normal Z⟩ → Normal t},{t. Γ⊨⟨Skip,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Skip [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def
             intro: exec.intros terminates.intros)
next
  case (Basic f)
  show "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Basic f,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Basic f ↓ Normal s}
                Basic f
              {t. Γ⊨⟨Basic f,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Basic f,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Basic [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def
             intro: exec.intros terminates.intros)
next
  case (Spec r)
  show "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨Spec r,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Spec r ↓ Normal s}
                Spec r
              {t. Γ⊨⟨Spec r,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Spec r,Normal Z⟩ → Abrupt t}"
    apply (rule hoaret.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. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                                Γ⊨c1↓Normal s}
                            c1
                           {t. Γ⊨⟨c1,Normal Z⟩ → Normal t},
                           {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}"
    using Seq.hyps by iprover
  have hyp_c2: "∀ Z. Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                                 Γ⊨c2↓Normal s}
                              c2
                            {t. Γ⊨⟨c2,Normal Z⟩ → Normal t},
                            {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}"
    using Seq.hyps by iprover
  from hyp_c1
  have "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                Γ⊨Seq c1 c2↓Normal s} c1
    {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧ Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
        Γ⊨c2↓Normal t},
    {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule ConseqMGT)
       (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
             elim: terminates_Normal_elim_cases
             intro: exec.intros)
  thus "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Seq c1 c2↓Normal s}
                Seq c1 c2
              {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}"
  proof (rule hoaret.Seq )
    show "Γ,Θ⊨_tF {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧
                    Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2 ↓ Normal t}
                 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 (rule 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 (rule exec.intros)
    qed
  qed
next
  case (Cond b c1 c2)
  have "∀Z. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                         Γ⊨c1↓Normal s}
                     c1
                   {t. Γ⊨⟨c1,Normal Z⟩ → Normal t},
                   {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ ⊨_tF ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨(Cond b c1 c2)↓Normal s}∩b)
                c1
                {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule ConseqMGT)
       (fastforce simp add: final_notin_def intro: exec.CondTrue
                 elim: terminates_Normal_elim_cases)
  moreover
  have "∀Z. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                               Γ⊨c2↓Normal s}
                      c2
                    {t. Γ⊨⟨c2,Normal Z⟩ → Normal t},
                    {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ⊨_tF ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨(Cond b c1 c2)↓Normal s}∩-b)
                c2
                {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule ConseqMGT)
       (fastforce simp add: final_notin_def intro: exec.CondFalse
                 elim: terminates_Normal_elim_cases)
  ultimately
  show "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
               Γ⊨(Cond b c1 c2)↓Normal s}
               (Cond b c1 c2)
              {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.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)) ∧
                    Γ⊨(While b c)↓Normal t}"
  let ?A = "λZ. {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}"
  let ?r = "{(t,s). Γ⊨(While b c)↓Normal s ∧ s∈b ∧
                    Γ⊨⟨c,Normal s⟩ → Normal t}"
  show "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨While b c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨(While b c)↓Normal s}
              (While b c)
              {t. Γ⊨⟨While b c,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z"
                         and ?Q'="λ Z. ?P' Z ∩ - b"])
    have wf_r: "wf ?r" by (rule wf_terminates_while)
    show "∀ Z. Γ,Θ⊨_tF (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)"
    proof (rule allI, rule hoaret.While [OF wf_r])
      fix Z
      from While
      have hyp_c: "∀Z. Γ,Θ⊨_tF{s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                                  Γ⊨c↓Normal s}
                                c
                              {t. Γ⊨⟨c,Normal Z⟩ → Normal t},
                              {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" by iprover
      show "∀σ. Γ,Θ⊨<sub>tF</sub> ({σ} ∩ ?P' Z ∩ b) c
                       ({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)"
      proof (rule allI, rule ConseqMGT [OF hyp_c])
        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)) ∧
                      Γ⊨(While b c)↓Normal t}
                   ∩ b"
        then obtain
          s_eq_σ: "s=σ" and
          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
          while_term:  "Γ⊨(While b c)↓Normal s" and
          s_in_b: "s∈b"
          by blast
        show "s ∈ {t. t = s ∧ Γ⊨⟨c,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                       Γ⊨c↓Normal t} ∧
        (∀t. t ∈ {t. Γ⊨⟨c,Normal s⟩ → Normal t} ⟶
             t ∈ {t. (t,σ) ∈ ?r} ∩
                 {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)) ∧
                      Γ⊨(While b c)↓Normal t}) ∧
         (∀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 while_term show ?C1
            by (blast elim: terminates_Normal_elim_cases)
        next
          {
            fix t
            assume s_t: "Γ⊨⟨c,Normal s⟩ → Normal t"
            with s_eq_σ while_term s_in_b have "(t,σ) ∈ ?r"
              by blast
            moreover
            from Z_s_unroll s_t s_in_b
            have "(Z, t) ∈ ?unroll"
              by (blast intro: rtrancl_into_rtrancl)
            moreover from while_term s_t s_in_b
            have "Γ⊨(While b c)↓Normal t"
              by (blast elim: terminates_Normal_elim_cases)
            moreover note noabort
            ultimately
            have "(t,σ) ∈ ?r ∧ (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)) ∧
                  Γ⊨(While b c)↓Normal t"
              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)) ∧
                       Γ⊨While b c ↓ Normal s}"
    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)
  from noStuck_Call
  have "∀s ∈ {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                         Γ⊨Call p↓ Normal s}.
          p ∈ dom Γ"
    by (fastforce simp add: final_notin_def)
  then show ?case
  proof (rule conseq_extract_state_indep_prop)
    assume p_defined: "p ∈ dom Γ"
    with MGT_Calls show
    "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧
                 Γ⊨⟨Call p ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F))∧
                 Γ⊨Call p↓Normal s}
                (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. Γ,Θ⊨_tF {s. s = Z ∧ Γ⊨⟨c s',Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                       Γ⊨c s'↓Normal s} c s'
      {t. Γ⊨⟨c s',Normal Z⟩ → Normal t},{t. Γ⊨⟨c s',Normal Z⟩ → Abrupt t}"
    using DynCom by simp
  have hyp':
  "Γ,Θ⊨<sub>tF</sub> {s. s = Z ∧ Γ⊨⟨DynCom c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
            Γ⊨DynCom c↓Normal s}
         (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
          elim: terminates_Normal_elim_cases)
  show "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨DynCom c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨DynCom c↓Normal s}
                DynCom c
             {t. Γ⊨⟨DynCom c,Normal Z⟩ → Normal t},
             {t. Γ⊨⟨DynCom c,Normal Z⟩ → Abrupt t}"
    apply (rule hoaret.DynCom)
    apply (clarsimp)
    apply (rule hyp' [simplified])
    done
next
  case (Guard f g c)
  have hyp_c: "∀Z. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                              Γ⊨c↓Normal s}
                     c
                   {t. Γ⊨⟨c,Normal Z⟩ → Normal t},
                   {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
    using Guard by iprover
  show "Γ,Θ⊨_tF {s. s = Z ∧ Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Guard f g c↓ Normal s}
                Guard f g c
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Abrupt t}"
  proof (cases "f ∈ F")
    case True
    from hyp_c
    have "Γ,Θ⊨<sub>tF</sub> (g ∩ {s. s=Z ∧
                     Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck}∪ Fault ` (-F))∧
                     Γ⊨Guard f g c↓ Normal s})
                   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
                   elim: terminates_Normal_elim_cases)
      done
    from True this
    show ?thesis
      by (rule conseqPre [OF Guarantee]) auto
  next
    case False
    from hyp_c
    have "Γ,Θ⊨_tF (g ∩ {s. s ∈ g ∧ s=Z ∧
                     Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck}∪ Fault ` (-F))∧
                     Γ⊨Guard f g c↓ Normal s} )
                   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
                   elim: terminates_Normal_elim_cases)
      done
    then show ?thesis
      apply (rule conseqPre [OF hoaret.Guard])
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply auto
      done
  qed
next
  case Throw
  show "Γ,Θ⊨<sub>tF</sub> {s. s = Z ∧ Γ⊨⟨Throw,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Throw ↓ Normal s}
              Throw
              {t. Γ⊨⟨Throw,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Throw,Normal Z⟩ → Abrupt t}"
    by (rule conseqPre [OF hoaret.Throw])
       (blast intro: exec.intros terminates.intros)
next
  case (Catch c₁ c₂)
  have "∀Z. Γ,Θ⊨_tF {s. s = Z ∧ Γ⊨⟨c₁,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                        Γ⊨c<sub>1</sub> ↓ Normal s}
                    c<sub>1</sub>
                  {t. Γ⊨⟨c<sub>1</sub>,Normal Z⟩ → Normal t},
                  {t. Γ⊨⟨c<sub>1</sub>,Normal Z⟩ → Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊨<sub>tF</sub> {s. s = Z ∧ Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Catch c₁ c₂ ↓ Normal s}
                c₁
               {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨c₁,Normal Z⟩ → Abrupt t ∧ Γ⊨c₂ ↓ Normal t ∧
                   Γ⊨⟨c₂,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F))}"
    by (rule ConseqMGT)
       (fastforce intro: exec.intros terminates.intros
                 elim: terminates_Normal_elim_cases
                 simp add: final_notin_def)
  moreover
  have
    "∀Z. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c<sub>2</sub>,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨c₂ ↓ Normal s} c₂
                  {t. Γ⊨⟨c₂,Normal Z⟩ → Normal t},
                  {t. Γ⊨⟨c₂,Normal Z⟩ → Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊨_tF {s. Γ⊨⟨c₁,Normal Z⟩ →Abrupt s ∧ Γ⊨c₂ ↓ Normal s ∧
                   Γ⊨⟨c₂,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F))}
               c<sub>2</sub>
               {t. Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal Z⟩ → Abrupt t}"
      by (rule ConseqMGT)
         (fastforce intro: exec.intros terminates.intros
                   simp add: noFault_def')
  ultimately
  show "Γ,Θ⊨<sub>tF</sub> {s. s = Z ∧ Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Catch c₁ c₂ ↓ Normal s}
                Catch c₁ c₂
               {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Catch )
qed


lemma Call_lemma':
 assumes Call_hyp:
 "∀q∈dom Γ. ∀Z. Γ,Θ⊨_tF{s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                       Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
                 (Call q)
                {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}"
 shows "∧Z. Γ,Θ ⊨<sub>tF</sub>
      {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ c ∈ redexes c')}
              c
      {t. Γ⊨⟨c,Normal Z⟩ → Normal t},
      {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
proof (induct c)
  case Skip
  show "Γ,Θ⊨_tF {s. s = Z ∧ Γ⊨⟨Skip,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Call p ↓ Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ Skip ∈ redexes c')}
               Skip
              {t. Γ⊨⟨Skip,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Skip,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip)
next
  case (Basic f)
  show "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Basic f,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Call p↓Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                      Basic f ∈ redexes c')}
               Basic f
              {t. Γ⊨⟨Basic f,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Basic f,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic)
next
  case (Spec r)
  show "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨Spec r,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Call p↓Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧
                 Spec r ∈ redexes c')}
               Spec r
              {t. Γ⊨⟨Spec r,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Spec r,Normal Z⟩ → Abrupt t}"
    apply (rule hoaret.Spec [THEN conseqPre])
    apply (clarsimp)
    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. Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨Call p↓Normal σ ∧
                 (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ c1 ∈ redexes c')}
                c1
               {t. Γ⊨⟨c1,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}"
    using Seq.hyps by iprover
  have hyp_c2:
    "∀Z. Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call p↓Normal σ ∧
                 (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ c2 ∈ redexes c')}
                c2
               {t. Γ⊨⟨c2,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}"
    using Seq.hyps (2) by iprover
  have c1: "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call p↓Normal σ ∧
              (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                    Seq c1 c2 ∈ redexes c')}
               c1
               {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧
                   Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                   Γ⊨Call p↓Normal σ ∧
                  (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal t) ∧
                        c2 ∈ redexes c')},
               {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
    assume "Γ⊨⟨Seq c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
    thus "Γ⊨⟨c1,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (blast dest: Seq_NoFaultStuckD1)
  next
    fix c'
    assume steps_c': "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
    assume red: "Seq c1 c2 ∈ redexes c'"
    from redexes_subset [OF red] steps_c'
    show "∃c'. Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z) ∧ c1 ∈ redexes c'"
      by (auto iff: root_in_redexes)
  next
    fix t
    assume "Γ⊨⟨Seq c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
            "Γ⊨⟨c1,Normal Z⟩ → Normal t"
    thus "Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (blast dest: Seq_NoFaultStuckD2)
  next
    fix c' t
    assume steps_c': "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
    assume red: "Seq c1 c2 ∈ redexes c'"
    assume exec_c1: "Γ⊨ ⟨c1,Normal Z⟩ → Normal t"
    show "∃c'. Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal t) ∧ c2 ∈ redexes c'"
    proof -
      note steps_c'
      also
      from exec_impl_steps_Normal [OF exec_c1]
      have "Γ⊨ (c1, Normal Z) →<sup>*</sup> (Skip, Normal t)".
      from steps_redexes_Seq [OF this red]
      obtain c'' where
        steps_c'': "Γ⊨ (c', Normal Z) →<sup>*</sup> (c'', Normal t)" and
        Skip: "Seq Skip c2 ∈ redexes c''"
        by blast
      note steps_c''
      also
      have step_Skip: "Γ⊨ (Seq Skip c2,Normal t) → (c2,Normal t)"
        by (rule step.SeqSkip)
      from step_redexes [OF step_Skip Skip]
      obtain c''' where
        step_c''': "Γ⊨ (c'', Normal t) → (c''', Normal t)" and
        c2: "c2 ∈ redexes c'''"
        by blast
      note step_c'''
      finally show ?thesis
        using c2
        by blast
    qed
  next
    fix t
    assume "Γ⊨⟨c1,Normal Z⟩ → Abrupt t"
    thus "Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t"
      by (blast intro: exec.intros)
  qed
  show "Γ,Θ⊨<sub>tF</sub> {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨Call p↓Normal σ ∧
              (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ Seq c1 c2 ∈ redexes c')}
              Seq c1 c2
              {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]])
       (blast intro: exec.intros)
next
  case (Cond b c1 c2)
  have hyp_c1:
       "∀Z. Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                        Γ⊨Call p↓Normal σ ∧
                    (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ c1 ∈ redexes c')}
                   c1
                  {t. Γ⊨⟨c1,Normal Z⟩ → Normal t},
                  {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}"
    using Cond.hyps by iprover
  have
  "Γ,Θ⊨<sub>tF</sub> ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
           Γ⊨Call p↓Normal σ ∧
           (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                 Cond b c1 c2 ∈ redexes c')}
           ∩ b)
           c1
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [OF hyp_c1],safe)
    assume "Z ∈ b" "Γ⊨⟨Cond b c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
    thus "Γ⊨⟨c1,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (auto simp add: final_notin_def intro: exec.CondTrue)
  next
    fix c'
    assume b: "Z ∈ b"
    assume steps_c': "Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z)"
    assume redex_c': "Cond b c1 c2 ∈ redexes c'"
    show "∃c'. Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z) ∧ c1 ∈ redexes c'"
    proof -
      note steps_c'
      also
      from b
      have "Γ⊨(Cond b c1 c2, Normal Z) → (c1, Normal Z)"
        by (rule step.CondTrue)
      from step_redexes [OF this redex_c'] obtain c'' where
        step_c'': "Γ⊨ (c', Normal Z) → (c'', Normal Z)" and
        c1: "c1 ∈ redexes c''"
        by blast
      note step_c''
      finally show ?thesis
        using c1
        by blast
    qed
  next
    fix t assume "Z ∈ b" "Γ⊨⟨c1,Normal Z⟩ → Normal t"
    thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t"
      by (blast intro: exec.CondTrue)
  next
    fix t assume "Z ∈ b" "Γ⊨⟨c1,Normal Z⟩ → Abrupt t"
    thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t"
      by (blast intro: exec.CondTrue)
  qed
  moreover
  have hyp_c2:
       "∀Z. Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨Call p↓Normal σ ∧
                    (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ c2 ∈ redexes c')}
                   c2
                  {t. Γ⊨⟨c2,Normal Z⟩ → Normal t},
                  {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}"
    using Cond.hyps by iprover
  have
  "Γ,Θ⊨<sub>tF</sub> ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
              Γ⊨Call p↓Normal σ ∧
           (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c', Normal s) ∧
                 Cond b c1 c2 ∈ redexes c')}
           ∩ -b)
           c2
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [OF hyp_c2],safe)
    assume "Z ∉ b" "Γ⊨⟨Cond b c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
    thus "Γ⊨⟨c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (auto simp add: final_notin_def intro: exec.CondFalse)
  next
    fix c'
    assume b: "Z ∉ b"
    assume steps_c': "Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z)"
    assume redex_c': "Cond b c1 c2 ∈ redexes c'"
    show "∃c'. Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z) ∧ c2 ∈ redexes c'"
    proof -
      note steps_c'
      also
      from b
      have "Γ⊨(Cond b c1 c2, Normal Z) → (c2, Normal Z)"
        by (rule step.CondFalse)
      from step_redexes [OF this redex_c'] obtain c'' where
        step_c'': "Γ⊨ (c', Normal Z) → (c'', Normal Z)" and
        c1: "c2 ∈ redexes c''"
        by blast
      note step_c''
      finally show ?thesis
        using c1
        by blast
    qed
  next
    fix t assume "Z ∉ b" "Γ⊨⟨c2,Normal Z⟩ → Normal t"
    thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t"
      by (blast intro: exec.CondFalse)
  next
    fix t assume "Z ∉ b" "Γ⊨⟨c2,Normal Z⟩ → Abrupt t"
    thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t"
      by (blast intro: exec.CondFalse)
  qed
  ultimately
  show
   "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
              Γ⊨Call p↓Normal σ ∧
           (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧
                 Cond b c1 c2 ∈ redexes c')}
           (Cond b c1 c2)
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}"
    by (rule hoaret.Cond)
next
  case (While b c)
  let ?unroll = "({(s,t). s∈b ∧ Γ⊨⟨c,Normal s⟩ → Normal t})<sup>*</sup>"
  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)) ∧
                    Γ⊨Call p↓Normal σ ∧
                  (∃c'. Γ⊨(Call p,Normal σ) →⁺
                               (c',Normal t) ∧ While b c ∈ redexes c')}"
  let ?A = "λZ. {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}"
  let ?r = "{(t,s). Γ⊨(While b c)↓Normal s ∧ s∈b ∧
                    Γ⊨⟨c,Normal s⟩ → Normal t}"
  show "Γ,Θ⊨_tF
       {s. s=Z ∧ Γ⊨⟨While b c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Call p↓Normal σ ∧
          (∃c'. Γ⊨(Call p,Normal σ)→<sup>+</sup>(c',Normal s) ∧ While b c ∈ redexes c')}
         (While b c)
       {t. Γ⊨⟨While b c,Normal Z⟩ → Normal t},
       {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z"
                         and ?Q'="λ Z. ?P' Z ∩ - b"])
    have wf_r: "wf ?r" by (rule wf_terminates_while)
    show "∀ Z. Γ,Θ⊨<sub>tF</sub> (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)"
    proof (rule allI, rule hoaret.While [OF wf_r])
      fix Z
      from While
      have hyp_c: "∀Z. Γ,Θ⊨<sub>tF</sub>
            {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                Γ⊨Call p↓Normal σ ∧
               (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ c ∈ redexes c')}
              c
            {t. Γ⊨⟨c,Normal Z⟩ → Normal t},
            {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" by iprover
      show "∀σ. Γ,Θ⊨_tF ({σ} ∩ ?P' Z ∩ b) c
                       ({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)"
      proof (rule allI, rule ConseqMGT [OF hyp_c])
        fix τ s
        assume  asm: "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)) ∧
                     Γ⊨Call p↓ Normal σ ∧
                     (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup>
                                  (c',Normal t) ∧ While b c ∈ redexes c')}
                   ∩ b"
        then obtain c' where
          s_eq_τ: "s=τ" and
          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
          termi:  "Γ⊨Call p ↓ Normal σ" and
          reach: "Γ⊨(Call p,Normal σ) →⁺ (c',Normal s)" and
          red_c': "While b c ∈ redexes c'" and
          s_in_b: "s∈b"
          by blast
        obtain c'' where
          reach_c: "Γ⊨(Call p,Normal σ) →⁺ (c'',Normal s)"
                   "Seq c (While b c) ∈ redexes c''"
        proof -
          note reach
          also from s_in_b
          have "Γ⊨(While b c,Normal s) → (Seq c (While b c),Normal s)"
            by (rule step.WhileTrue)
          from step_redexes [OF this red_c'] obtain c'' where
            step: "Γ⊨ (c', Normal s) → (c'', Normal s)" and
            red_c'': "Seq c (While b c) ∈ redexes c''"
            by blast
          note step
          finally
          show ?thesis
            using red_c''
            by (blast intro: that)
        qed
        from reach termi
        have "Γ⊨c' ↓ Normal s"
          by (rule steps_preserves_termination')
        from redexes_preserves_termination [OF this red_c']
        have termi_while: "Γ⊨While b c ↓ Normal s" .
        show "s ∈ {t. t = s ∧ Γ⊨⟨c,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                      Γ⊨Call p ↓ Normal σ ∧
                   (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal t) ∧ c ∈ redexes c')} ∧
        (∀t. t ∈ {t. Γ⊨⟨c,Normal s⟩ → Normal t} ⟶
             t ∈ {t. (t,τ) ∈ ?r} ∩
                 {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)) ∧
                      Γ⊨Call p ↓ Normal σ ∧
                    (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal t) ∧
                          While b c ∈ redexes c')}) ∧
         (∀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 termi reach_c show ?C1
            apply clarsimp
            apply (drule redexes_subset)
            apply simp
            apply (blast intro: root_in_redexes)
            done
        next
          {
            fix t
            assume s_t: "Γ⊨⟨c,Normal s⟩ → Normal t"
            with s_eq_τ termi_while s_in_b have "(t,τ) ∈ ?r"
              by blast
            moreover
            from Z_s_unroll s_t s_in_b
            have "(Z, t) ∈ ?unroll"
              by (blast intro: rtrancl_into_rtrancl)
            moreover
            obtain c'' where
              reach_c'': "Γ⊨(Call p,Normal σ) →⁺ (c'',Normal t)"
                        "(While b c) ∈ redexes c''"
            proof -
              note reach_c (1)
              also from s_in_b
              have "Γ⊨(While b c,Normal s)→ (Seq c (While b c),Normal s)"
                by (rule step.WhileTrue)
              have "Γ⊨ (Seq c (While b c), Normal s) →⁺
                        (While b c, Normal t)"
              proof -
                from exec_impl_steps_Normal [OF s_t]
                have "Γ⊨ (c, Normal s) →^* (Skip, Normal t)".
                hence "Γ⊨ (Seq c (While b c), Normal s) →^*
                          (Seq Skip (While b c), Normal t)"
                  by (rule SeqSteps) auto
                moreover
                have "Γ⊨(Seq Skip (While b c), Normal t)→(While b c, Normal t)"
                  by (rule step.SeqSkip)
                ultimately show ?thesis by (rule rtranclp_into_tranclp1)
              qed
              from steps_redexes' [OF this reach_c (2)]
              obtain c''' where
                step: "Γ⊨ (c'', Normal s) →⁺ (c''', Normal t)" and
                red_c'': "While b c ∈ redexes c'''"
                by blast
              note step
              finally
              show ?thesis
                using red_c''
                by (blast intro: that)
            qed
            moreover note noabort termi
            ultimately
            have "(t,τ) ∈ ?r ∧ (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)) ∧
                  Γ⊨Call p ↓ Normal σ ∧
                    (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c', Normal t) ∧
                             While b c ∈ redexes c')"
              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)) ∧
                       Γ⊨Call p↓Normal σ ∧
                   (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                         While b c ∈ redexes c')}"
    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 q)
  let ?P = "{s. s=Z ∧ Γ⊨⟨Call q ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
               Γ⊨Call p↓Normal σ ∧
              (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ Call q ∈ redexes c')}"
  from noStuck_Call
  have "∀s ∈ ?P. q ∈ dom Γ"
    by (fastforce simp add: final_notin_def)
  then show ?case
  proof (rule conseq_extract_state_indep_prop)
    assume q_defined: "q ∈ dom Γ"
    from Call_hyp have
      "∀q∈dom Γ. ∀Z.
        Γ,Θ⊨<sub>tF</sub>{s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                        Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
                 (Call q)
                {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}"
      by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified]
         terminates_Normal_Call_body)
    from Call_hyp q_defined have Call_hyp':
    "∀Z. Γ,Θ ⊨_tF {s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
                  (Call q)
                 {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t},
                 {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}"
      by auto
    show
     "Γ,Θ⊨<sub>tF</sub> ?P
           (Call q)
          {t. Γ⊨⟨Call q ,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Call q ,Normal Z⟩ → Abrupt t}"
    proof (rule ConseqMGT [OF Call_hyp'],safe)
      fix c'
      assume termi: "Γ⊨Call p ↓ Normal σ"
      assume steps_c': "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
      assume red_c': "Call q ∈ redexes c'"
      show "Γ⊨Call q ↓ Normal Z"
      proof -
        from steps_preserves_termination' [OF steps_c' termi]
        have "Γ⊨c' ↓ Normal Z" .
        from redexes_preserves_termination [OF this red_c']
        show ?thesis .
      qed
    next
      fix c'
      assume termi: "Γ⊨Call p ↓ Normal σ"
      assume steps_c': "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
      assume red_c': "Call q ∈ redexes c'"
      from redex_redexes [OF this]
      have "redex c' = Call q"
        by auto
      with termi steps_c'
      show "((Z, q), σ, p) ∈ termi_call_steps Γ"
        by (auto simp add: termi_call_steps_def)
    qed
  qed
next
  case (DynCom c)
  have hyp:
    "∧s'. ∀Z. Γ,Θ⊨<sub>tF</sub>
      {s. s = Z ∧ Γ⊨⟨c s',Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
            Γ⊨Call p ↓ Normal σ ∧
          (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ c s' ∈ redexes c')}
        (c s')
       {t. Γ⊨⟨c s',Normal Z⟩ → Normal t},{t. Γ⊨⟨c s',Normal Z⟩ → Abrupt t}"
    using DynCom by simp
  have hyp':
    "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨DynCom c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Call p ↓ Normal σ ∧
               (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ DynCom c ∈ redexes c')}
        (c Z)
       {t. Γ⊨⟨DynCom c,Normal Z⟩ → Normal t},{t. Γ⊨⟨DynCom c,Normal Z⟩ → Abrupt t}"
  proof (rule ConseqMGT [OF hyp],safe)
    assume "Γ⊨⟨DynCom c,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
    then show "Γ⊨⟨c Z,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (fastforce simp add: final_notin_def intro: exec.intros)
  next
    fix c'
    assume steps: "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
    assume c': "DynCom c ∈ redexes c'"
    have "Γ⊨ (DynCom c, Normal Z) → (c Z,Normal Z)"
      by (rule step.DynCom)
    from step_redexes [OF this c'] obtain c'' where
      step: "Γ⊨ (c', Normal Z) → (c'', Normal Z)"  and c'': "c Z ∈ redexes c''"
      by blast
    note steps also note step
    finally show "∃c'. Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z) ∧ c Z ∈ redexes c'"
      using c'' by blast
  next
    fix t
    assume "Γ⊨⟨c Z,Normal Z⟩ → Normal t"
    thus "Γ⊨⟨DynCom c,Normal Z⟩ → Normal t"
      by (auto intro: exec.intros)
  next
    fix t
    assume "Γ⊨⟨c Z,Normal Z⟩ → Abrupt t"
    thus "Γ⊨⟨DynCom c,Normal Z⟩ → Abrupt t"
      by (auto intro: exec.intros)
  qed
  show ?case
    apply (rule hoaret.DynCom)
    apply safe
    apply (rule hyp')
    done
next
  case (Guard f g c)
  have hyp_c: "∀Z. Γ,Θ⊨<sub>tF</sub>
         {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
              Γ⊨Call p↓Normal σ ∧
            (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧ c ∈ redexes c')}
          c
         {t. Γ⊨⟨c,Normal Z⟩ → Normal t},
         {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}"
    using Guard.hyps by iprover
  show "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨Guard f g c ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨Call p↓Normal σ ∧
            (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ Guard f g c ∈ redexes c')}
              Guard f g c
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Abrupt t}"
  proof (cases "f ∈ F")
    case True
    have "Γ,Θ⊨<sub>tF</sub> (g ∩ {s. s=Z ∧
                     Γ⊨⟨Guard f g c ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Call p↓Normal σ ∧
            (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                  Guard f g c ∈ redexes c')})
              c
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Abrupt t}"
    proof (rule ConseqMGT [OF hyp_c], safe)
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" "Z∈g"
      thus "Γ⊨⟨c,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
        by (auto simp add: final_notin_def intro: exec.intros)
    next
      fix c'
      assume steps: "Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z)"
      assume c': "Guard f g c ∈ redexes c'"
      assume "Z ∈ g"
      from this have "Γ⊨(Guard f g c,Normal Z) → (c,Normal Z)"
        by (rule step.Guard)
      from step_redexes [OF this c'] obtain c'' where
        step: "Γ⊨ (c', Normal Z) → (c'', Normal Z)"  and c'': "c ∈ redexes c''"
        by blast
      note steps also note step
      finally show "∃c'. Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z) ∧ c ∈ redexes c'"
        using c'' by blast
    next
      fix t
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
             "Γ⊨⟨c,Normal Z⟩ → Normal t" "Z ∈ g"
      thus "Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t"
        by (auto simp add: final_notin_def intro: exec.intros )
    next
      fix t
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
              "Γ⊨⟨c,Normal Z⟩ → Abrupt t" "Z ∈ g"
      thus "Γ⊨⟨Guard f g c ,Normal Z⟩ → Abrupt t"
        by (auto simp add: final_notin_def intro: exec.intros )
    qed
    from True this show ?thesis
      by (rule conseqPre [OF Guarantee]) auto
  next
    case False
    have "Γ,Θ⊨_tF (g ∩ {s. s=Z ∧
                     Γ⊨⟨Guard f g c ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                 Γ⊨Call p↓Normal σ ∧
            (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧
                  Guard f g c ∈ redexes c')})
              c
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Abrupt t}"
    proof (rule ConseqMGT [OF hyp_c], safe)
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      thus "Γ⊨⟨c,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
        using False
        by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros)
    next
      fix c'
      assume steps: "Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z)"
      assume c': "Guard f g c ∈ redexes c'"

      assume "Z ∈ g"
      from this have "Γ⊨(Guard f g c,Normal Z) → (c,Normal Z)"
        by (rule step.Guard)
      from step_redexes [OF this c'] obtain c'' where
        step: "Γ⊨ (c', Normal Z) → (c'', Normal Z)"  and c'': "c ∈ redexes c''"
        by blast
      note steps also note step
      finally show "∃c'. Γ⊨ (Call p, Normal σ) →⁺ (c', Normal Z) ∧ c ∈ redexes c'"
        using c'' by blast
    next
      fix t
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
        "Γ⊨⟨c,Normal Z⟩ → Normal t"
      thus "Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t"
        using False
        by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
    next
      fix t
      assume "Γ⊨⟨Guard f g c ,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
             "Γ⊨⟨c,Normal Z⟩ → Abrupt t"
      thus "Γ⊨⟨Guard f g c ,Normal Z⟩ → Abrupt t"
        using False
        by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
    qed
    then show ?thesis
      apply (rule conseqPre [OF hoaret.Guard])
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply auto
      done
  qed
next
  case Throw
  show "Γ,Θ⊨_tF {s. s=Z ∧ Γ⊨⟨Throw,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨Call p↓Normal σ ∧
                (∃c'. Γ⊨(Call p, Normal σ) →<sup>+</sup> (c',Normal s) ∧ Throw ∈ redexes c')}
              Throw
              {t. Γ⊨⟨Throw,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Throw,Normal Z⟩ → Abrupt t}"
    by (rule conseqPre [OF hoaret.Throw])
       (blast intro: exec.intros terminates.intros)
next
  case (Catch c<sub>1</sub> c<sub>2</sub>)
  have hyp_c1:
   "∀Z. Γ,Θ⊨<sub>tF</sub> {s. s= Z ∧ Γ⊨⟨c<sub>1</sub>,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call p ↓ Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal s) ∧
                      c₁ ∈ redexes c')}
               c₁
              {t. Γ⊨⟨c₁,Normal Z⟩ → Normal t},{t. Γ⊨⟨c₁,Normal Z⟩ → Abrupt t}"
    using Catch.hyps by iprover
  have hyp_c2:
   "∀Z. Γ,Θ⊨_tF {s. s= Z ∧ Γ⊨⟨c₂,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                     Γ⊨Call p↓ Normal σ ∧
                (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal s) ∧ c<sub>2</sub> ∈ redexes c')}
               c<sub>2</sub>
              {t. Γ⊨⟨c<sub>2</sub>,Normal Z⟩ → Normal t},{t. Γ⊨⟨c<sub>2</sub>,Normal Z⟩ → Abrupt t}"
    using Catch.hyps by iprover
  have
    "Γ,Θ⊨<sub>tF</sub> {s. s = Z ∧ Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
               Γ⊨Call p↓ Normal σ ∧
            (∃c'. Γ⊨(Call p,Normal σ)→⁺(c',Normal s) ∧
                   Catch c₁ c₂ ∈ redexes c')}
            c₁
           {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Normal t},
           {t. Γ⊨⟨c₁,Normal Z⟩ → Abrupt t ∧
               Γ⊨⟨c₂,Normal t⟩ →∉({Stuck} ∪ Fault`(-F)) ∧ Γ⊨Call p ↓ Normal σ ∧
               (∃c'. Γ⊨(Call p,Normal σ) →<sup>+</sup> (c',Normal t) ∧ c<sub>2</sub> ∈ redexes c')}"
  proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
    assume "Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
    thus "Γ⊨⟨c₁,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (fastforce simp add: final_notin_def intro: exec.intros)
  next
    fix c'
    assume steps: "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
    assume c': "Catch c<sub>1</sub> c<sub>2</sub> ∈ redexes c'"
    from steps redexes_subset [OF this]
    show "∃c'. Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z) ∧ c<sub>1</sub> ∈ redexes c'"
      by (auto iff:  root_in_redexes)
  next
    fix t
    assume "Γ⊨⟨c<sub>1</sub>,Normal Z⟩ → Normal t"
    thus "Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal Z⟩ → Normal t"
      by (auto intro: exec.intros)
  next
    fix t
    assume "Γ⊨⟨Catch c<sub>1</sub> c<sub>2</sub>,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))"
      "Γ⊨⟨c₁,Normal Z⟩ → Abrupt t"
    thus "Γ⊨⟨c₂,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F))"
      by (auto simp add: final_notin_def intro: exec.intros)
  next
    fix c' t
    assume steps_c': "Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal Z)"
    assume red: "Catch c<sub>1</sub> c<sub>2</sub> ∈ redexes c'"
    assume exec_c<sub>1</sub>: "Γ⊨ ⟨c<sub>1</sub>,Normal Z⟩ → Abrupt t"
    show "∃c'. Γ⊨ (Call p, Normal σ) →<sup>+</sup> (c', Normal t) ∧ c<sub>2</sub> ∈ redexes c'"
    proof -
      note steps_c'
      also
      from exec_impl_steps_Normal_Abrupt [OF exec_c<sub>1</sub>]
      have "Γ⊨ (c<sub>1</sub>, Normal Z) →<sup>*</sup> (Throw, Normal t)".
      from steps_redexes_Catch [OF this red]
      obtain c'' where
        steps_c'': "Γ⊨ (c', Normal Z) →<sup>*</sup> (c'', Normal t)" and
        Catch: "Catch Throw c<sub>2</sub> ∈ redexes c''"
        by blast
      note steps_c''
      also
      have step_Catch: "Γ⊨ (Catch Throw c<sub>2</sub>,Normal t) → (c<sub>2</sub>,Normal t)"
        by (rule step.CatchThrow)
      from step_redexes [OF step_Catch Catch]
      obtain c''' where
        step_c''': "Γ⊨ (c'', Normal t) → (c''', Normal t)" and
        c2: "c<sub>2</sub> ∈ redexes c'''"
        by blast
      note step_c'''
      finally show ?thesis
        using c2
        by blast
    qed
  qed
  moreover
  have "Γ,Θ⊨<sub>tF</sub> {t. Γ⊨⟨c<sub>1</sub>,Normal Z⟩ → Abrupt t ∧
                  Γ⊨⟨c<sub>2</sub>,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨Call p ↓ Normal σ ∧
                  (∃c'. Γ⊨(Call p,Normal σ) →⁺ (c',Normal t) ∧ c₂ ∈ redexes c')}
               c₂
              {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Catch c₁ c₂,Normal Z⟩ → Abrupt t}"
    by (rule ConseqMGT [OF hyp_c2]) (fastforce intro: exec.intros)
  ultimately show ?case
    by (rule hoaret.Catch)
qed


text ‹To prove a procedure implementation correct it suffices to assume
 only the procedure specifications of procedures that actually
 occur during evaluation of the body.
 ›

lemma Call_lemma:
 assumes A:
 "∀q ∈ dom Γ. ∀Z. Γ,Θ ⊨_tF
                 {s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
                 (Call q)
                {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}"
 assumes pdef: "p ∈ dom Γ"
 shows "∧Z. Γ,Θ ⊨<sub>tF</sub>
              ({σ} ∩ {s. s=Z ∧Γ⊨⟨the (Γ p),Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                                 Γ⊨the (Γ p)↓Normal s})
                 the (Γ p)
              {t. Γ⊨⟨the (Γ p),Normal Z⟩ → Normal t},
              {t. Γ⊨⟨the (Γ p),Normal Z⟩ → Abrupt t}"
apply (rule conseqPre)
apply (rule Call_lemma' [OF A])
using pdef
apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step Γ)", OF step.Call] root_in_redexes)
done

lemma Call_lemma_switch_Call_body:
 assumes
 call: "∀q ∈ dom Γ. ∀Z. Γ,Θ ⊨_tF
                 {s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
                 (Call q)
                {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t},
                {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}"
 assumes p_defined: "p ∈ dom Γ"
 shows "∧Z. Γ,Θ ⊨<sub>tF</sub>
              ({σ} ∩ {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                                 Γ⊨Call p↓Normal s})
                 the (Γ p)
              {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
              {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}"
apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined])
apply (rule conseqPre)
apply (rule Call_lemma')
apply (rule call)
using p_defined
apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step Γ)", OF step.Call]
root_in_redexes)
done

lemma MGT_Call:
"∀p ∈ dom Γ. ∀Z.
  Γ,Θ ⊨_tF {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
             Γ⊨(Call p)↓Normal s}
           (Call p)
          {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}"
apply (intro ballI allI)
apply (rule CallRec' [where Procs="dom Γ" and
    P="λp Z. {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                    Γ⊨Call p↓Normal s}" and
    Q="λp Z. {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t}" and
    A="λp Z. {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}" and
    r="termi_call_steps Γ"
    ])
apply    simp
apply   simp
apply  (rule wf_termi_call_steps)
apply (intro ballI allI)
apply simp
apply (rule Call_lemma_switch_Call_body [rule_format, simplified])
apply  (rule hoaret.Asm)
apply  fastforce
apply assumption
done


lemma CollInt_iff: "{s. P s} ∩ {s. Q s} = {s. P s ∧ Q s}"
  by auto

lemma image_Un_conv: "f ` (∪p∈dom Γ. ∪Z. {x p Z}) = (∪p∈dom Γ. ∪Z. {f (x p Z)})"
  by (auto iff: not_None_eq)


text ‹Another proof of ‹MGT_Call›, maybe a little more readable›
lemma
"∀p ∈ dom Γ. ∀Z.
  Γ,{} ⊨_tF {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
             Γ⊨(Call p)↓Normal s}
           (Call p)
          {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
          {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}"
proof -
  {
    fix p Z σ
    assume defined: "p ∈ dom Γ"
    define Specs where "Specs = (∪p∈dom Γ. ∪Z.
            {({s. s=Z ∧
              Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
              Γ⊨Call p↓Normal s},
             p,
             {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
             {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t})})"
    define Specs_wf where "Specs_wf p σ = (λ(P,q,Q,A).
                       (P ∩ {s. ((s,q),σ,p) ∈ termi_call_steps Γ}, q, Q, A)) ` Specs" for p σ
    have "Γ,Specs_wf p σ
            ⊨<sub>tF</sub>({σ} ∩
                 {s. s = Z ∧ Γ⊨⟨the (Γ p),Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨the (Γ p)↓Normal s})
                (the (Γ p))
               {t. Γ⊨⟨the (Γ p),Normal Z⟩ → Normal t},
               {t. Γ⊨⟨the (Γ p),Normal Z⟩ → Abrupt t}"
      apply (rule Call_lemma [rule_format, OF _ defined])
      apply (rule hoaret.Asm)
      apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv)
      apply (rule_tac x=q in bexI)
      apply (rule_tac x=Z in exI)
      apply (clarsimp simp add: CollInt_iff)
      apply auto
      done
    hence "Γ,Specs_wf p σ
            ⊨_tF({σ} ∩
                 {s. s = Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
                  Γ⊨Call p↓Normal s})
                (the (Γ p))
               {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
               {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}"
      by (simp only: exec_Call_body' [OF defined]
                   noFaultStuck_Call_body' [OF defined]
                  terminates_Normal_Call_body [OF defined])
  } note bdy=this
  show ?thesis
    apply (intro ballI allI)
    apply (rule hoaret.CallRec [where Specs="(∪p∈dom Γ. ∪Z.
            {({s. s=Z ∧
              Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧
              Γ⊨Call p↓Normal s},
             p,
             {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t},
             {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t})})",
             OF _ wf_termi_call_steps [of Γ] refl])
    apply fastforce
    apply clarify
    apply (rule conjI)
    apply  fastforce
    apply (rule allI)
    apply (simp (no_asm_use) only : Un_empty_left)
    apply (rule bdy)
    apply auto
    done
qed


theorem hoaret_complete: "Γ⊨_tF P c Q,A ==> Γ,{}⊨_tF P c Q,A"
  by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call])

lemma hoaret_complete':
  assumes cvalid: "Γ,Θ⊨_tF P c Q,A"
  shows  "Γ,Θ⊨_tF P c Q,A"
proof (cases "Γ⊨_tF P c Q,A")
  case True
  hence "Γ,{}⊨_tF P c Q,A"
    by (rule hoaret_complete)
  thus "Γ,Θ⊨_tF P c Q,A"
    by (rule hoaret_augment_context) simp
next
  case False
  with cvalid
  show ?thesis
    by (rule ExFalso)
qed

subsection ‹And Now: Some Useful Rules›

subsubsection ‹Modify Return›

lemma Proc_exnModifyReturn_sound:
  assumes valid_call: "Γ,Θ ⊨_tF P call_exn init p return' result_exn c Q,A"
  assumes valid_modif:
  "∀σ. Γ,Θ ⊨_UNIV {σ} (Call p) (Modif σ),(ModifAbr σ)"
  assumes res_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 "Γ,Θ ⊨_tF P (call_exn init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_UNIV P (Call p) Q,A"
    by (auto intro: valid_augment_Faults)
  assume exec: "Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from exec
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: exec_call_exn_Normal_elim)
    fix bdy t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t'"
    assume exec_c: "Γ⊨⟨c s t',Normal (return s t')⟩ → t"
    from exec_body bdy
    have "Γ⊨⟨(Call p ),Normal (init s)⟩ → Normal t'"
      by (auto simp add: intro: exec.intros)
    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
    have "t' ∈ Modif (init s)"
      by auto
    with res_modif have "Normal (return' s t') = Normal (return s t')"
      by simp
    with exec_body exec_c bdy
    have "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exn)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Abrupt t'"
    assume t: "t = Abrupt (result_exn (return s t') t')"
    also from exec_body bdy
    have "Γ⊨⟨(Call p),Normal (init s)⟩ → Abrupt t'"
      by (auto simp add: intro: exec.intros)
    from cvalidD [OF valid_modif [rule_format, of "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
    have "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exnAbrupt)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy f
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊨⟨bdy,Normal (init s)⟩ → Fault f"  and
      t: "t = Fault f"
    with bdy have "Γ⊨⟨call_exn init p return' result_exn c ,Normal s⟩ → t"
      by (auto intro: exec_call_exnFault)
    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
    show ?thesis
      by simp
  next
    fix bdy
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊨⟨bdy,Normal (init s)⟩ → Stuck"
      "t = Stuck"
    with bdy have "Γ⊨⟨call_exn init p return' result_exn c ,Normal s⟩ → t"
      by (auto intro: exec_call_exnStuck)
    from valid_call ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  next
    assume "Γ p = None" "t=Stuck"
    hence "Γ⊨⟨call_exn init p return' result_exn c ,Normal s⟩ → t"
      by (auto intro: exec_call_exnUndefined)
    from valid_call ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_UNIV P (Call p) Q,A"
    by (auto intro: valid_augment_Faults)
  assume P: "s ∈ P"
  from valid_call ctxt P
  have call: "Γ⊨call_exn init p return' result_exn c↓ Normal s"
    by (rule cvalidt_termD)
  show "Γ⊨call_exn init p return result_exn c ↓ Normal s"
  proof (cases "p ∈ dom Γ")
    case True
    with call obtain bdy where
      bdy: "Γ p = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and
      termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶
                    Γ⊨c s t ↓ Normal (return' s t)"
      by cases auto
    {
      fix t
      assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t"
      hence "Γ⊨c s t ↓ Normal (return s t)"
      proof -
        from exec_bdy bdy
        have "Γ⊨⟨(Call p ),Normal (init s)⟩ → Normal t"
          by (auto simp add: intro: exec.intros)
        from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
          res_modif
        have "return' s t = return s t"
          by auto
        with termi_c exec_bdy show ?thesis by auto
      qed
    }
    with bdy termi_bdy
    show ?thesis
      by (iprover intro: terminates_call_exn)
  next
    case False
    thus ?thesis
      by (auto intro: terminates_call_exnUndefined)
  qed
qed

lemma ProcModifyReturn_sound:
  assumes valid_call: "Γ,Θ ⊨_tF P call init p return' c Q,A"
  assumes valid_modif:
  "∀σ. Γ,Θ ⊨_UNIV {σ} (Call p) (Modif σ),(ModifAbr σ)"
  assumes res_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 "Γ,Θ ⊨_tF P (call init p return c) Q,A"
  using valid_call valid_modif res_modif ret_modifAbr unfolding call_call_exn
  by (rule Proc_exnModifyReturn_sound)


lemma Proc_exnModifyReturn:
  assumes spec: "Γ,Θ⊨_tF P (call_exn init p return' result_exn c) Q,A"
  assumes res_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 modifies_spec:
  "∀σ. Γ,Θ⊨_UNIV {σ} (Call p) (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊨_tF P (call_exn init p return result_exn c) Q,A"
apply (rule hoaret_complete')
apply (rule Proc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
        OF _ _ res_modif ret_modifAbr])
apply (rule hoaret_sound [OF spec])
using modifies_spec
apply (blast intro: hoare_sound)
done

lemma ProcModifyReturn:
  assumes spec: "Γ,Θ⊨_tF P (call init p return' c) Q,A"
  assumes res_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 modifies_spec:
  "∀σ. Γ,Θ⊨_UNIV {σ} (Call p) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊨_tF P (call init p return c) Q,A"
  using spec res_modif ret_modifAbr modifies_spec unfolding call_call_exn by (rule Proc_exnModifyReturn)

lemma Proc_exnModifyReturnSameFaults_sound:
  assumes valid_call: "Γ,Θ ⊨_tF P call_exn init p return' result_exn c Q,A"
  assumes valid_modif:
  "∀σ. Γ,Θ ⊨_F {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes res_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 "Γ,Θ ⊨_tF P (call_exn init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  assume exec: "Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from exec
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: exec_call_exn_Normal_elim)
    fix bdy t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t'"
    assume exec_c: "Γ⊨⟨c s t',Normal (return s t')⟩ → t"
    from exec_body bdy
    have "Γ⊨⟨(Call p) ,Normal (init s)⟩ → Normal t'"
      by (auto simp add: intro: exec.intros)
    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
    have "t' ∈ Modif (init s)"
      by auto
    with res_modif have "Normal (return' s t') = Normal (return s t')"
      by simp
    with exec_body exec_c bdy
    have "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exn)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy t'
    assume bdy: "Γ p = Some bdy"
    assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Abrupt t'"
    assume t: "t = Abrupt (result_exn (return s t') t')"
    also
    from exec_body bdy
    have "Γ⊨⟨Call p ,Normal (init s)⟩ → Abrupt t'"
      by (auto simp add: intro: exec.intros)
    from cvalidD [OF valid_modif [rule_format, of "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
    have "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exnAbrupt)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis
      by simp
  next
    fix bdy f
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊨⟨bdy,Normal (init s)⟩ → Fault f"  and
      t: "t = Fault f"
    with bdy have "Γ⊨⟨call_exn init p return' result_exn c ,Normal s⟩ → t"
      by (auto intro: exec_call_exnFault)
    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
    show ?thesis
      by simp
  next
    fix bdy
    assume bdy: "Γ p = Some bdy"
    assume "Γ⊨⟨bdy,Normal (init s)⟩ → Stuck"
      "t = Stuck"
    with bdy have "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exnStuck)
    from valid_call ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  next
    assume "Γ p = None" "t=Stuck"
    hence "Γ⊨⟨call_exn init p return' result_exn c,Normal s⟩ → t"
      by (auto intro: exec_call_exnUndefined)
    from valid_call ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  assume P: "s ∈ P"
  from valid_call ctxt P
  have call: "Γ⊨call_exn init p return' result_exn c↓ Normal s"
    by (rule cvalidt_termD)
  show "Γ⊨call_exn init p return result_exn c ↓ Normal s"
  proof (cases "p ∈ dom Γ")
    case True
    with call obtain bdy where
      bdy: "Γ p = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and
      termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶
                    Γ⊨c s t ↓ Normal (return' s t)"
      by cases auto
    {
      fix t
      assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t"
      hence "Γ⊨c s t ↓ Normal (return s t)"
      proof -
        from exec_bdy bdy
        have "Γ⊨⟨(Call p ),Normal (init s)⟩ → Normal t"
          by (auto simp add: intro: exec.intros)
        from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
          res_modif
        have "return' s t = return s t"
          by auto
        with termi_c exec_bdy show ?thesis by auto
      qed
    }
    with bdy termi_bdy
    show ?thesis
      by (iprover intro: terminates_call_exn)
  next
    case False
    thus ?thesis
      by (auto intro: terminates_call_exnUndefined)
  qed
qed

lemma ProcModifyReturnSameFaults_sound:
  assumes valid_call: "Γ,Θ ⊨_tF P call init p return' c Q,A"
  assumes valid_modif:
  "∀σ. Γ,Θ ⊨_F {σ} Call p (Modif σ),(ModifAbr σ)"
  assumes res_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 "Γ,Θ ⊨_tF P (call init p return c) Q,A"
  using valid_call valid_modif res_modif ret_modifAbr unfolding call_call_exn
  by (rule Proc_exnModifyReturnSameFaults_sound)

lemma Proc_exnModifyReturnSameFaults:
  assumes spec: "Γ,Θ⊨_tF P (call_exn init p return' result_exn c) Q,A"
  assumes res_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 modifies_spec:
  "∀σ. Γ,Θ⊨_F {σ} (Call p) (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊨_tF P (call_exn init p return result_exn c) Q,A"
apply (rule hoaret_complete')
apply (rule Proc_exnModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=ModifAbr,
          OF _ _ res_modif ret_modifAbr])
apply (rule hoaret_sound [OF spec])
using modifies_spec
apply (blast intro: hoare_sound)
done


lemma ProcModifyReturnSameFaults:
  assumes spec: "Γ,Θ⊨_tF P (call init p return' c) Q,A"
  assumes res_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 modifies_spec:
  "∀σ. Γ,Θ⊨_F {σ} (Call p) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊨_tF P (call init p return c) Q,A"
  using spec res_modif ret_modifAbr modifies_spec unfolding call_call_exn
  by (rule Proc_exnModifyReturnSameFaults)



subsubsection ‹DynCall›

lemma dynProc_exnModifyReturn_sound:
assumes valid_call: "Γ,Θ ⊨_tF P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "∀s∈P. ∀σ. Γ,Θ ⊨_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 "Γ,Θ ⊨_tF P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_UNIV P (Call p) Q,A"
    by (auto intro: valid_augment_Faults)
  assume exec: "Γ⊨⟨dynCall_exn f g init p return result_exn c,Normal s⟩ → t"
  assume t_notin_F: "t ∉ Fault ` F"
  assume P: "s ∈ P"
  with valid_modif
  have valid_modif':
    "∀σ. Γ,Θ⊨<sub>UNIV</sub> {σ} (Call (p s)) (Modif σ),(ModifAbr σ)"
    by blast
  from exec
  have "Γ⊨⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ → t"
    by (cases rule: exec_dynCall_exn_Normal_elim)
  then show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: exec_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⟩ → t" by simp
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases rule: exec_call_exn_Normal_elim)
      fix bdy t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t'"
      assume exec_c: "Γ⊨⟨c s t',Normal (return s t')⟩ → t"
      from exec_body bdy
      have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t'"
        by (auto simp add: intro: exec.Call)
      from cvalidD [OF valid_modif' [rule_format, of "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
      have "Γ⊨⟨call_exn init (p s) return' result_exn c,Normal s⟩ → t"
        by (auto intro: exec_call_exn)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Abrupt t'"
      assume t: "t = Abrupt (result_exn (return s t') t')"
      also from exec_body bdy
      have "Γ⊨⟨Call (p s) ,Normal (init s)⟩ → Abrupt t'"
        by (auto simp add: intro: exec.intros)
      from cvalidD [OF valid_modif' [rule_format, of "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
      have "Γ⊨⟨call_exn init (p s) return' result_exn c,Normal s⟩ → t"
        by (auto intro: exec_call_exnAbrupt)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy f'
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊨⟨bdy,Normal (init s)⟩ → Fault f'"  and
        t: "t = Fault f'"
      with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnFault)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
      show ?thesis
        by blast
    next
      fix bdy
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊨⟨bdy,Normal (init s)⟩ → Stuck"
        "t = Stuck"
      with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnStuck)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cvalidt_postD)
    next
      fix bdy
      assume "Γ (p s) = None" "t=Stuck"
      hence "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnUndefined)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cvalidt_postD)
    qed
  next
    case (someFault)
    then obtain guards_fail:"s ∉ g"
      and t: "t = Fault f" by simp
    from exec_maybe_guard_Fault [OF guards_fail] t
    have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
      by (simp add: dynCall_exn_def exec_guards_DynCom)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis by simp
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_UNIV P (Call p) Q,A"
    by (auto intro: valid_augment_Faults)
  assume P: "s ∈ P"
  from valid_call ctxt P
  have "Γ⊨dynCall_exn f g init p return' result_exn c↓ Normal s"
    by (rule cvalidt_termD)
  thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
  proof (cases rule: terminates_dynCall_exn_elim)
    case noFault
    then obtain guards_ok: "s ∈ g"
        and call: "Γ⊨call_exn init (p s) return' result_exn c↓ Normal s"
      by auto
    have "Γ⊨call_exn init (p s) return result_exn c ↓ Normal s"
    proof (cases "p s ∈ dom Γ")
      case True
      with call obtain bdy where
        bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and
        termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶
                      Γ⊨c s t ↓ Normal (return' s t)"
        by cases auto
      {
        fix t
        assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t"
        hence "Γ⊨c s t ↓ Normal (return s t)"
        proof -
          from exec_bdy bdy
          have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t"
            by (auto simp add: intro: exec.intros)
          from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
            ret_modif
          have "return' s t = return s t"
            by auto
          with termi_c exec_bdy show ?thesis by auto
        qed
      }
      with bdy termi_bdy
      show ?thesis
        by (iprover intro: terminates_call_exn)
    next
      case False
      thus ?thesis
        by (auto intro: terminates_call_exnUndefined)
    qed
    thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
      by (iprover intro: terminates_dynCall_exn)
  next
    case (someFault)
    then have guard_fail: "s ∉ g" by simp
    thus ?thesis
      by (simp add: terminates_maybe_guard_Fault dynCall_exn_def)
  qed
qed

lemma dynProcModifyReturn_sound:
assumes valid_call: "Γ,Θ ⊨_tF P dynCall init p return' c Q,A"
assumes valid_modif:
    "∀s∈P. ∀σ. Γ,Θ ⊨_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 "Γ,Θ ⊨_tF 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: "Γ,Θ⊨_tF 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 "Γ,Θ ⊨_tF P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoaret_complete')
apply (rule dynProc_exnModifyReturn_sound
        [where Modif=Modif and ModifAbr=ModifAbr,
            OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_sound [OF modif [rule_format]])
apply assumption
  done

lemma dynProcModifyReturn:
assumes dyn_call: "Γ,Θ⊨_tF 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 "Γ,Θ ⊨_tF 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: "Γ,Θ ⊨_tF P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "∀s∈P. ∀σ. Γ,Θ ⊨_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 "Γ,Θ ⊨_tF P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  assume exec: "Γ⊨⟨dynCall_exn f g init p return result_exn c,Normal s⟩ → t"
  assume t_notin_F: "t ∉ Fault ` F"
  assume P: "s ∈ P"
  with valid_modif
  have valid_modif':
    "∀σ. Γ,Θ⊨<sub>F</sub> {σ} (Call (p s)) (Modif σ),(ModifAbr σ)"
    by blast
  from exec
  have "Γ⊨⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ → t"
    by (cases rule: exec_dynCall_exn_Normal_elim)
  then show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: exec_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⟩ → t" by simp
    then show "t ∈ Normal ` Q ∪ Abrupt ` A"
    proof (cases rule: exec_call_exn_Normal_elim)
      fix bdy t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t'"
      assume exec_c: "Γ⊨⟨c s t',Normal (return s t')⟩ → t"
      from exec_body bdy
      have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t'"
        by (auto simp add: intro: exec.intros)
      from cvalidD [OF valid_modif' [rule_format, of "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
      have "Γ⊨⟨call_exn init (p s) return' result_exn c,Normal s⟩ → t"
        by (auto intro: exec_call_exn)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy t'
      assume bdy: "Γ (p s) = Some bdy"
      assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Abrupt t'"
      assume t: "t = Abrupt (result_exn (return s t') t')"
      also from exec_body bdy
      have "Γ⊨⟨Call (p s) ,Normal (init s)⟩ → Abrupt t'"
        by (auto simp add: intro: exec.intros)
      from cvalidD [OF valid_modif' [rule_format, of "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
      have "Γ⊨⟨call_exn init (p s) return' result_exn c,Normal s⟩ → t"
        by (auto intro: exec_call_exnAbrupt)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
      show ?thesis
        by simp
    next
      fix bdy f'
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊨⟨bdy,Normal (init s)⟩ → Fault f'"  and
        t: "t = Fault f'"
      with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnFault)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
      show ?thesis
        by simp
    next
      fix bdy
      assume bdy: "Γ (p s) = Some bdy"
      assume "Γ⊨⟨bdy,Normal (init s)⟩ → Stuck"
        "t = Stuck"
      with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnStuck)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cvalidt_postD)
    next
      fix bdy
      assume "Γ (p s) = None" "t=Stuck"
      hence "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t"
        by (auto intro: exec_call_exnUndefined)
      from exec_maybe_guard_noFault [OF this guards_ok]
      have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
        by (simp add: dynCall_exn_def exec_maybe_guard_DynCom)
      from valid_call ctxt this P t_notin_F
      show ?thesis
        by (rule cvalidt_postD)
    qed
  next
    case (someFault)
    then obtain guards_fail:"s ∉ g"
      and t: "t = Fault f" by simp
    from exec_maybe_guard_Fault [OF guards_fail] t
    have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t"
      by (simp add: dynCall_exn_def exec_guards_DynCom)
    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
    show ?thesis by simp
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  assume P: "s ∈ P"
  from valid_call ctxt P
  have "Γ⊨dynCall_exn f g init p return' result_exn c↓ Normal s"
    by (rule cvalidt_termD)
  thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
  proof (cases rule: terminates_dynCall_exn_elim)
    case noFault
    then obtain guards_ok: "s ∈ g"
        and call: "Γ⊨call_exn init (p s) return' result_exn c↓ Normal s"
      by auto
    have "Γ⊨call_exn init (p s) return result_exn c ↓ Normal s"
    proof (cases "p s ∈ dom Γ")
      case True
      with call obtain bdy where
        bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and
        termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶
                      Γ⊨c s t ↓ Normal (return' s t)"
        by cases auto
      {
        fix t
        assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t"
        hence "Γ⊨c s t ↓ Normal (return s t)"
        proof -
          from exec_bdy bdy
          have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t"
            by (auto simp add: intro: exec.intros)
          from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
            ret_modif
          have "return' s t = return s t"
            by auto
          with termi_c exec_bdy show ?thesis by auto
        qed
      }
      with bdy termi_bdy
      show ?thesis
        by (iprover intro: terminates_call_exn)
    next
      case False
      thus ?thesis
        by (auto intro: terminates_call_exnUndefined)
    qed
    thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
      by (iprover intro: terminates_dynCall_exn)
  next
    case (someFault)
    then have guard_fail: "s ∉ g" by simp
    thus ?thesis
      by (simp add: terminates_maybe_guard_Fault dynCall_exn_def)
  qed
qed

lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "Γ,Θ ⊨_tF P dynCall init p return' c Q,A"
assumes valid_modif:
    "∀s∈P. ∀σ. Γ,Θ ⊨_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 "Γ,Θ ⊨_tF 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: "Γ,Θ⊨_tF 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 "Γ,Θ ⊨_tF P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoaret_complete')
apply (rule dynProc_exnModifyReturnSameFaults_sound
        [where Modif=Modif and ModifAbr=ModifAbr,
          OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_sound [OF modif [rule_format]])
apply assumption
  done

lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊨_tF 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 "Γ,Θ ⊨_tF 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: "Γ,Θ ⊨_tF P c Q,A"
  assumes valid_R: "Γ,Θ ⊨_tF P c R,B"
  shows "Γ,Θ ⊨_tF P c (Q ∩ R),(A ∩ B)"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from valid_Q ctxt exec P t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` A"
    by (rule cvalidt_postD)
  moreover
  from valid_R ctxt exec P t_notin_F have "t ∈ Normal ` R ∪ Abrupt ` B"
    by (rule cvalidt_postD)
  ultimately show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ B)"
    by blast
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from valid_Q ctxt P
  show "Γ⊨c ↓ Normal s"
    by (rule cvalidt_termD)
qed

lemma PostConjI:
  assumes deriv_Q: "Γ,Θ⊨_tF P c Q,A"
  assumes deriv_R: "Γ,Θ⊨_tF P c R,B"
  shows "Γ,Θ⊨_tF P c (Q ∩ R),(A ∩ B)"
apply (rule hoaret_complete')
apply (rule PostConjI_sound)
apply (rule hoaret_sound [OF deriv_Q])
apply (rule hoaret_sound [OF deriv_R])
done


lemma Merge_PostConj_sound:
  assumes validF: "Γ,Θ⊨_tF P c Q,A"
  assumes validG: "Γ,Θ⊨_tG P' c R,X"
  assumes F_G: "F ⊆ G"
  assumes P_P': "P ⊆ P'"
  shows "Γ,Θ⊨_tF P c (Q ∩ R),(A ∩ X)"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  with F_G have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨_tG P (Call p) Q,A"
    by (auto intro: validt_augment_Faults)
  assume exec: "Γ⊨⟨c,Normal s⟩ → 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 cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault]
    have t: "t ∈ Normal ` Q ∪ Abrupt ` A".
    then have "t ∉ Fault ` G"
      by auto
    from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this]
    have "t ∈ Normal ` R ∪ Abrupt ` X" .
    with t show ?thesis by auto
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from validF ctxt P
  show "Γ⊨c ↓ Normal s"
    by (rule cvalidt_termD)
qed



lemma Merge_PostConj:
  assumes validF: "Γ,Θ⊨_tF P c Q,A"
  assumes validG: "Γ,Θ⊨_tG P' c R,X"
  assumes F_G: "F ⊆ G"
  assumes P_P': "P ⊆ P'"
  shows "Γ,Θ⊨_tF P c (Q ∩ R),(A ∩ X)"
apply (rule hoaret_complete')
apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
using validF apply (blast intro:hoaret_sound)
using validG apply (blast intro:hoaret_sound)
done


subsubsection ‹Guards and Guarantees›

lemma SplitGuards_sound:
  assumes valid_c1: "Γ,Θ⊨_tF P c₁ Q,A"
  assumes valid_c2: "Γ,Θ⊨_F P c₂ UNIV,UNIV"
  assumes c: "(c₁ ∩_g c₂) = Some c"
  shows "Γ,Θ⊨_tF P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨_F P (Call p) Q,A"
    by (auto simp add: validt_def)
  assume exec: "Γ⊨⟨c,Normal s⟩ → 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_exec_noFault [OF c exec]
    have "Γ⊨⟨c₁,Normal s⟩ → t" by simp
    from valid_c1 ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  next
    case Abrupt
    with inter_guards_exec_noFault [OF c exec]
    have "Γ⊨⟨c₁,Normal s⟩ → t" by simp
    from valid_c1 ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  next
    case (Fault f)
    assume t: "t=Fault f"
    with exec inter_guards_exec_Fault [OF c]
    have "Γ⊨⟨c₁,Normal s⟩ → Fault f ∨ Γ⊨⟨c₂,Normal s⟩ → Fault f"
      by auto
    then show ?thesis
    proof (cases rule: disjE [consumes 1])
      assume "Γ⊨⟨c₁,Normal s⟩ → Fault f"
      from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F
      show ?thesis
        by blast
    next
      assume "Γ⊨⟨c₂,Normal s⟩ → Fault f"
      from cvalidD [OF valid_c2 ctxt' this P] t t_notin_F
      show ?thesis
        by blast
    qed
  next
    case Stuck
    with inter_guards_exec_noFault [OF c exec]
    have "Γ⊨⟨c₁,Normal s⟩ → t" by simp
    from valid_c1 ctxt this P t_notin_F
    show ?thesis
      by (rule cvalidt_postD)
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  show "Γ⊨c ↓ Normal s"
  proof -
    from valid_c1 ctxt P
    have "Γ⊨c₁ ↓ Normal s"
      by (rule cvalidt_termD)
    with c show ?thesis
      by (rule inter_guards_terminates)
  qed
qed

lemma SplitGuards:
  assumes c: "(c₁ ∩_g c₂) = Some c"
  assumes deriv_c1: "Γ,Θ⊨_tF P c₁ Q,A"
  assumes deriv_c2: "Γ,Θ⊨_F P c₂ UNIV,UNIV"
  shows "Γ,Θ⊨_tF P c Q,A"
apply (rule hoaret_complete')
apply (rule SplitGuards_sound [OF _ _ c])
apply (rule hoaret_sound [OF deriv_c1])
apply (rule hoare_sound [OF deriv_c2])
done

lemma CombineStrip_sound:
  assumes valid: "Γ,Θ⊨_tF P c Q,A"
  assumes valid_strip: "Γ,Θ⊨_{} P (strip_guards (-F) c) UNIV,UNIV"
  shows "Γ,Θ⊨_t{} P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨_{} P (Call p) Q,A"
    by (auto simp add: validt_def)
  from ctxt have ctxt'': "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases t)
    case (Normal t')
    from cvalidt_postD [OF valid ctxt'' exec P] Normal
    show ?thesis
      by auto
  next
    case (Abrupt t')
    from cvalidt_postD [OF valid 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⟩ → Fault f"
        by (auto intro: exec_to_exec_strip_guards_Fault)
      from cvalidD [OF valid_strip ctxt' this P] Fault
      have False
        by auto
      thus ?thesis ..
    next
      case False
      with cvalidt_postD [OF valid ctxt'' exec P] Fault
      show ?thesis
        by auto
    qed
  next
    case Stuck
    from cvalidt_postD [OF valid ctxt'' exec P] Stuck
    show ?thesis
      by auto
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_t{} P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  assume P: "s ∈ P"
  show "Γ⊨c ↓ Normal s"
  proof -
    from valid ctxt' P
    show "Γ⊨c ↓ Normal s"
      by (rule cvalidt_termD)
  qed
qed

lemma CombineStrip:
  assumes deriv: "Γ,Θ⊨_tF P c Q,A"
  assumes deriv_strip: "Γ,Θ⊨_{} P (strip_guards (-F) c) UNIV,UNIV"
  shows "Γ,Θ⊨_t{} P c Q,A"
apply (rule hoaret_complete')
apply (rule CombineStrip_sound)
apply  (iprover intro: hoaret_sound [OF deriv])
apply (iprover intro: hoare_sound [OF deriv_strip])
done

lemma GuardsFlip_sound:
  assumes valid: "Γ,Θ⊨_tF P c Q,A"
  assumes validFlip: "Γ,Θ⊨_-F P c UNIV,UNIV"
  shows "Γ,Θ⊨_t{} P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  from ctxt have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  from ctxt have ctxtFlip: "∀(P, p, Q, A)∈Θ. Γ⊨_-F P (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases t)
    case (Normal t')
    from cvalidt_postD [OF valid ctxt' exec P] Normal
    show ?thesis
      by auto
  next
    case (Abrupt t')
    from cvalidt_postD [OF valid 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 cvalidD [OF validFlip ctxtFlip exec P] Fault
      have False
        by auto
      thus ?thesis ..
    next
      case False
      with cvalidt_postD [OF valid ctxt' exec P] Fault
      show ?thesis
        by auto
    qed
  next
    case Stuck
    from cvalidt_postD [OF valid ctxt' exec P] Stuck
    show ?thesis
      by auto
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨_t{} P (Call p) Q,A"
  hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  assume P: "s ∈ P"
  show "Γ⊨c ↓ Normal s"
  proof -
    from valid ctxt' P
    show "Γ⊨c ↓ Normal s"
      by (rule cvalidt_termD)
  qed
qed


lemma GuardsFlip:
  assumes deriv: "Γ,Θ⊨_tF P c Q,A"
  assumes derivFlip: "Γ,Θ⊨_-F P c UNIV,UNIV"
  shows "Γ,Θ⊨_t{} P c Q,A"
apply (rule hoaret_complete')
apply (rule GuardsFlip_sound)
apply  (iprover intro: hoaret_sound [OF deriv])
apply (iprover intro: hoare_sound [OF derivFlip])
done

lemma MarkGuardsI_sound:
  assumes valid: "Γ,Θ⊨_t{} P c Q,A"
  shows "Γ,Θ⊨_t{} P mark_guards f c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  assume exec: "Γ⊨⟨mark_guards f c,Normal s⟩ → t"
  from exec_mark_guards_to_exec [OF exec] obtain t' where
    exec_c: "Γ⊨⟨c,Normal s⟩ → 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 cvalidt_postD [OF valid [rule_format] ctxt exec_c P]
    have "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by blast
    with t'_noFault
    show ?thesis
      by auto
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨c ↓ Normal s".
  thus "Γ⊨mark_guards f c ↓ Normal s"
    by (rule terminates_to_terminates_mark_guards)
qed

lemma MarkGuardsI:
  assumes deriv: "Γ,Θ⊨_t{} P c Q,A"
  shows "Γ,Θ⊨_t{} P mark_guards f c Q,A"
apply (rule hoaret_complete')
apply (rule MarkGuardsI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done


lemma MarkGuardsD_sound:
  assumes valid: "Γ,Θ⊨_t{} P mark_guards f c Q,A"
  shows "Γ,Θ⊨_t{} P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases "isFault t")
    case True
    with exec_to_exec_mark_guards_Fault exec
    obtain f' where "Γ⊨⟨mark_guards f c,Normal s⟩ → Fault f'"
      by (fastforce elim: isFaultE)
    from cvalidt_postD [OF valid [rule_format] ctxt this P]
    have False
      by auto
    thus ?thesis ..
  next
    case False
    from exec_to_exec_mark_guards [OF exec False]
    obtain f' where "Γ⊨⟨mark_guards f c,Normal s⟩ → t"
      by auto
    from cvalidt_postD [OF valid [rule_format] ctxt this P]
    show ?thesis
      by auto
  qed
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨mark_guards f c ↓ Normal s".
  thus "Γ⊨c ↓ Normal s"
    by (rule terminates_mark_guards_to_terminates)
qed

lemma MarkGuardsD:
  assumes deriv: "Γ,Θ⊨_t{} P mark_guards f c Q,A"
  shows "Γ,Θ⊨_t{} P c Q,A"
apply (rule hoaret_complete')
apply (rule MarkGuardsD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done

lemma MergeGuardsI_sound:
  assumes valid: "Γ,Θ⊨_tF P c Q,A"
  shows "Γ,Θ⊨_tF P merge_guards c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume exec_merge: "Γ⊨⟨merge_guards c,Normal s⟩ → t"
  from exec_merge_guards_to_exec [OF exec_merge]
  have exec: "Γ⊨⟨c,Normal s⟩ → t" .
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from cvalidt_postD [OF valid [rule_format] ctxt exec P t_notin_F]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨c ↓ Normal s".
  thus "Γ⊨merge_guards c ↓ Normal s"
    by (rule terminates_to_terminates_merge_guards)
qed

lemma MergeGuardsI:
  assumes deriv: "Γ,Θ⊨_tF P c Q,A"
  shows "Γ,Θ⊨_tF P merge_guards c Q,A"
apply (rule hoaret_complete')
apply (rule MergeGuardsI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done

lemma MergeGuardsD_sound:
  assumes valid: "Γ,Θ⊨_tF P merge_guards c Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  from exec_to_exec_merge_guards [OF exec]
  have exec_merge: "Γ⊨⟨merge_guards c,Normal s⟩ → t".
  assume P: "s ∈ P"
  assume t_notin_F: "t ∉ Fault ` F"
  from cvalidt_postD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨merge_guards c ↓ Normal s".
  thus "Γ⊨c ↓ Normal s"
    by (rule terminates_merge_guards_to_terminates)
qed

lemma MergeGuardsD:
  assumes deriv: "Γ,Θ⊨_tF P merge_guards c Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
apply (rule hoaret_complete')
apply (rule MergeGuardsD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done


lemma SubsetGuards_sound:
  assumes c_c': "c ⊆_g c'"
  assumes valid: "Γ,Θ⊨_t{} P c' Q,A"
  shows "Γ,Θ⊨_t{} P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_t{} P (Call p) Q,A"
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  from exec_to_exec_subseteq_guards [OF c_c' exec] obtain t' where
    exec_c': "Γ⊨⟨c',Normal s⟩ → t'" and
    t'_noFault: "¬ isFault t' ⟶ t' = t"
    by blast
  assume P: "s ∈ P"
  assume t_noFault: "t ∉ Fault ` {}"
  from cvalidt_postD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by auto
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨<sub>t{}</sub> P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have termi_c': "Γ⊨c' ↓ Normal s".
  from cvalidt_postD [OF valid ctxt _ P]
  have noFault_c': "Γ⊨⟨c',Normal s⟩ →∉Fault ` UNIV"
    by (auto simp add: final_notin_def)
  from termi_c' c_c' noFault_c'
  show "Γ⊨c ↓ Normal s"
    by (rule terminates_fewer_guards)
qed

lemma SubsetGuards:
  assumes c_c': "c ⊆_g c'"
  assumes deriv: "Γ,Θ⊨_t{} P c' Q,A"
  shows "Γ,Θ⊨_t{} P c Q,A"
apply (rule hoaret_complete')
apply (rule SubsetGuards_sound [OF c_c'])
apply (iprover intro: hoaret_sound [OF deriv])
done

lemma NormalizeD_sound:
  assumes valid: "Γ,Θ⊨_tF P (normalize c) Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume exec: "Γ⊨⟨c,Normal s⟩ → t"
  hence exec_norm: "Γ⊨⟨normalize c,Normal s⟩ → t"
    by (rule exec_to_exec_normalize)
  assume P: "s ∈ P"
  assume noFault: "t ∉ Fault ` F"
  from cvalidt_postD [OF valid [rule_format] ctxt exec_norm P noFault]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨normalize c ↓ Normal s".
  thus "Γ⊨c ↓ Normal s"
    by (rule terminates_normalize_to_terminates)
qed

lemma NormalizeD:
  assumes deriv: "Γ,Θ⊨_tF P (normalize c) Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
apply (rule hoaret_complete')
apply (rule NormalizeD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done

lemma NormalizeI_sound:
  assumes valid: "Γ,Θ⊨_tF P c Q,A"
  shows "Γ,Θ⊨_tF P (normalize c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume "Γ⊨⟨normalize c,Normal s⟩ → t"
  hence exec: "Γ⊨⟨c,Normal s⟩ → t"
    by (rule exec_normalize_to_exec)
  assume P: "s ∈ P"
  assume noFault: "t ∉ Fault ` F"
  from cvalidt_postD [OF valid [rule_format] ctxt exec P noFault]
  show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
  fix s
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨_tF P (Call p) Q,A"
  assume P: "s ∈ P"
  from cvalidt_termD [OF valid ctxt P]
  have "Γ⊨ c ↓ Normal s".
  thus "Γ⊨normalize c ↓ Normal s"
    by (rule terminates_to_terminates_normalize)
qed

lemma NormalizeI:
  assumes deriv: "Γ,Θ⊨_tF P c Q,A"
  shows "Γ,Θ⊨_tF P (normalize c) Q,A"
apply (rule hoaret_complete')
apply (rule NormalizeI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done

subsubsection ‹Restricting the Procedure Environment›

lemma validt_restrict_to_validt:
assumes validt_c: "Γ|⊨_tF P c Q,A"
shows "Γ⊨_tF P c Q,A"
proof -
  from validt_c
  have valid_c: "Γ|⊨_F P c Q,A" by (simp add: validt_def)
  hence "Γ⊨_F P c Q,A" by (rule valid_restrict_to_valid)
  moreover
  {
    fix s
    assume P: "s ∈ P"
    have "Γ⊨c↓Normal s"
    proof -
      from P validt_c have "Γ|⊨c↓Normal s"
        by (auto simp add: validt_def)
      moreover
      from P valid_c
      have "Γ|⊨⟨c,Normal s⟩ →∉{Stuck}"
        by (auto simp add: valid_def  final_notin_def)
      ultimately show ?thesis
        by (rule terminates_restrict_to_terminates)
    qed
   }
   ultimately show ?thesis
     by (auto simp add: validt_def)
qed


lemma augment_procs:
assumes deriv_c: "Γ|,{}⊨_tF P c Q,A"
shows "Γ,{}⊨_tF P c Q,A"
  apply (rule hoaret_complete)
  apply (rule validt_restrict_to_validt)
  apply (insert hoaret_sound [OF deriv_c])
  by (simp add: cvalidt_def)

subsubsection ‹Miscellaneous›

lemma augment_Faults:
assumes deriv_c: "Γ,{}⊨_tF P c Q,A"
assumes F: "F ⊆ F'"
shows "Γ,{}⊨_tF' P c Q,A"
  apply (rule hoaret_complete)
  apply (rule validt_augment_Faults [OF _ F])
  apply (insert hoaret_sound [OF deriv_c])
  by (simp add: cvalidt_def)

lemma TerminationPartial_sound:
  assumes "termination": "∀s ∈ P. Γ⊨c↓Normal s"
  assumes partial_corr: "Γ,Θ⊨_F P c Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
using "termination" partial_corr
by (auto simp add: cvalidt_def validt_def cvalid_def)

lemma TerminationPartial:
  assumes partial_deriv: "Γ,Θ⊨_F P c Q,A"
  assumes "termination": "∀s ∈ P. Γ⊨c↓Normal s"
  shows "Γ,Θ⊨_tF P c Q,A"
  apply (rule hoaret_complete')
  apply (rule TerminationPartial_sound [OF "termination"])
  apply (rule hoare_sound [OF partial_deriv])
  done

lemma TerminationPartialStrip:
  assumes partial_deriv: "Γ,Θ⊨_F P c Q,A"
  assumes "termination": "∀s ∈ P. strip F' Γ⊨strip_guards F' c↓Normal s"
  shows "Γ,Θ⊨_tF P c Q,A"
proof -
  from "termination" have "∀s ∈ P. Γ⊨c↓Normal s"
    by (auto intro: terminates_strip_guards_to_terminates
      terminates_strip_to_terminates)
  with partial_deriv
  show ?thesis
    by (rule TerminationPartial)
qed

lemma SplitTotalPartial:
  assumes termi: "Γ,Θ⊨_tF P c Q',A'"
  assumes part: "Γ,Θ⊨_F P c Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
proof -
  from hoaret_sound [OF termi] hoare_sound [OF part]
  have "Γ,Θ⊨_tF P c Q,A"
    by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
  thus ?thesis
    by (rule hoaret_complete')
qed

lemma SplitTotalPartial':
  assumes termi: "Γ,Θ⊨_tUNIV P c Q',A'"
  assumes part: "Γ,Θ⊨_F P c Q,A"
  shows "Γ,Θ⊨_tF P c Q,A"
proof -
  from hoaret_sound [OF termi] hoare_sound [OF part]
  have "Γ,Θ⊨_tF P c Q,A"
    by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
  thus ?thesis
    by (rule hoaret_complete')
qed

end