Theory HoarePartialProps

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

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

*)

section ‹Properties of Partial Correctness Hoare Logic›

theory HoarePartialProps imports HoarePartialDef begin

subsection ‹Soundness›

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

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

subsection ‹Completeness›

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

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


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

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


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

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

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

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

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

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

lemma conseq_extract_state_indep_prop:
  assumes state_indep_prop:"s  P. R"
  assumes to_show: "R  Γ,Θ⊢⇘/FP c Q,A"
  shows "Γ,Θ⊢⇘/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:
    "pdom Γ. Z. Γ,Θ ⊢⇘/F{s. s=Z  ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F))}
        (Call p)
       {t. ΓCall p,Normal Z  Normal t},
       {t. ΓCall p,Normal Z  Abrupt t}"
  shows "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F))} c
             {t. Γc,Normal Z  Normal t},{t. Γc,Normal Z  Abrupt t}"
proof (induct c)
  case Skip
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓSkip,Normal s ⇒∉({Stuck}  Fault ` (-F))} Skip
           {t. ΓSkip,Normal Z  Normal t},{t. ΓSkip,Normal Z  Abrupt t}"
    by (rule hoarep.Skip [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
  case (Basic f)
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓBasic f,Normal s ⇒∉({Stuck}  Fault ` (-F))} Basic f
           {t. ΓBasic f,Normal Z  Normal t},
           {t. ΓBasic f,Normal Z  Abrupt t}"
    by (rule hoarep.Basic [THEN conseqPre])
       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
  case (Spec r)
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓSpec r,Normal s ⇒∉({Stuck}  Fault ` (-F))} Spec r
           {t. ΓSpec r,Normal Z  Normal t},
           {t. ΓSpec r,Normal Z  Abrupt t}"
    apply (rule hoarep.Spec [THEN conseqPre])
    apply (clarsimp simp add: final_notin_def)
    apply (case_tac "t. (Z,t)  r")
    apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
    done
next
  case (Seq c1 c2)
  have hyp_c1: "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F))} c1
                           {t. Γc1,Normal Z  Normal t},
                           {t. Γc1,Normal Z  Abrupt t}"
    using Seq.hyps by iprover
  have hyp_c2: "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F))} c2
                          {t. Γc2,Normal Z  Normal t},
                          {t. Γc2,Normal Z  Abrupt t}"
    using Seq.hyps by iprover
  from hyp_c1
  have "Γ,Θ⊢⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))} c1
              {t. Γc1,Normal Z  Normal t 
                  Γc2,Normal t ⇒∉({Stuck}  Fault ` (-F))},
              {t. ΓSeq c1 c2,Normal Z  Abrupt t}"
    by (rule ConseqMGT)
       (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
             intro: exec.Seq)
  thus "Γ,Θ⊢⇘/F{s. s=Z  ΓSeq c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))}
                   Seq c1 c2
              {t. ΓSeq c1 c2,Normal Z  Normal t},
              {t. ΓSeq c1 c2,Normal Z  Abrupt t}"
  proof (rule hoarep.Seq )
    show "Γ,Θ⊢⇘/F{t. Γc1,Normal Z  Normal t 
                      Γc2,Normal t ⇒∉({Stuck}  Fault ` (-F))}
                   c2
                 {t. ΓSeq c1 c2,Normal Z  Normal t},
                 {t. ΓSeq c1 c2,Normal Z  Abrupt t}"
    proof (rule ConseqMGT [OF hyp_c2],safe)
      fix r t
      assume "Γc1,Normal Z  Normal r" "Γc2,Normal r  Normal t"
      then show "ΓSeq c1 c2,Normal Z  Normal t"
        by (iprover intro: exec.intros)
    next
      fix r t
      assume "Γc1,Normal Z  Normal r" "Γc2,Normal r  Abrupt t"
      then show "ΓSeq c1 c2,Normal Z  Abrupt t"
        by (iprover intro: exec.intros)
    qed
  qed
next
  case (Cond b c1 c2)
  have "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F))} c1
                 {t. Γc1,Normal Z  Normal t},
                 {t. Γc1,Normal Z  Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ⊢⇘/F({s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))}b)
                   c1
                {t. ΓCond b c1 c2,Normal Z  Normal t},
                {t. ΓCond b c1 c2,Normal Z  Abrupt t}"
    by (rule ConseqMGT)
       (fastforce intro: exec.CondTrue simp add: final_notin_def)
  moreover
  have "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F))} c2
                    {t. Γc2,Normal Z  Normal t},
                    {t. Γc2,Normal Z  Abrupt t}"
    using Cond.hyps by iprover
  hence "Γ,Θ⊢⇘/F({s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))}-b)
                  c2
                {t. ΓCond b c1 c2,Normal Z  Normal t},
                {t. ΓCond b c1 c2,Normal Z  Abrupt t}"
    by (rule ConseqMGT)
       (fastforce intro: exec.CondFalse simp add: final_notin_def)
  ultimately
  show "Γ,Θ⊢⇘/F{s. s=Z  ΓCond b c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))}
                 Cond b c1 c2
              {t. ΓCond b c1 c2,Normal Z  Normal t},
              {t. ΓCond b c1 c2,Normal Z  Abrupt t}"
    by (rule hoarep.Cond)
next
  case (While b c)
  let ?unroll = "({(s,t). 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))}"
  let ?A' = "λZ. {t. ΓWhile b c,Normal Z  Abrupt t}"
  show "Γ,Θ⊢⇘/F{s. s=Z  ΓWhile b c,Normal s ⇒∉({Stuck}  Fault ` (-F))}
                While b c
              {t. ΓWhile b c,Normal Z  Normal t},
              {t. ΓWhile b c,Normal Z  Abrupt t}"
  proof (rule ConseqMGT [where ?P'="?P'"
                         and ?Q'="λZ. ?P' Z  - b" and ?A'="?A'"])
    show "Z. Γ,Θ⊢⇘/F(?P' Z) (While b c) (?P' Z  - b),(?A' Z)"
    proof (rule allI, rule hoarep.While)
      fix Z
      from While
      have "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F))} c
                        {t. Γc,Normal Z  Normal t},
                        {t. Γc,Normal Z  Abrupt t}" by iprover
      then show "Γ,Θ⊢⇘/F(?P' Z   b) c (?P' Z),(?A' Z)"
      proof (rule ConseqMGT)
        fix s
        assume  "s {t. (Z, t)  ?unroll 
                      (e. (Z,e)?unroll  eb
                            Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
                               (u. Γc,Normal e Abrupt u 
                                    ΓWhile b c,Normal Z  Abrupt u))}
                    b"
        then obtain
          Z_s_unroll: "(Z,s)  ?unroll" and
          noabort:"e. (Z,e)?unroll  eb
                         Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
                            (u. Γc,Normal e Abrupt u 
                                  ΓWhile b c,Normal Z  Abrupt u)" and
          s_in_b: "sb"
          by blast
        show "s  {t. t = s  Γc,Normal t ⇒∉({Stuck}  Fault ` (-F))} 
        (t. t  {t. Γc,Normal s  Normal t} 
             t  {t. (Z, t)  ?unroll 
                  (e. (Z,e)?unroll   eb
                        Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
                           (u. Γc,Normal e Abrupt u 
                                  ΓWhile b c,Normal Z  Abrupt u))}) 
         (t. t  {t. Γc,Normal s  Abrupt t} 
             t  {t. ΓWhile b c,Normal Z  Abrupt t})"
          (is "?C1  ?C2  ?C3")
        proof (intro conjI)
          from Z_s_unroll noabort s_in_b show ?C1 by blast
        next
          {
            fix t
            assume s_t: "Γc,Normal s  Normal t"
            moreover
            from Z_s_unroll s_t s_in_b
            have "(Z, t)  ?unroll"
              by (blast intro: rtrancl_into_rtrancl)
            moreover note noabort
            ultimately
            have "(Z, t)  ?unroll 
                  (e. (Z,e)?unroll  eb
                         Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
                            (u. Γc,Normal e Abrupt u 
                                  ΓWhile b c,Normal Z  Abrupt u))"
              by iprover
          }
          then show ?C2 by blast
        next
          {
            fix t
            assume s_t:  "Γc,Normal s  Abrupt t"
            from Z_s_unroll noabort s_t s_in_b
            have "ΓWhile b c,Normal Z  Abrupt t"
              by blast
          } thus ?C3 by simp
        qed
      qed
    qed
  next
    fix s
    assume P: "s  {s. s=Z  ΓWhile b c,Normal s ⇒∉({Stuck}  Fault ` (-F))}"
    hence WhileNoFault: "ΓWhile b c,Normal Z ⇒∉({Stuck}  Fault ` (-F))"
      by auto
    show "s  ?P' s 
    (t. t(?P' s  - b)
         t{t. ΓWhile b c,Normal Z  Normal t})
    (t. t?A' s  t?A' Z)"
    proof (intro conjI)
      {
        fix e
        assume "(Z,e)  ?unroll" "e  b"
        from this WhileNoFault
        have "Γc,Normal e ⇒∉({Stuck}  Fault ` (-F)) 
               (u. Γc,Normal e Abrupt u 
                    ΓWhile b c,Normal Z  Abrupt u)" (is "?Prop Z e")
        proof (induct rule: converse_rtrancl_induct [consumes 1])
          assume e_in_b: "e  b"
          assume WhileNoFault: "ΓWhile b c,Normal e ⇒∉({Stuck}  Fault ` (-F))"
          with e_in_b WhileNoFault
          have cNoFault: "Γc,Normal e ⇒∉({Stuck}  Fault ` (-F))"
            by (auto simp add: final_notin_def intro: exec.intros)
          moreover
          {
            fix u assume "Γc,Normal e  Abrupt u"
            with e_in_b have "ΓWhile b c,Normal e  Abrupt u"
              by (blast intro: exec.intros)
          }
          ultimately
          show "?Prop e e"
            by iprover
        next
          fix Z r
          assume e_in_b: "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)
  let ?P = "{s. s=Z  ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F))}"
  from noStuck_Call have "s  ?P. p  dom Γ"
    by (fastforce simp add: final_notin_def )
  then show "Γ,Θ⊢⇘/F?P (Call p)
               {t. ΓCall p,Normal Z  Normal t},
               {t. ΓCall p,Normal Z  Abrupt t}"
  proof (rule conseq_extract_state_indep_prop)
    assume p_definied: "p  dom Γ"
    with MGT_Calls show
      "Γ,Θ⊢⇘/F{s. s=Z 
                 ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F))}
                  (Call p)
                 {t. ΓCall p,Normal Z  Normal t},
                 {t. ΓCall  p,Normal Z  Abrupt t}"
      by (auto)
  qed
next
  case (DynCom c)
  have hyp:
    "s'. Z. Γ,Θ⊢⇘/F{s. s = Z  Γc s',Normal s ⇒∉({Stuck}  Fault ` (-F))} c s'
      {t. Γc s',Normal Z  Normal t},{t. Γc s',Normal Z  Abrupt t}"
    using DynCom by simp
  have hyp':
  "Γ,Θ⊢⇘/F{s. s = Z  ΓDynCom c,Normal s ⇒∉({Stuck}  Fault ` (-F))} c Z
        {t. ΓDynCom c,Normal Z  Normal t},{t. ΓDynCom c,Normal Z  Abrupt t}"
    by (rule ConseqMGT [OF hyp])
       (fastforce simp add: final_notin_def intro: exec.intros)
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓDynCom c,Normal s ⇒∉({Stuck}  Fault ` (-F))}
               DynCom c
             {t. ΓDynCom c,Normal Z  Normal t},
             {t. ΓDynCom c,Normal Z  Abrupt t}"
    apply (rule hoarep.DynCom)
    apply (clarsimp)
    apply (rule hyp' [simplified])
    done
next
  case (Guard f g c)
  have hyp_c: "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc,Normal s ⇒∉({Stuck}  Fault ` (-F))} c
                    {t. Γc,Normal Z  Normal t},
                    {t. Γc,Normal Z  Abrupt t}"
    using Guard by iprover
  show ?case
  proof (cases "f  F")
    case True
    from hyp_c
    have "Γ,Θ⊢⇘/F(g  {s. s = Z 
                    ΓGuard f g c,Normal s ⇒∉({Stuck}  Fault ` (- F))})
             c
           {t. ΓGuard f g c,Normal Z  Normal t},
           {t. ΓGuard f g c,Normal Z  Abrupt t}"
      apply (rule ConseqMGT)
      apply (insert True)
      apply (auto simp add: final_notin_def intro: exec.intros)
      done
    from True this
    show ?thesis
      by (rule conseqPre [OF Guarantee]) auto
  next
    case False
    from hyp_c
    have "Γ,Θ⊢⇘/F(g  {s. s=Z  ΓGuard f g c,Normal s ⇒∉({Stuck}  Fault ` (-F))})
           c
           {t. ΓGuard f g c,Normal Z  Normal t},
           {t. ΓGuard f g c,Normal Z  Abrupt t}"
      apply (rule ConseqMGT)
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply (auto simp add: final_notin_def intro: exec.intros)
      done
    then show ?thesis
      apply (rule conseqPre [OF hoarep.Guard])
      apply clarify
      apply (frule Guard_noFaultStuckD [OF _ False])
      apply auto
      done
  qed
next
  case Throw
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓThrow,Normal s ⇒∉({Stuck}  Fault ` (-F))} Throw
              {t. ΓThrow,Normal Z  Normal t},
              {t. ΓThrow,Normal Z  Abrupt t}"
    by (rule conseqPre [OF hoarep.Throw]) (blast intro: exec.intros)
next
  case (Catch c1 c2)
  have "Z. Γ,Θ⊢⇘/F{s. s = Z  Γc1,Normal s ⇒∉({Stuck}  Fault ` (-F))} c1
                  {t. Γc1,Normal Z  Normal t},
                  {t. Γc1,Normal Z  Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊢⇘/F{s. s = Z  ΓCatch c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))} c1
               {t. ΓCatch c1 c2,Normal Z  Normal t},
               {t. Γc1,Normal Z  Abrupt t 
                   ΓCatch c1 c2,Normal Z ⇒∉({Stuck}  Fault ` (-F))}"
    by (rule ConseqMGT)
       (fastforce intro: exec.intros simp add: final_notin_def)
  moreover
  have "Z. Γ,Θ⊢⇘/F{s. s=Z  Γc2,Normal s ⇒∉({Stuck}  Fault ` (-F))} c2
                  {t. Γc2,Normal Z  Normal t},
                  {t. Γc2,Normal Z  Abrupt t}"
    using Catch.hyps by iprover
  hence "Γ,Θ⊢⇘/F{s. Γc1,Normal Z Abrupt s 
                   ΓCatch c1 c2,Normal Z ⇒∉({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  simp add: final_notin_def)
  ultimately
  show "Γ,Θ⊢⇘/F{s. s = Z  ΓCatch c1 c2,Normal s ⇒∉({Stuck}  Fault ` (-F))}
                   Catch c1 c2
              {t. ΓCatch c1 c2,Normal Z  Normal t},
              {t. ΓCatch c1 c2,Normal Z  Abrupt t}"
    by (rule hoarep.Catch)
qed

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

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

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


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


subsection ‹And Now: Some Useful Rules›

subsubsection ‹Consequence›


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

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

lemma "s  P. P' Q' A'. Γ,Θ⊢⇘/FP' c Q',A'  s  P'  Q'  Q  A'  A
            Γ,Θ⊢⇘/FP c Q,A"
  apply (rule LiberalConseq)
  apply (rule ballI)
  apply (drule (1) bspec)
  apply clarify
  apply (rule_tac x=P' in exI)
  apply (rule_tac x=Q' in exI)
  apply (rule_tac x=A' in exI)
  apply auto
  done

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

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

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

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

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

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

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

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


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

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

subsubsection ‹Modify Return›

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

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

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

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

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

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


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


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


subsubsection ‹DynCall›



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

lemma dynProcModifyReturn_sound:
assumes valid_call: "n. Γ,Θ n:⇘/FP dynCall init p return' c Q,A"
assumes valid_modif:
    "s  P. σ. n.
       Γ,Θn:⇘/UNIV{σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "s t. t  Modif (init s)
            return' s t = return s t"
assumes ret_modifAbr: "s t. t  ModifAbr (init s)
                              return' s t = return s t"
shows "Γ,Θ n:⇘/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: "Γ,Θ⊢⇘/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 "Γ,Θ⊢⇘/FP (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
          OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done

lemma dynProcModifyReturn:
assumes dyn_call: "Γ,Θ⊢⇘/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 "Γ,Θ⊢⇘/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: "n. Γ,Θ n:⇘/FP dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
    "s  P. σ. n.
       Γ,Θn:⇘/F{σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "s t. t  Modif (init s)  return' s t = return s t"
assumes ret_modifAbr: "s t. t  ModifAbr (init s)  result_exn (return' s t) t = result_exn (return s t) t"
shows "Γ,Θ n:⇘/FP (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γ n:⇘/FP (Call p) Q,A"
  assume exec: "ΓdynCall_exn f g init p return result_exn c,Normal s =n t"
  assume t_notin_F: "t  Fault ` F"
  assume P: "s  P"
  with valid_modif
  have valid_modif': "σ. n.
    Γ,Θn:⇘/F{σ} Call (p s) (Modif σ),(ModifAbr σ)"
    by blast
  from exec
  have exec_call: "Γmaybe_guard f g (call_exn init (p s) return result_exn c),Normal s =n t"
    by (cases rule: execn_dynCall_exn_Normal_elim)
  then show "t  Normal ` Q  Abrupt ` A"
  proof (cases rule: execn_maybe_guard_Normal_elim_cases)
    case noFault
    from noFault have guards_ok: "s  g" by simp
    from noFault have "Γ call_exn init (p s) return result_exn c,Normal s =n t" by simp
    then show "t  Normal ` Q  Abrupt ` A"

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


lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "n. Γ,Θ n:⇘/FP dynCall init p return' c Q,A"
assumes valid_modif:
    "s  P. σ. n.
       Γ,Θn:⇘/F{σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
    "s t. t  Modif (init s)  return' s t = return s t"
assumes ret_modifAbr: "s t. t  ModifAbr (init s)  return' s t = return s t"
shows "Γ,Θ n:⇘/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: "Γ,Θ⊢⇘/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 "Γ,Θ⊢⇘/FP (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturnSameFaults_sound
        [where Modif=Modif and ModifAbr=ModifAbr,
           OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
  done

lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊢⇘/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 "Γ,Θ⊢⇘/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: "n. Γ,Θ n:⇘/FP c Q,A"
assumes valid_R: "n. Γ,Θ n:⇘/FP c R,B"
shows "Γ,Θ n:⇘/FP c (Q  R),(A  B)"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "(P, p, Q, A)Θ. Γ n:⇘/FP (Call p) Q,A"
  assume exec: "Γc,Normal s =n t"
  assume P: "s  P"
  assume t_notin_F: "t  Fault ` F"
  from valid_Q [rule_format] ctxt exec P t_notin_F have "t  Normal ` Q  Abrupt ` A"
    by (rule cnvalidD)
  moreover
  from valid_R [rule_format] ctxt exec P t_notin_F have "t  Normal ` R  Abrupt ` B"
    by (rule cnvalidD)
  ultimately show "t  Normal ` (Q  R)  Abrupt ` (A  B)"
    by blast
qed

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

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

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

subsubsection ‹Weaken Context›


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

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

subsubsection ‹Guards and Guarantees›

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

lemma SplitGuards:
  assumes c: "(c1 g c2) = Some c"
  assumes deriv_c1: "Γ,Θ⊢⇘/FP c1 Q,A"
  assumes deriv_c2: "Γ,Θ⊢⇘/FP c2 UNIV,UNIV"
  shows "Γ,Θ⊢⇘/FP c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule SplitGuards_sound [OF _ _ c])
using deriv_c1
apply (blast intro: hoare_cnvalid)
using deriv_c2
apply (blast intro: hoare_cnvalid)
done

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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


subsubsection ‹Restricting the Procedure Environment›

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

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

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

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

end