Theory HoareTotalProps

(*
    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: "Γ,Θt⇘/FP c Q,A"
 shows "Γ,Θt⇘/FP c Q,A"
using hoare
proof (induct)
  case (Skip Θ F P A)
  show "Γ,Θt⇘/FP 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 "Γ,Θt⇘/F{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 "Γ,Θt⇘/F{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: "Γ,Θt⇘/FP c1 R,A" by fact
  have valid_c2: "Γ,Θt⇘/FR c2 Q,A" by fact
  show "Γ,Θt⇘/FP Seq c1 c2 Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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 "tNormal ` Q  Abrupt ` A"
    proof (cases r)
      case (Normal r')
      with exec_c2 r
      show "tNormal ` 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)Θ. Γt⇘/FP (Call p) Q,A"
    assume P: "sP"
    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: "rNormal ` 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: "Γ,Θt⇘/F(P  b) c1 Q,A" by fact
  have valid_c2: "Γ,Θt⇘/F(P  - b) c2 Q,A" by fact
  show "Γ,Θt⇘/FP Cond b c1 c2 Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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 "sb")
      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)Θ. Γt⇘/FP (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: "σ. Γ,Θt⇘/F({σ}  P  b) c ({t. (t, σ)  r}  P),A"
    using While.hyps by iprover
  show "Γ,Θt⇘/FP (While b c) (P  - b),A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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: "sb"
        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 "sb" "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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/F(g  P) c Q,A" by fact
  show "Γ,Θt⇘/F(g  P) Guard f g c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/F(g  P) c Q,A" by fact
  have f_F: "f  F" by fact
  show "Γ,Θt⇘/FP Guard f g c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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 τt⇘/F({τ}  P) the (Γ p) Q,A)" by auto
  show "Γ,Θt⇘/FP (Call p) Q,A"
  proof -
    {
      fix τp
      assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
      from wf
      have "τ p P Q A.  τp = (τ,p); (P,p,Q,A)  Specs 
                  Γt⇘/F({τ}  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 "Γt⇘/F(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:
              "Γt⇘/F({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:
              "Γt⇘/F({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 τ. Γt⇘/FP Call p Q,A"
          by (auto simp add: cvalidt_def Specs_wf)
        with ctxt have "(P, p, Q, A)Θ  Specs_wf p τ. Γt⇘/FP Call p Q,A"
          by auto
        with p valid_body
        show "Γt⇘/F({τ}  P) (the (Γ p)) Q,A"
          by (simp add: cvalidt_def) blast
      qed
    }
    note lem = this
    have valid_body':
      "τ. (P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A 
      (P,p,Q,A)Specs. Γt⇘/F({τ}  P) (the (Γ p)) Q,A"
      by (auto intro: lem)
    show "Γ,Θt⇘/FP (Call p) Q,A"
    proof (rule cvalidtI)
      fix s t
      assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "sP. Γ,Θt⇘/FP (c s) Q,A" by simp
  show "Γ,Θt⇘/FP DynCom c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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 "Γ,Θt⇘/FA 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 c1 Q R c2 A)
  have valid_c1: "Γ,Θt⇘/FP c1 Q,R" by fact
  have valid_c2: "Γ,Θt⇘/FR c2 Q,A" by fact
  show "Γ,Θt⇘/FP Catch c1 c2 Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
    assume exec: "ΓCatch c1 c2,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: "Γc1,Normal s  Abrupt s'"
      assume exec_c2: "Γc2,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: "Γc1,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)Θ. Γt⇘/FP (Call p) Q,A"
    assume P: "s  P"
    show "ΓCatch 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  Abrupt r"
        from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
        have r: "Abrupt rNormal ` Q  Abrupt ` R"
          by auto
        hence "Abrupt rAbrupt ` R" by fast
        with cvalidt_termD [OF valid_c2 ctxt] exec_c1
        have "Γc2  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'. (Γ,Θt⇘/FP' c Q',A')  s  P' Q'  Q  A'  A)" by blast
  show "Γ,Θt⇘/FP c Q,A"
  proof (rule cvalidtI)
    fix s t
    assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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': "Γ,Θt⇘/FP' 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)Θ. Γt⇘/FP (Call p) Q,A"
    assume P: "s  P"
    show "Γc  Normal s"
    proof -
      from P adapt
      obtain P' and Q' and  A' where
        "Γ,Θt⇘/FP' 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 "Γ,Θt⇘/FP (Call p) Q,A"
    by (auto simp add: cvalidt_def )
next
  case ExFalso thus ?case by iprover
qed

lemma hoaret_sound':
"Γ,{}t⇘/FP c Q,A  Γt⇘/FP c Q,A"
  apply (drule hoaret_sound)
  apply (simp add: cvalidt_def)
  done

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

subsection ‹Completeness›

lemma MGT_valid:
"Γt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F))  ΓcNormal 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))  ΓcNormal 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))  ΓcNormal s}"
  thus "ΓcNormal s"
    by blast
qed

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

lemma MGT_implies_complete:
  assumes MGT: "Z. Γ,{}t⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                                 ΓcNormal s}
                              c
                            {t. Γc,Normal Z  Normal t},
                            {t. Γc,Normal Z  Abrupt t}"
  assumes valid: "Γt⇘/FP c Q,A"
  shows "Γ,{}t⇘/FP 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  Γ,Θt⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP 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. Γ,Θt⇘/F{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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                          ΓcNormal s}
               c
             {t. Γc,Normal Z  Normal t},{t. Γc,Normal Z  Abrupt t}"
proof (induct c)
  case Skip
  show "Γ,Θt⇘/F{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 "Γ,Θt⇘/F{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 "Γ,Θt⇘/F{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. Γ,Θt⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                                Γc1Normal s}
                            c1
                           {t. Γc1,Normal Z  Normal t},
                           {t. Γc1,Normal Z  Abrupt t}"
    using Seq.hyps by iprover
  have hyp_c2: " Z. Γ,Θt⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                                 Γc2Normal s}
                              c2
                            {t. Γc2,Normal Z  Normal t},
                            {t. Γc2,Normal Z  Abrupt t}"
    using Seq.hyps by iprover
  from hyp_c1
  have "Γ,Θt⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                ΓSeq c1 c2Normal s} c1
    {t. Γc1,Normal Z  Normal t  Γc2,Normal t ⇒∉({Stuck}  Fault ` (-F)) 
        Γc2Normal 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 "Γ,Θt⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓSeq c1 c2Normal 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 "Γ,Θt⇘/F{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. Γ,Θt⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                         Γc1Normal s}
                     c1
                   {t. Γc1,Normal Z  Normal t},
                   {t. Γc1,Normal Z  Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θt⇘/F({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. Γ,Θt⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                               Γc2Normal s}
                      c2
                    {t. Γc2,Normal Z  Normal t},
                    {t. Γc2,Normal Z  Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θt⇘/F({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 "Γ,Θt⇘/F{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). sb  Γc,Normal s  Normal t})*"
  let ?P' = "λZ. {t. (Z,t)?unroll 
                    (e. (Z,e)?unroll  eb
                          Γ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  sb 
                    Γc,Normal s  Normal t}"
  show "Γ,Θt⇘/F{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. Γ,Θt⇘/F(?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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                                  ΓcNormal s}
                                c
                              {t. Γc,Normal Z  Normal t},
                              {t. Γc,Normal Z  Abrupt t}" by iprover
      show "σ. Γ,Θt⇘/F({σ}  ?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  eb
                            Γ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  eb
                         Γ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: "sb"
          by blast
        show "s  {t. t = s  Γc,Normal t ⇒∉({Stuck}  Fault ` (-F)) 
                       ΓcNormal t} 
        (t. t  {t. Γc,Normal s  Normal t} 
             t  {t. (t,σ)  ?r} 
                 {t. (Z, t)  ?unroll 
                     (e. (Z,e)?unroll   eb
                            Γ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  eb
                         Γ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: "eb"
          assume WhileNoFault: "ΓWhile b c,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
          assume hyp: "eb;Γ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
    "Γ,Θt⇘/F{s. s=Z 
                 ΓCall p ,Normal s ⇒∉({Stuck}  Fault ` (-F))
                 ΓCall  pNormal 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. Γ,Θt⇘/F{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':
  "Γ,Θt⇘/F{s. s = Z  ΓDynCom c,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
            ΓDynCom cNormal 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 "Γ,Θt⇘/F{s. s=Z  ΓDynCom c,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓDynCom cNormal 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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                              ΓcNormal s}
                     c
                   {t. Γc,Normal Z  Normal t},
                   {t. Γc,Normal Z  Abrupt t}"
    using Guard by iprover
  show "Γ,Θt⇘/F{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 "Γ,Θt⇘/F(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 "Γ,Θt⇘/F(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 "Γ,Θt⇘/F{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 c1 c2)
  have "Z. Γ,Θt⇘/F{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 Catch.hyps by iprover
  hence "Γ,Θt⇘/F{s. s = Z  ΓCatch c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                   ΓCatch c1 c2  Normal s}
                c1
               {t. ΓCatch c1 c2,Normal Z  Normal t},
               {t. Γc1,Normal Z  Abrupt t  Γc2  Normal t 
                   Γc2,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. Γ,Θt⇘/F{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 Catch.hyps by iprover
  hence "Γ,Θt⇘/F{s. Γc1,Normal Z Abrupt s  Γc2  Normal s 
                   Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F))}
               c2
               {t. ΓCatch c1 c2,Normal Z  Normal t},
               {t. ΓCatch c1 c2,Normal Z  Abrupt t}"
      by (rule ConseqMGT)
         (fastforce intro: exec.intros terminates.intros
                   simp add: noFault_def')
  ultimately
  show "Γ,Θt⇘/F{s. s = Z  ΓCatch c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                   ΓCatch c1 c2  Normal s}
                Catch c1 c2
               {t. ΓCatch c1 c2,Normal Z  Normal t},
               {t. ΓCatch c1 c2,Normal Z  Abrupt t}"
    by (rule hoaret.Catch )
qed


lemma Call_lemma':
 assumes Call_hyp:
 "qdom Γ. Z. Γ,Θt⇘/F{s. s=Z  ΓCall q,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                       ΓCall qNormal 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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F))  ΓCall pNormal σ 
                (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 "Γ,Θt⇘/F{s. s = Z  ΓSkip,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓCall p  Normal σ 
                (c'. Γ(Call p,Normal σ) + (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 "Γ,Θt⇘/F{s. s=Z  ΓBasic f,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                   ΓCall pNormal σ 
                (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 "Γ,Θt⇘/F{s. s=Z  ΓSpec r,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                   ΓCall pNormal σ 
                (c'. Γ(Call p,Normal σ) + (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. Γ,Θt⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                     ΓCall pNormal σ 
                 (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. Γ,Θt⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                    ΓCall pNormal σ 
                 (c'. Γ(Call p,Normal σ) + (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: "Γ,Θt⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                    ΓCall pNormal σ 
              (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 pNormal σ 
                  (c'. Γ(Call p,Normal σ) + (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 σ) + (c', Normal Z)"
    assume red: "Seq c1 c2  redexes c'"
    from redexes_subset [OF red] steps_c'
    show "c'. Γ (Call p, Normal σ) + (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 σ) + (c', Normal Z)"
    assume red: "Seq c1 c2  redexes c'"
    assume exec_c1: "Γ c1,Normal Z  Normal t"
    show "c'. Γ (Call p, Normal σ) + (c', Normal t)  c2  redexes c'"
    proof -
      note steps_c'
      also
      from exec_impl_steps_Normal [OF exec_c1]
      have "Γ (c1, Normal Z) * (Skip, Normal t)".
      from steps_redexes_Seq [OF this red]
      obtain c'' where
        steps_c'': "Γ (c', Normal Z) * (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 "Γ,Θt⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                  ΓCall pNormal σ 
              (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. Γ,Θt⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                        ΓCall pNormal σ 
                    (c'. Γ(Call p,Normal σ) + (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
  "Γ,Θt⇘/F({s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
           ΓCall pNormal σ 
           (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. Γ,Θt⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                     ΓCall pNormal σ 
                    (c'. Γ(Call p,Normal σ) + (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
  "Γ,Θt⇘/F({s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
              ΓCall pNormal σ 
           (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
   "Γ,Θt⇘/F{s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
              ΓCall pNormal σ 
           (c'. Γ(Call p,Normal σ) + (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). sb  Γc,Normal s  Normal t})*"
  let ?P' = "λZ. {t. (Z,t)?unroll 
                    (e. (Z,e)?unroll  eb
                          Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
                             (u. Γc,Normal e Abrupt u 
                                  ΓWhile b c,Normal Z  Abrupt u)) 
                    ΓCall pNormal σ 
                  (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  sb 
                    Γc,Normal s  Normal t}"
  show "Γ,Θt⇘/F{s. s=Z  ΓWhile b c,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓCall pNormal σ 
          (c'. Γ(Call p,Normal σ)+(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. Γ,Θt⇘/F(?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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                ΓCall pNormal σ 
               (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 "σ. Γ,Θt⇘/F({σ}  ?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  eb
                            Γ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')}
                    b"
        then obtain c' where
          s_eq_τ: "s=τ" and
          Z_s_unroll: "(Z,s)  ?unroll" and
          noabort:"e. (Z,e)?unroll  eb
                         Γ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: "sb"
          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 σ) + (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   eb
                            Γ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  eb
                         Γ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')"
              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 pNormal σ 
                   (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: "eb"
          assume WhileNoFault: "ΓWhile b c,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
          assume hyp: "eb;Γ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 pNormal σ 
              (c'. Γ(Call p,Normal σ) + (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
      "qdom Γ. Z.
        Γ,Θt⇘/F{s. s=Z  ΓCall q,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                        ΓCall qNormal 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. Γ,Θt⇘/F{s. s=Z  ΓCall q,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                     ΓCall qNormal 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
     "Γ,Θt⇘/F?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 σ) + (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 σ) + (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. Γ,Θt⇘/F{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':
    "Γ,Θt⇘/F{s. s=Z  ΓDynCom c,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓCall p  Normal σ 
               (c'. Γ(Call p,Normal σ) + (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 σ) + (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 σ) + (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. Γ,Θt⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
              ΓCall pNormal σ 
            (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 "Γ,Θt⇘/F{s. s=Z  ΓGuard f g c ,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                  ΓCall pNormal σ 
            (c'. Γ(Call p,Normal σ) + (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 "Γ,Θt⇘/F(g  {s. s=Z 
                     ΓGuard f g c ,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓCall pNormal σ 
            (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))" "Zg"
      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 "Γ,Θt⇘/F(g  {s. s=Z 
                     ΓGuard f g c ,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                 ΓCall pNormal σ 
            (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))"
      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 "Γ,Θt⇘/F{s. s=Z  ΓThrow,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                  ΓCall pNormal σ 
                (c'. Γ(Call p, Normal σ) + (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 c1 c2)
  have hyp_c1:
   "Z. Γ,Θt⇘/F{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 Catch.hyps by iprover
  have hyp_c2:
   "Z. Γ,Θt⇘/F{s. s= Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                     ΓCall p Normal σ 
                (c'. Γ(Call p,Normal σ) + (c',Normal s)  c2  redexes c')}
               c2
              {t. Γc2,Normal Z  Normal t},{t. Γc2,Normal Z  Abrupt t}"
    using Catch.hyps by iprover
  have
    "Γ,Θt⇘/F{s. s = Z  ΓCatch c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
               ΓCall p Normal σ 
            (c'. Γ(Call p,Normal σ)+(c',Normal s) 
                   Catch c1 c2  redexes c')}
            c1
           {t. ΓCatch c1 c2,Normal Z  Normal t},
           {t. Γc1,Normal Z  Abrupt t 
               Γc2,Normal t ⇒∉({Stuck}  Fault`(-F))  ΓCall p  Normal σ 
               (c'. Γ(Call p,Normal σ) + (c',Normal t)  c2  redexes c')}"
  proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
    assume "ΓCatch c1 c2,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
    thus "Γc1,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
      by (fastforce simp add: final_notin_def intro: exec.intros)
  next
    fix c'
    assume steps: "Γ (Call p, Normal σ) + (c', Normal Z)"
    assume c': "Catch c1 c2  redexes c'"
    from steps redexes_subset [OF this]
    show "c'. Γ (Call p, Normal σ) + (c', Normal Z)  c1  redexes c'"
      by (auto iff:  root_in_redexes)
  next
    fix t
    assume "Γc1,Normal Z  Normal t"
    thus "ΓCatch c1 c2,Normal Z  Normal t"
      by (auto intro: exec.intros)
  next
    fix t
    assume "ΓCatch c1 c2,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
      "Γc1,Normal Z  Abrupt t"
    thus "Γc2,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 σ) + (c', Normal Z)"
    assume red: "Catch c1 c2  redexes c'"
    assume exec_c1: "Γ c1,Normal Z  Abrupt t"
    show "c'. Γ (Call p, Normal σ) + (c', Normal t)  c2  redexes c'"
    proof -
      note steps_c'
      also
      from exec_impl_steps_Normal_Abrupt [OF exec_c1]
      have "Γ (c1, Normal Z) * (Throw, Normal t)".
      from steps_redexes_Catch [OF this red]
      obtain c'' where
        steps_c'': "Γ (c', Normal Z) * (c'', Normal t)" and
        Catch: "Catch Throw c2  redexes c''"
        by blast
      note steps_c''
      also
      have step_Catch: "Γ (Catch Throw c2,Normal t)  (c2,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: "c2  redexes c'''"
        by blast
      note step_c'''
      finally show ?thesis
        using c2
        by blast
    qed
  qed
  moreover
  have "Γ,Θt⇘/F{t. Γc1,Normal Z  Abrupt t 
                  Γc2,Normal t ⇒∉({Stuck}  Fault ` (-F)) 
                  ΓCall p  Normal σ 
                  (c'. Γ(Call p,Normal σ) + (c',Normal t)  c2  redexes c')}
               c2
              {t. ΓCatch c1 c2,Normal Z  Normal t},
              {t. ΓCatch c1 c2,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. Γ,Θt⇘/F{s. s=Z  ΓCall q,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                    ΓCall qNormal 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. Γ,Θt⇘/F({σ}  {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. Γ,Θt⇘/F{s. s=Z  ΓCall q,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                    ΓCall qNormal 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. Γ,Θt⇘/F({σ}  {s. s=Z  ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                                 ΓCall pNormal 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.
  Γ,Θt⇘/F{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 pNormal 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 ` (pdom Γ. Z. {x p Z}) =  (pdom Γ. 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.
  Γ,{}t⇘/F{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 = (pdom Γ. Z.
            {({s. s=Z 
              ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
              ΓCall pNormal 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 σt⇘/F({σ} 
                 {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 σt⇘/F({σ} 
                 {s. s = Z  ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
                  ΓCall pNormal 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="(pdom Γ. Z.
            {({s. s=Z 
              ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F)) 
              ΓCall pNormal 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: "Γt⇘/FP c Q,A  Γ,{}t⇘/FP c Q,A"
  by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call])

lemma hoaret_complete':
  assumes cvalid: "Γ,Θt⇘/FP c Q,A"
  shows  "Γ,Θt⇘/FP c Q,A"
proof (cases "Γt⇘/FP c Q,A")
  case True
  hence "Γ,{}t⇘/FP c Q,A"
    by (rule hoaret_complete)
  thus "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (call_exn init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  hence "(P, p, Q, A)Θ. Γ ⊨⇘/FP (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/UNIVP (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)Θ. Γt⇘/FP (Call p) Q,A"
  hence "(P, p, Q, A)Θ. Γ ⊨⇘/FP (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/UNIVP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP (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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP (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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (call_exn init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  hence ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/FP (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)Θ. Γt⇘/FP (Call p) Q,A"
  hence ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP (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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP (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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "sP. σ. Γ,Θ ⊨⇘/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 "Γ,Θt⇘/FP (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  hence "(P, p, Q, A)Θ. Γ ⊨⇘/FP (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/UNIVP (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':
    "σ. Γ,Θ⊨⇘/UNIV{σ} (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)Θ. Γt⇘/FP (Call p) Q,A"
  hence "(P, p, Q, A)Θ. Γ ⊨⇘/FP (Call p) Q,A"
    by (auto simp add: validt_def)
  then have ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/UNIVP (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: "Γ,Θt⇘/FP dynCall init p return' c Q,A"
assumes valid_modif:
    "sP. σ. Γ,Θ ⊨⇘/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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "sP. σ. Γ,Θ ⊨⇘/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 "Γ,Θt⇘/FP (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  hence ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/FP (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':
    "σ. Γ,Θ⊨⇘/F{σ} (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)Θ. Γt⇘/FP (Call p) Q,A"
  hence ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/FP (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: "Γ,Θt⇘/FP dynCall init p return' c Q,A"
assumes valid_modif:
    "sP. σ. Γ,Θ ⊨⇘/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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP 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 "Γ,Θt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  assumes valid_R: "Γ,Θt⇘/FP c R,B"
  shows "Γ,Θt⇘/FP c (Q  R),(A  B)"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  assumes deriv_R: "Γ,Θt⇘/FP c R,B"
  shows "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP c Q,A"
  assumes validG: "Γ,Θt⇘/GP' c R,X"
  assumes F_G: "F  G"
  assumes P_P': "P  P'"
  shows "Γ,Θt⇘/FP c (Q  R),(A  X)"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  with F_G have ctxt': "(P, p, Q, A)Θ. Γt⇘/GP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  assumes validG: "Γ,Θt⇘/GP' c R,X"
  assumes F_G: "F  G"
  assumes P_P': "P  P'"
  shows "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP c1 Q,A"
  assumes valid_c2: "Γ,Θ⊨⇘/FP c2 UNIV,UNIV"
  assumes c: "(c1 g c2) = Some c"
  shows "Γ,Θt⇘/FP c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (Call p) Q,A"
  hence ctxt': "(P, p, Q, A)Θ. Γ ⊨⇘/FP (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 "Γc1,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 "Γc1,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 "Γc1,Normal s  Fault f  Γc2,Normal s  Fault f"
      by auto
    then show ?thesis
    proof (cases rule: disjE [consumes 1])
      assume "Γc1,Normal s  Fault f"
      from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F
      show ?thesis
        by blast
    next
      assume "Γc2,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 "Γc1,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)Θ. Γt⇘/FP (Call p) Q,A"
  assume P: "s  P"
  show "Γc  Normal s"
  proof -
    from valid_c1 ctxt P
    have "Γc1  Normal s"
      by (rule cvalidt_termD)
    with c show ?thesis
      by (rule inter_guards_terminates)
  qed
qed

lemma SplitGuards:
  assumes c: "(c1 g c2) = Some c"
  assumes deriv_c1: "Γ,Θt⇘/FP c1 Q,A"
  assumes deriv_c2: "Γ,Θ⊢⇘/FP c2 UNIV,UNIV"
  shows "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP 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)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP c Q,A"
  assumes validFlip: "Γ,Θ⊨⇘/-FP 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)Θ. Γt⇘/FP (Call p) Q,A"
    by (auto intro: valid_augment_Faults simp add: validt_def)
  from ctxt have ctxtFlip: "(P, p, Q, A)Θ. Γ⊨⇘/-FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  assumes derivFlip: "Γ,Θ⊢⇘/-FP 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: "Γ,Θt⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP merge_guards c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP 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: "Γ,Θt⇘/FP merge_guards c Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP merge_guards c Q,A"
  shows "Γ,Θt⇘/FP 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)Θ. Γt⇘/{}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: "Γ,Θt⇘/FP (normalize c) Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP (normalize c) Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
apply (rule hoaret_complete')
apply (rule NormalizeD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done

lemma NormalizeI_sound:
  assumes valid: "Γ,Θt⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP (normalize c) Q,A"
proof (rule cvalidtI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γt⇘/FP (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)Θ. Γt⇘/FP (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: "Γ,Θt⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP (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: "Γ|⇘M⇙⊨t⇘/FP c Q,A"
shows "Γt⇘/FP c Q,A"
proof -
  from validt_c
  have valid_c: "Γ|⇘M⇙⊨⇘/FP c Q,A" by (simp add: validt_def)
  hence "Γ⊨⇘/FP c Q,A" by (rule valid_restrict_to_valid)
  moreover
  {
    fix s
    assume P: "s  P"
    have "ΓcNormal s"
    proof -
      from P validt_c have "Γ|⇘McNormal s"
        by (auto simp add: validt_def)
      moreover
      from P valid_c
      have "Γ|⇘Mc,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: "Γ|⇘M,{}t⇘/FP c Q,A"
shows "Γ,{}t⇘/FP 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: "Γ,{}t⇘/FP c Q,A"
assumes F: "F  F'"
shows "Γ,{}t⇘/F'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. ΓcNormal s"
  assumes partial_corr: "Γ,Θ⊨⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
using "termination" partial_corr
by (auto simp add: cvalidt_def validt_def cvalid_def)

lemma TerminationPartial:
  assumes partial_deriv: "Γ,Θ⊢⇘/FP c Q,A"
  assumes "termination": "s  P. ΓcNormal s"
  shows "Γ,Θt⇘/FP 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: "Γ,Θ⊢⇘/FP c Q,A"
  assumes "termination": "s  P. strip F' Γstrip_guards F' cNormal s"
  shows "Γ,Θt⇘/FP c Q,A"
proof -
  from "termination" have "s  P. ΓcNormal 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: "Γ,Θt⇘/FP c Q',A'"
  assumes part: "Γ,Θ⊢⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
proof -
  from hoaret_sound [OF termi] hoare_sound [OF part]
  have "Γ,Θt⇘/FP 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: "Γ,Θt⇘/UNIVP c Q',A'"
  assumes part: "Γ,Θ⊢⇘/FP c Q,A"
  shows "Γ,Θt⇘/FP c Q,A"
proof -
  from hoaret_sound [OF termi] hoare_sound [OF part]
  have "Γ,Θt⇘/FP c Q,A"
    by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
  thus ?thesis
    by (rule hoaret_complete')
qed

end