Quelle  HoarePartial.thy

(*
    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 ‹Derived Hoare Rules for Partial Correctness›

theory HoarePartial imports HoarePartialProps begin

lemma conseq_no_aux:
  "[Γ,Θ⊨_F P' c Q',A';
    ∀s. s ∈ P ⟶ (s∈P' ∧ (Q' ⊆ Q) ∧ (A' ⊆ A))]
  ==>
  Γ,Θ⊨_F P c Q,A"
  by (rule conseq [where P'="λZ. P'" and Q'="λZ. Q'" and A'="λZ. A'"]) auto


lemma conseq_exploit_pre:
             "[∀s ∈ P. Γ,Θ⊨_F ({s} ∩ P) c Q,A]
              ==>
              Γ,Θ⊨_F P c Q,A"
  apply (rule Conseq)
  apply clarify
  apply (rule_tac x="{s} ∩ P" in exI)
  apply (rule_tac x="Q" in exI)
  apply (rule_tac x="A" in exI)
  by simp


lemma conseq:"[∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z);
              ∀s. s ∈ P ⟶ (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A))]
              ==>
              Γ,Θ⊨_F P c Q,A"
  by (rule Conseq') blast

lemma Lem: "[∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z);
             P ⊆ {s. ∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A)}]
             ==>
             Γ,Θ⊨_F P (lem x c) Q,A"
  apply (unfold lem_def)
  apply (erule conseq)
  apply blast
  done

lemma LemAnno:
assumes conseq:  "P ⊆ {s. ∃Z. s∈P' Z ∧
                     (∀t. t ∈ Q' Z ⟶ t ∈ Q) ∧ (∀t. t ∈ A' Z ⟶ t ∈ A)}"
assumes lem: "∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z)"
shows "Γ,Θ⊨_F P (lem x c) Q,A"
  apply (rule Lem [OF lem])
  using conseq
  by blast

lemma LemAnnoNoAbrupt:
assumes conseq:  "P ⊆ {s. ∃Z. s∈P' Z ∧ (∀t. t ∈ Q' Z ⟶ t ∈ Q)}"
assumes lem: "∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),{}"
shows "Γ,Θ⊨_F P (lem x c) Q,{}"
  apply (rule Lem [OF lem])
  using conseq
  by blast

lemma TrivPost: "∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z)
                 ==>
                 ∀Z. Γ,Θ⊨_F (P' Z) c UNIV,UNIV"
apply (rule allI)
apply (erule conseq)
apply auto
done

lemma TrivPostNoAbr: "∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),{}
                 ==>
                 ∀Z. Γ,Θ⊨_F (P' Z) c UNIV,{}"
apply (rule allI)
apply (erule conseq)
apply auto
done

lemma conseq_under_new_pre:"[Γ,Θ⊨_F P' c Q',A';
        ∀s ∈ P. s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A]
\<Longrightarrow> Γ,Θ⊨_F P c Q,A"
apply (rule conseq)
apply (rule allI)
apply assumption
apply auto
done

lemma conseq_Kleymann:"[∀Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z);
              ∀s ∈ P. (∃Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A))]
              ==>
              Γ,Θ⊨_F P c Q,A"
  by (rule Conseq') blast

lemma DynComConseq:
  assumes "P ⊆ {s. ∃P' Q' A'. Γ,Θ⊨_F P' (c s) Q',A' ∧ P ⊆ P' ∧ Q' ⊆ Q ∧ A' ⊆ A}"
  shows "Γ,Θ⊨_F P DynCom c Q,A"
  using assms
  apply -
  apply (rule DynCom)
  apply clarsimp
  apply (rule Conseq)
  apply clarsimp
  apply blast
  done

lemma SpecAnno:
 assumes consequence: "P ⊆ {s. (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A))}"
 assumes spec: "∀Z. Γ,Θ⊨_F (P' Z) (c Z) (Q' Z),(A' Z)"
 assumes bdy_constant:  "∀Z. c Z = c undefined"
 shows   "Γ,Θ⊨_F P (specAnno P' c Q' A') Q,A"
proof -
  from spec bdy_constant
  have "∀Z. Γ,Θ⊨_F ((P' Z)) (c undefined) (Q' Z),(A' Z)"
    apply -
    apply (rule allI)
    apply (erule_tac x=Z in allE)
    apply (erule_tac x=Z in allE)
    apply simp
    done
  with consequence show ?thesis
    apply (simp add: specAnno_def)
    apply (erule conseq)
    apply blast
    done
qed

lemma SpecAnno':
 "[P ⊆ {s. ∃ Z. s∈P' Z ∧
            (∀t. t ∈ Q' Z ⟶ t ∈ Q) ∧ (∀t. t ∈ A' Z ⟶ t ∈ A)};
   ∀Z. Γ,Θ⊨_F (P' Z) (c Z) (Q' Z),(A' Z);
   ∀Z. c Z = c undefined
  ] ==>
    Γ,Θ⊨_F P (specAnno P' c Q' A') Q,A"
apply (simp only: subset_iff [THEN sym])
apply (erule (1) SpecAnno)
apply assumption
done


lemma SpecAnnoNoAbrupt:
 "[P ⊆ {s. ∃ Z. s∈P' Z ∧
            (∀t. t ∈ Q' Z ⟶ t ∈ Q)};
   ∀Z. Γ,Θ⊨_F (P' Z) (c Z) (Q' Z),{};
   ∀Z. c Z = c undefined
  ] ==>
    Γ,Θ⊨_F P (specAnno P' c Q' (λs. {})) Q,A"
apply (rule SpecAnno')
apply auto
done

lemma Skip: "P ⊆ Q ==> Γ,Θ⊨_F P Skip Q,A"
  by (rule hoarep.Skip [THEN conseqPre],simp)

lemma Basic: "P ⊆ {s. (f s) ∈ Q} ==> Γ,Θ⊨_F P (Basic f) Q,A"
  by (rule hoarep.Basic [THEN conseqPre])

lemma BasicCond:
  "[P ⊆ {s. (b s ⟶ f s∈Q) ∧ (¬ b s ⟶ g s∈Q)}] ==>
   Γ,Θ⊨_F P Basic (λs. if b s then f s else g s) Q,A"
  apply (rule Basic)
  apply auto
  done

lemma Spec: "P ⊆ {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)}
            ==> Γ,Θ⊨_F P (Spec r) Q,A"
by (rule hoarep.Spec [THEN conseqPre])

lemma SpecIf:
  "[P ⊆ {s. (b s ⟶ f s ∈ Q) ∧ (¬ b s ⟶ g s ∈ Q ∧ h s ∈ Q)}] ==>
   Γ,Θ⊨_F P Spec (if_rel b f g h) Q,A"
  apply (rule Spec)
  apply (auto simp add: if_rel_def)
  done


lemma Seq [trans, intro?]:
  "[Γ,Θ⊨_F P c₁ R,A; Γ,Θ⊨_F R c₂ Q,A] ==> Γ,Θ⊨_F P (Seq c₁ c₂) Q,A"
  by (rule hoarep.Seq)

lemma SeqSame:
  "[Γ,Θ⊨_F P c₁ Q,A; Γ,Θ⊨_F Q c₂ Q,A] ==> Γ,Θ⊨_F P (Seq c₁ c₂) Q,A"
  by (rule hoarep.Seq)


lemma SeqSwap:
  "[Γ,Θ⊨_F R c2 Q,A; Γ,Θ⊨_F P c1 R,A] ==> Γ,Θ⊨_F P (Seq c1 c2) Q,A"
  by (rule Seq)

lemma BSeq:
  "[Γ,Θ⊨_F P c₁ R,A; Γ,Θ⊨_F R c₂ Q,A] ==> Γ,Θ⊨_F P (bseq c₁ c₂) Q,A"
  by (unfold bseq_def) (rule Seq)

lemma BSeqSame:
  "[Γ,Θ⊨_F P c₁ Q,A; Γ,Θ⊨_F Q c₂ Q,A] ==> Γ,Θ⊨_F P (bseq c₁ c₂) Q,A"
  by (rule BSeq)

lemma Cond:
  assumes wp: "P ⊆ {s. (s∈b ⟶ s∈P₁) ∧ (s∉b ⟶ s∈P₂)}"
  assumes deriv_c1: "Γ,Θ⊨_F P₁ c₁ Q,A"
  assumes deriv_c2: "Γ,Θ⊨_F P₂ c₂ Q,A"
  shows "Γ,Θ⊨_F P (Cond b c₁ c₂) Q,A"
proof (rule hoarep.Cond [THEN conseqPre])
  from deriv_c1
  show "Γ,Θ⊨_F ({s. (s ∈ b ⟶ s ∈ P₁) ∧ (s ∉ b ⟶ s ∈ P₂)} ∩ b) c₁ Q,A"
    by (rule conseqPre) blast
next
  from deriv_c2
  show "Γ,Θ⊨_F ({s. (s ∈ b ⟶ s ∈ P₁) ∧ (s ∉ b ⟶ s ∈ P₂)} ∩ - b) c₂ Q,A"
    by (rule conseqPre) blast
next
  show "P ⊆ {s. (s∈b ⟶ s∈P₁) ∧ (s∉b ⟶ s∈P₂)}" by (rule wp)
qed


lemma CondSwap:
  "[Γ,Θ⊨_F P1 c1 Q,A; Γ,Θ⊨_F P2 c2 Q,A; P ⊆ {s. (s∈b ⟶ s∈P1) ∧ (s∉b ⟶ s∈P2)}]
   ==>
   Γ,Θ⊨_F P (Cond b c1 c2) Q,A"
  by (rule Cond)

lemma Cond':
  "[P ⊆ {s. (b ⊆ P1) ∧ (- b ⊆ P2)};Γ,Θ⊨_F P1 c1 Q,A; Γ,Θ⊨_F P2 c2 Q,A]
   ==>
   Γ,Θ⊨_F P (Cond b c1 c2) Q,A"
  by (rule CondSwap) blast+

lemma CondInv:
  assumes wp: "P ⊆ Q"
  assumes inv: "Q ⊆ {s. (s∈b ⟶ s∈P₁) ∧ (s∉b ⟶ s∈P₂)}"
  assumes deriv_c1: "Γ,Θ⊨_F P₁ c₁ Q,A"
  assumes deriv_c2: "Γ,Θ⊨_F P₂ c₂ Q,A"
  shows "Γ,Θ⊨_F P (Cond b c₁ c₂) Q,A"
proof -
  from wp inv
  have "P ⊆ {s. (s∈b ⟶ s∈P₁) ∧ (s∉b ⟶ s∈P₂)}"
    by blast
  from Cond [OF this deriv_c1 deriv_c2]
  show ?thesis .
qed

lemma CondInv':
  assumes wp: "P ⊆ I"
  assumes inv: "I ⊆ {s. (s∈b ⟶ s∈P₁) ∧ (s∉b ⟶ s∈P₂)}"
  assumes wp': "I ⊆ Q"
  assumes deriv_c1: "Γ,Θ⊨_F P₁ c₁ I,A"
  assumes deriv_c2: "Γ,Θ⊨_F P₂ c₂ I,A"
  shows "Γ,Θ⊨_F P (Cond b c₁ c₂) Q,A"
proof -
  from CondInv [OF wp inv deriv_c1 deriv_c2]
  have "Γ,Θ⊨_F P (Cond b c₁ c₂) I,A".
  from conseqPost [OF this wp' subset_refl]
  show ?thesis .
qed


lemma switchNil:
  "P ⊆ Q ==> Γ,Θ⊨_F P (switch v []) Q,A"
  by (simp add: Skip)

lemma switchCons:
  "[P ⊆ {s. (v s ∈ V ⟶ s ∈ P₁) ∧ (v s ∉ V ⟶ s ∈ P₂)};
        Γ,Θ⊨_F P₁ c Q,A;
        Γ,Θ⊨_F P₂ (switch v vs) Q,A]
\<Longrightarrow> Γ,Θ⊨_F P (switch v ((V,c)#vs)) Q,A"
  by (simp add: Cond)

lemma Guard:
 "[P ⊆ g ∩ R; Γ,Θ⊨_F R c Q,A]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
apply (rule Guard [THEN conseqPre, of _ _ _ _ R])
apply (erule conseqPre)
apply auto
done

lemma GuardSwap:
 "[ Γ,Θ⊨_F R c Q,A; P ⊆ g ∩ R]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
  by (rule Guard)

lemma Guarantee:
 "[P ⊆ {s. s ∈ g ⟶ s ∈ R}; Γ,Θ⊨_F R c Q,A; f ∈ F]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
apply (rule Guarantee [THEN conseqPre, of _ _ _ _ _ "{s. s ∈ g ⟶ s ∈ R}"])
apply   assumption
apply  (erule conseqPre)
apply auto
done

lemma GuaranteeSwap:
 "[ Γ,Θ⊨_F R c Q,A; P ⊆ {s. s ∈ g ⟶ s ∈ R}; f ∈ F]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
  by (rule Guarantee)

lemma GuardStrip:
 "[P ⊆ R; Γ,Θ⊨_F R c Q,A; f ∈ F]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
apply (rule Guarantee [THEN conseqPre])
apply auto
done

lemma GuardStripSame:
 "[Γ,Θ⊨_F P c Q,A; f ∈ F]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
  by (rule GuardStrip [OF subset_refl])

lemma GuardStripSwap:
 "[Γ,Θ⊨_F R c Q,A; P ⊆ R; f ∈ F]
  ==> Γ,Θ⊨_F P (Guard f g c) Q,A"
  by (rule GuardStrip)

lemma GuaranteeStrip:
 "[P ⊆ R; Γ,Θ⊨_F R c Q,A; f ∈ F]
  ==> Γ,Θ⊨_F P (guaranteeStrip f g c) Q,A"
  by (unfold guaranteeStrip_def) (rule GuardStrip)

lemma GuaranteeStripSwap:
 "[Γ,Θ⊨_F R c Q,A; P ⊆ R; f ∈ F]
  ==> Γ,Θ⊨_F P (guaranteeStrip f g c) Q,A"
  by (unfold guaranteeStrip_def) (rule GuardStrip)

lemma GuaranteeAsGuard:
 "[P ⊆ g ∩ R; Γ,Θ⊨_F R c Q,A]
  ==> Γ,Θ⊨_F P (guaranteeStrip f g c) Q,A"
  by (unfold guaranteeStrip_def) (rule Guard)


lemma GuaranteeAsGuardSwap:
 "[ Γ,Θ⊨_F R c Q,A; P ⊆ g ∩ R]
  ==> Γ,Θ⊨_F P (guaranteeStrip f g c) Q,A"
  by (rule GuaranteeAsGuard)

lemma GuardsNil:
  "Γ,Θ⊨_F P c Q,A ==>
   Γ,Θ⊨_F P (guards [] c) Q,A"
  by simp

lemma GuardsCons:
  "Γ,Θ⊨_F P Guard f g (guards gs c) Q,A ==>
   Γ,Θ⊨_F P (guards ((f,g)#gs) c) Q,A"
  by simp

lemma GuardsConsGuaranteeStrip:
  "Γ,Θ⊨_F P guaranteeStrip f g (guards gs c) Q,A ==>
   Γ,Θ⊨_F P (guards (guaranteeStripPair f g#gs) c) Q,A"
  by (simp add: guaranteeStripPair_def guaranteeStrip_def)

lemma While:
  assumes P_I: "P ⊆ I"
  assumes deriv_body: "Γ,Θ⊨_F (I ∩ b) c I,A"
  assumes I_Q: "I ∩ -b ⊆ Q"
  shows "Γ,Θ⊨_F P (whileAnno b I V c) Q,A"
proof -
  from deriv_body P_I I_Q
  show ?thesis
    apply (simp add: whileAnno_def)
    apply (erule conseqPrePost [OF HoarePartialDef.While])
    apply simp_all
    done
qed

text ‹@{term "J"} will be instantiated by tactic with @{term "gs' ∩ I"} for
 those guards that are not stripped.›
lemma  WhileAnnoG:
  "Γ,Θ⊨_F P (guards gs
                    (whileAnno b J V (Seq c (guards gs Skip)))) Q,A
        ==>
        Γ,Θ⊨_F P (whileAnnoG gs b I V c) Q,A"
  by (simp add: whileAnnoG_def whileAnno_def while_def)


text ‹This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}›

lemma WhileNoGuard':
  assumes P_I: "P ⊆ I"
  assumes deriv_body: "Γ,Θ⊨_F (I ∩ b) c I,A"
  assumes I_Q: "I ∩ -b ⊆ Q"
  shows "Γ,Θ⊨_F P (whileAnno b I V (Seq c Skip)) Q,A"
  apply (rule While [OF P_I _ I_Q])
  apply (rule Seq)
  apply  (rule deriv_body)
  apply (rule hoarep.Skip)
  done

lemma WhileAnnoFix:
assumes consequence: "P ⊆ {s. (∃ Z. s∈I Z ∧ (I Z ∩ -b ⊆ Q)) }"
assumes bdy: "∀Z. Γ,Θ⊨_F (I Z ∩ b) (c Z) (I Z),A"
assumes bdy_constant:  "∀Z. c Z = c undefined"
shows "Γ,Θ⊨_F P (whileAnnoFix b I V c) Q,A"
proof -
  from bdy bdy_constant
  have bdy': "∀Z. Γ,Θ⊨_F (I Z ∩ b) (c undefined) (I Z),A"
    apply -
    apply (rule allI)
    apply (erule_tac x=Z in allE)
    apply (erule_tac x=Z in allE)
    apply simp
    done
  have "∀Z. Γ,Θ⊨_F (I Z) (whileAnnoFix b I V c) (I Z ∩ -b),A"
    apply rule
    apply (unfold whileAnnoFix_def)
    apply (rule hoarep.While)
    apply (rule bdy' [rule_format])
    done
  then
  show ?thesis
    apply (rule conseq)
    using consequence
    by blast
qed

lemma WhileAnnoFix':
assumes consequence: "P ⊆ {s. (∃ Z. s∈I Z ∧
                               (∀t. t ∈ I Z ∩ -b ⟶ t ∈ Q)) }"
assumes bdy: "∀Z. Γ,Θ⊨_F (I Z ∩ b) (c Z) (I Z),A"
assumes bdy_constant:  "∀Z. c Z = c undefined"
shows "Γ,Θ⊨_F P (whileAnnoFix b I V c) Q,A"
  apply (rule WhileAnnoFix [OF _ bdy bdy_constant])
  using consequence by blast

lemma WhileAnnoGFix:
assumes whileAnnoFix:
  "Γ,Θ⊨_F P (guards gs
                (whileAnnoFix b J V (λZ. (Seq (c Z) (guards gs Skip))))) Q,A"
shows "Γ,Θ⊨_F P (whileAnnoGFix gs b I V c) Q,A"
  using whileAnnoFix
  by (simp add: whileAnnoGFix_def whileAnnoFix_def while_def)

lemma Bind:
  assumes adapt: "P ⊆ {s. s ∈ P' s}"
  assumes c: "∀s. Γ,Θ⊨_F (P' s) (c (e s)) Q,A"
  shows "Γ,Θ⊨_F P (bind e c) Q,A"
apply (rule conseq [where P'="λZ. {s. s=Z ∧ s ∈ P' Z}" and Q'="λZ. Q" and
A'="λZ. A"])
apply  (rule allI)
apply  (unfold bind_def)
apply  (rule DynCom)
apply  (rule ballI)
apply  simp
apply  (rule conseqPre)
apply   (rule c [rule_format])
apply  blast
using adapt
apply blast
done

lemma Block_exn:
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
assumes bdy: "∀s. Γ,Θ⊨_F (P' s) bdy {t. return s t ∈ R s t},{t. result_exn (return s t) t ∈ A}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
shows "Γ,Θ⊨_F P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="λZ. {s. s=Z ∧ init s ∈ P' Z}" and Q'="λZ. Q" and
A'="λZ. A"])
prefer 2
using adapt
apply  blast
apply (rule allI)
apply (unfold block_exn_def)
apply (rule DynCom)
apply (rule ballI)
apply clarsimp
apply (rule_tac R="{t. return Z t ∈ R Z t}" in SeqSwap )
apply  (rule_tac  P'="λZ'. {t. t=Z' ∧ return Z t ∈ R Z t}" and
          Q'="λZ'. Q" and A'="λZ'. A" in conseq)
prefer 2 apply simp
apply  (rule allI)
apply  (rule DynCom)
apply  (clarsimp)
apply  (rule SeqSwap)
apply   (rule c [rule_format])
apply  (rule Basic)
apply  clarsimp
apply (rule_tac R="{t. result_exn (return Z t) t ∈ A}" in Catch)
apply  (rule_tac R="{i. i ∈ P' Z}" in Seq)
apply   (rule Basic)
apply   clarsimp
apply  simp
apply  (rule bdy [rule_format])
apply (rule SeqSwap)
apply  (rule Throw)
apply (rule Basic)
apply simp
done

lemma Block:
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
assumes bdy: "∀s. Γ,Θ⊨_F (P' s) bdy {t. return s t ∈ R s t},{t. return s t ∈ A}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
shows "Γ,Θ⊨_F P (block init bdy return c) Q,A"
  unfolding block_def
  by (rule Block_exn [OF adapt bdy c])


lemma BlockSwap:
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes bdy: "∀s. Γ,Θ⊨_F (P' s) bdy {t. return s t ∈ R s t},{t. return s t ∈ A}"
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
shows "Γ,Θ⊨_F P (block init bdy return c) Q,A"
using adapt bdy c
  by (rule Block)


lemma Block_exnSpec:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ (result_exn (return s t) t) ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes bdy: "∀Z. Γ,Θ⊨_F (P' Z) bdy (Q' Z),(A' Z)"
  shows "Γ,Θ⊨_F P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="λZ. {s. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ (result_exn (return s t) t) ∈ A)}" and Q'="λZ. Q" and
A'="λZ. A"])
prefer 2
using adapt
apply  blast
apply (rule allI)
apply (unfold block_exn_def)
apply (rule DynCom)
apply (rule ballI)
apply clarsimp
apply (rule_tac R="{t. return s t ∈ R s t}" in SeqSwap )
apply  (rule_tac  P'="λZ'. {t. t=Z' ∧ return s t ∈ R s t}" and
          Q'="λZ'. Q" and A'="λZ'. A" in conseq)
prefer 2 apply simp
apply  (rule allI)
apply  (rule DynCom)
apply  (clarsimp)
apply  (rule SeqSwap)
apply   (rule c [rule_format])
apply  (rule Basic)
apply  clarsimp
apply (rule_tac R="{t. (result_exn (return s t) t) ∈ A}" in Catch)
apply  (rule_tac R="{i. i ∈ P' Z}" in Seq)
apply   (rule Basic)
apply   clarsimp
apply  simp
apply  (rule conseq [OF bdy])
apply  clarsimp
apply  blast
apply (rule SeqSwap)
apply  (rule Throw)
apply (rule Basic)
apply simp
  done

lemma BlockSpec:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes bdy: "∀Z. Γ,Θ⊨_F (P' Z) bdy (Q' Z),(A' Z)"
  shows "Γ,Θ⊨_F P (block init bdy return c) Q,A"
  unfolding block_def
  by (rule Block_exnSpec [OF adapt c bdy])


lemma Throw: "P ⊆ A ==> Γ,Θ⊨_F P Throw Q,A"
  by (rule hoarep.Throw [THEN conseqPre])

lemmas Catch = hoarep.Catch
lemma CatchSwap: "[Γ,Θ⊨_F R c₂ Q,A; Γ,Θ⊨_F P c₁ Q,R] ==> Γ,Θ⊨_F P Catch c₁ c₂ Q,A"
  by (rule hoarep.Catch)

lemma CatchSame: "[Γ,Θ⊨_F P c₁ Q,A; Γ,Θ⊨_F A c₂ Q,A] ==> Γ,Θ⊨_F P Catch c₁ c₂ Q,A"
  by (rule hoarep.Catch)

lemma raise: "P ⊆ {s. f s ∈ A} ==> Γ,Θ⊨_F P raise f Q,A"
  apply (simp add: raise_def)
  apply (rule Seq)
  apply  (rule Basic)
  apply  (assumption)
  apply (rule Throw)
  apply (rule subset_refl)
  done

lemma condCatch: "[Γ,Θ⊨_F P c₁ Q,((b ∩ R) ∪ (-b ∩ A));Γ,Θ⊨_F R c₂ Q,A]
                  ==> Γ,Θ⊨_FP condCatch c₁ b c₂ Q,A"
  apply (simp add: condCatch_def)
  apply (rule Catch)
  apply  assumption
  apply (rule CondSwap)
  apply   (assumption)
  apply  (rule hoarep.Throw)
  apply blast
  done

lemma condCatchSwap: "[Γ,Θ⊨_F R c₂ Q,A;Γ,Θ⊨_F P c₁ Q,((b ∩ R) ∪ (-b ∩ A))]
                  ==> Γ,Θ⊨_FP condCatch c₁ b c₂ Q,A"
  by (rule condCatch)

lemma condCatchSame:
  assumes c1: "Γ,Θ⊨_F P c₁ Q,A"
  assumes c2: "Γ,Θ⊨_F A c₂ Q,A"
  shows "Γ,Θ⊨_FP condCatch c₁ b c₂ Q,A"
proof -
  have eq: "((b ∩ A) ∪ (-b ∩ A)) = A" by blast
  show ?thesis
    apply (rule condCatch [OF _ c2])
    apply (simp add: eq)
    apply (rule c1)
    done
qed

lemma ProcSpec:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊨_F (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊨_F P (call init p return c) Q,A"
using adapt c p
apply (unfold call_def)
by (rule BlockSpec)

lemma Proc_exnSpec:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ result_exn (return s t) t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊨_F (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊨_F P (call_exn init p return result_exn c) Q,A"
using adapt c p
apply (unfold call_exn_def)
  by (rule Block_exnSpec)

lemma ProcSpec':
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t ∈ Q' Z. return s t ∈ R s t) ∧
                             (∀t ∈ A' Z. return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊨_F (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊨_F P (call init p return c) Q,A"
apply (rule ProcSpec [OF _ c p])
apply (insert adapt)
apply clarsimp
apply (drule (1) subsetD)
apply (clarsimp)
apply (rule_tac x=Z in exI)
apply blast
done

lemma Proc_exnSpecNoAbrupt:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊨_F (P' Z) Call p (Q' Z),{}"
  shows "Γ,Θ⊨_F P (call_exn init p return result_exn c) Q,A"
apply (rule Proc_exnSpec [OF _ c p])
using adapt
apply simp
  done

lemma ProcSpecNoAbrupt:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' Z ∧
                             (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊨_F (P' Z) Call p (Q' Z),{}"
  shows "Γ,Θ⊨_F P (call init p return c) Q,A"
apply (rule ProcSpec [OF _ c p])
using adapt
apply simp
done

lemma FCall:
"Γ,Θ⊨_F P (call init p return (λs t. c (result t))) Q,A
\<Longrightarrow> Γ,Θ⊨_F P (fcall init p return result c) Q,A"
  by (simp add: fcall_def)


lemma ProcRec:
  assumes deriv_bodies:
   "∀p∈Procs.
    ∀Z. Γ,Θ∪(∪p∈Procs. ∪Z. {(P p Z,p,Q p Z,A p Z)})
        ⊨_F (P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes Procs_defined: "Procs ⊆ dom Γ"
  shows "∀p∈Procs. ∀Z. Γ,Θ⊨_F(P p Z) Call p (Q p Z),(A p Z)"
  by (intro strip)
     (rule CallRec'
     [OF _   Procs_defined deriv_bodies],
     simp_all)

lemma ProcRec':
  assumes ctxt: "Θ' = Θ∪(∪p∈Procs. ∪Z. {(P p Z,p,Q p Z,A p Z)})"
  assumes deriv_bodies:
   "∀p∈Procs. ∀Z. Γ,Θ'⊨_F (P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes Procs_defined: "Procs ⊆ dom Γ"
  shows "∀p∈Procs. ∀Z. Γ,Θ⊨_F(P p Z) Call p (Q p Z),(A p Z)"
  using ctxt deriv_bodies
  apply simp
  apply (erule ProcRec [OF _ Procs_defined])
  done


lemma ProcRecList:
  assumes deriv_bodies:
   "∀p∈set Procs.
    ∀Z. Γ,Θ∪(∪p∈set Procs. ∪Z. {(P p Z,p,Q p Z,A p Z)})
        ⊨_F (P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes dist: "distinct Procs"
  assumes Procs_defined: "set Procs ⊆ dom Γ"
  shows "∀p∈set Procs. ∀Z. Γ,Θ⊨_F(P p Z) Call p (Q p Z),(A p Z)"
  using deriv_bodies Procs_defined
  by (rule ProcRec)

lemma  ProcRecSpecs:
  "[∀(P,p,Q,A) ∈ Specs. Γ,Θ∪Specs⊨_F P (the (Γ p)) Q,A;
    ∀(P,p,Q,A) ∈ Specs. p ∈ dom Γ]
  ==> ∀(P,p,Q,A) ∈ Specs. Γ,Θ⊨_F P (Call p) Q,A"
apply (auto intro: CallRec)
done


lemma ProcRec1:
  assumes deriv_body:
   "∀Z. Γ,Θ∪(∪Z. {(P Z,p,Q Z,A Z)})⊨_F (P Z) (the (Γ p)) (Q Z),(A Z)"
  assumes p_defined: "p ∈ dom Γ"
  shows "∀Z. Γ,Θ⊨_F (P Z) Call p (Q Z),(A Z)"
proof -
  from deriv_body p_defined
  have "∀p∈{p}. ∀Z. Γ,Θ⊨_F (P Z) Call p (Q Z),(A Z)"
    by - (rule ProcRec [where A="λp. A" and P="λp. P" and Q="λp. Q"],
          simp_all)
  thus ?thesis
    by simp
qed

lemma ProcNoRec1:
  assumes deriv_body:
   "∀Z. Γ,Θ⊨_F (P Z) (the (Γ p)) (Q Z),(A Z)"
  assumes p_def: "p ∈ dom Γ"
  shows "∀Z. Γ,Θ⊨_F (P Z) Call p (Q Z),(A Z)"
proof -
from deriv_body
  have "∀Z. Γ,Θ∪(∪Z. {(P Z,p,Q Z,A Z)})
             ⊨_F (P Z) (the (Γ p)) (Q Z),(A Z)"
    by (blast intro: hoare_augment_context)
  from this p_def
  show ?thesis
    by (rule ProcRec1)
qed

lemma ProcBody:
 assumes WP: "P ⊆ P'"
 assumes deriv_body: "Γ,Θ⊨_F P' body Q,A"
 assumes body: "Γ p = Some body"
 shows "Γ,Θ⊨_F P Call p Q,A"
apply (rule conseqPre [OF _ WP])
apply (rule ProcNoRec1 [rule_format, where P="λZ. P'" and Q="λZ. Q" and A="λZ. A"])
apply  (insert body)
apply  simp
apply  (rule hoare_augment_context [OF deriv_body])
apply  blast
apply fastforce
done

lemma CallBody:
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
assumes bdy: "∀s. Γ,Θ⊨_F (P' s) body {t. return s t ∈ R s t},{t. return s t ∈ A}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes body: "Γ p = Some body"
shows "Γ,Θ⊨_F P (call init p return c) Q,A"
apply (unfold call_def)
apply (rule Block [OF adapt _ c])
apply (rule allI)
apply (rule ProcBody [where Γ=Γ, OF _ bdy [rule_format] body])
apply simp
done

lemma Call_exnBody:
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
assumes bdy: "∀s. Γ,Θ⊨_F (P' s) body {t. return s t ∈ R s t},{t. result_exn (return s t) t ∈ A}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes body: "Γ p = Some body"
shows "Γ,Θ⊨_F P (call_exn init p return result_exn c) Q,A"
apply (unfold call_exn_def)
apply (rule Block_exn [OF adapt _ c])
apply (rule allI)
apply (rule ProcBody [where Γ=Γ, OF _ bdy [rule_format] body])
apply simp
done

lemmas ProcModifyReturn = HoarePartialProps.ProcModifyReturn
lemmas ProcModifyReturnSameFaults = HoarePartialProps.ProcModifyReturnSameFaults
lemmas Proc_exnModifyReturn = HoarePartialProps.Proc_exnModifyReturn
lemmas Proc_exnModifyReturnSameFaults = HoarePartialProps.Proc_exnModifyReturnSameFaults

lemma Proc_exnModifyReturnNoAbr:
  assumes spec: "Γ,Θ⊨_F P (call_exn init p return' result_exn c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊨_UNIV {σ} Call p (Modif σ),{}"
  shows "Γ,Θ⊨_F P (call_exn init p return result_exn c) Q,A"
  by (rule Proc_exnModifyReturn [OF spec result_conform _ modifies_spec]) simp

lemma ProcModifyReturnNoAbr:
  assumes spec: "Γ,Θ⊨_F P (call init p return' c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊨_UNIV {σ} Call p (Modif σ),{}"
  shows "Γ,Θ⊨_F P (call init p return c) Q,A"
by (rule ProcModifyReturn [OF spec result_conform _ modifies_spec]) simp

lemma Proc_exnModifyReturnNoAbrSameFaults:
  assumes spec: "Γ,Θ⊨_F P (call_exn init p return' result_exn c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊨_F {σ} Call p (Modif σ),{}"
  shows "Γ,Θ⊨_F P (call_exn init p return result_exn c) Q,A"
  by (rule Proc_exnModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp

lemma ProcModifyReturnNoAbrSameFaults:
  assumes spec: "Γ,Θ⊨_F P (call init p return' c) Q,A"
  assumes result_conform:
      "∀s t. t ∈ Modif (init s) ⟶ (return' s t) = (return s t)"
  assumes modifies_spec:
  "∀σ. Γ,Θ⊨_F {σ} Call p (Modif σ),{}"
  shows "Γ,Θ⊨_F P (call init p return c) Q,A"
by (rule ProcModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp

lemma DynProc_exn:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' s Z ∧
                          (∀t. t ∈ Q' s Z ⟶ return s t ∈ R s t) ∧
                          (∀t. t ∈ A' s Z ⟶ result_exn (return s t) t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊨_F (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊨_F P dynCall_exn f UNIV init p return result_exn c Q,A"
apply (rule conseq [where P'="λZ. {s. s=Z ∧ s ∈ P}"
  and Q'="λZ. Q" and A'="λZ. A"])
prefer 2
using adapt
apply  blast
apply (rule allI)
apply (unfold dynCall_exn_def call_exn_def maybe_guard_UNIV block_exn_def guards.simps)
apply (rule DynCom)
apply clarsimp
apply (rule DynCom)
apply clarsimp
apply (frule in_mono [rule_format, OF adapt])
apply clarsimp
apply (rename_tac Z')
apply (rule_tac R="Q' Z Z'" in Seq)
apply  (rule CatchSwap)
apply   (rule SeqSwap)
apply    (rule Throw)
apply    (rule subset_refl)
apply   (rule Basic)
apply   (rule subset_refl)
apply  (rule_tac R="{i. i ∈ P' Z Z'}" in Seq)
apply   (rule Basic)
apply   clarsimp
apply  simp
apply  (rule_tac Q'="Q' Z Z'" and A'="A' Z Z'" in conseqPost)
using p
apply    clarsimp
apply   simp
apply  clarsimp
apply  (rule_tac  P'="λZ''. {t. t=Z'' ∧ return Z t ∈ R Z t}" and
          Q'="λZ''. Q" and A'="λZ''. A" in conseq)
prefer 2 apply simp
apply (rule allI)
apply (rule DynCom)
apply clarsimp
apply (rule SeqSwap)
apply  (rule c [rule_format])
apply (rule Basic)
apply clarsimp
  done

lemma DynProc_exn_guards_cons:
  assumes p: "Γ,Θ⊨_F P dynCall_exn f UNIV init p return result_exn c Q,A"
  shows "Γ,Θ⊨_F (g ∩ P) dynCall_exn f g init p return result_exn c Q,A"
  using p apply (clarsimp simp add: dynCall_exn_def maybe_guard_def)
  apply (rule Guard)
   apply (rule subset_refl)
  apply assumption
  done

lemma DynProc:
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' s Z ∧
                          (∀t. t ∈ Q' s Z ⟶ return s t ∈ R s t) ∧
                          (∀t. t ∈ A' s Z ⟶ return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊨_F (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊨_F P dynCall init p return c Q,A"
  using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn)

lemma DynProc_exn':
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' s Z ∧
                          (∀t ∈ Q' s Z. return s t ∈ R s t) ∧
                          (∀t ∈ A' s Z. result_exn (return s t) t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊨_F (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊨_F P dynCall_exn f UNIV init p return result_exn c Q,A"
proof -
  from adapt have "P ⊆ {s. ∃Z. init s ∈ P' s Z ∧
                          (∀t. t ∈ Q' s Z ⟶ return s t ∈ R s t) ∧
                          (∀t. t ∈ A' s Z ⟶ result_exn (return s t) t ∈ A)}"
    by blast
  from this c p show ?thesis
    by (rule DynProc_exn)
qed

lemma DynProc':
  assumes adapt: "P ⊆ {s. ∃Z. init s ∈ P' s Z ∧
                          (∀t ∈ Q' s Z. return s t ∈ R s t) ∧
                          (∀t ∈ A' s Z. return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊨_F (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊨_F P dynCall init p return c Q,A"
  using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn')

lemma DynProc_exnStaticSpec:
assumes adapt: "P ⊆ {s. s ∈ S ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ) ∧
                            (∀τ. τ ∈ A' Z ⟶ result_exn (return s τ) τ ∈ A))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀s∈S. ∀Z. Γ,Θ⊨_F (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "Γ,Θ⊨_F P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
  from adapt have P_S: "P ⊆ S"
    by blast
  have "Γ,Θ⊨_F (P ∩ S) (dynCall_exn f UNIV init p return result_exn c) Q,A"
    apply (rule DynProc_exn [where P'="λs Z. P' Z" and Q'="λs Z. Q' Z"
                         and A'="λs Z. A' Z", OF _ c])
    apply  clarsimp
    apply  (frule in_mono [rule_format, OF adapt])
    apply  clarsimp
    using spec
    apply clarsimp
    done
  thus ?thesis
    by (rule conseqPre) (insert P_S,blast)
qed

lemma DynProcStaticSpec:
assumes adapt: "P ⊆ {s. s ∈ S ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ) ∧
                            (∀τ. τ ∈ A' Z ⟶ return s τ ∈ A))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀s∈S. ∀Z. Γ,Θ⊨_F (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnStaticSpec)

lemma DynProc_exnProcPar:
assumes adapt: "P ⊆ {s. p s = q ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ) ∧
                            (∀τ. τ ∈ A' Z ⟶ result_exn (return s τ) τ ∈ A))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊨_F (P' Z) Call q (Q' Z),(A' Z)"
shows "Γ,Θ⊨_F P (dynCall_exn f UNIV init p return result_exn c) Q,A"
  apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF adapt c])
  using spec
  apply simp
  done

lemma DynProcProcPar:
assumes adapt: "P ⊆ {s. p s = q ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ) ∧
                            (∀τ. τ ∈ A' Z ⟶ return s τ ∈ A))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊨_F (P' Z) Call q (Q' Z),(A' Z)"
shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  apply (rule DynProcStaticSpec [where S="{s. p s = q}",simplified, OF adapt c])
  using spec
  apply simp
  done

lemma DynProc_exnProcParNoAbrupt:
assumes adapt: "P ⊆ {s. p s = q ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊨_F (P' Z) Call q (Q' Z),{}"
shows "Γ,Θ⊨_F P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
  have "P ⊆ {s. p s = q ∧ (∃ Z. init s ∈ P' Z ∧
                      (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                      (∀t. t ∈ {} ⟶ result_exn (return s t) t ∈ A))}"
    (is "P ⊆ ?P'")
  proof
    fix s
    assume P: "s∈P"
    with adapt obtain Z where
      Pre: "p s = q ∧ init s ∈ P' Z" and
      adapt_Norm: "∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ"
      by blast
    from  adapt_Norm
    have "∀t. t ∈ Q' Z ⟶ return s t ∈ R s t"
      by auto
    then
    show "s∈?P'"
      using Pre by blast
  qed
  note P = this
  show ?thesis
    apply -
    apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF P c])
    apply (insert spec)
    apply auto
    done
qed

lemma DynProcProcParNoAbrupt:
assumes adapt: "P ⊆ {s. p s = q ∧ (∃Z. init s ∈ P' Z ∧
                            (∀τ. τ ∈ Q' Z ⟶ return s τ ∈ R s τ))}"
assumes c: "∀s t. Γ,Θ⊨_F (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊨_F (P' Z) Call q (Q' Z),{}"
shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnProcParNoAbrupt)

lemma DynProc_exnModifyReturnNoAbr:
  assumes to_prove: "Γ,Θ⊨_F P (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀s ∈ P. ∀σ. Γ,Θ⊨_UNIV {σ} Call (p s) (Modif σ),{}"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from ret_nrm_modif
  have "∀s t. t ∈ (Modif (init s))
        ⟶ return' s t = return s t"
    by iprover
  then
  have ret_nrm_modif': "∀s t. t ∈ (Modif (init s))
                      ⟶ return' s t = return s t"
    by simp
  have ret_abr_modif': "∀s t. t ∈ {}
                        ⟶ result_exn (return' s t) t = result_exn (return s t) t"
    by simp
  from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
    by (rule dynProc_exnModifyReturn)
qed

lemma DynProcModifyReturnNoAbr:
  assumes to_prove: "Γ,Θ⊨_F P (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀s ∈ P. ∀σ. Γ,Θ⊨_UNIV {σ} Call (p s) (Modif σ),{}"
          shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule DynProc_exnModifyReturnNoAbr)

lemma ProcDyn_exnModifyReturnNoAbrSameFaults:
  assumes to_prove: "Γ,Θ⊨_F P (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀s ∈ P. ∀σ. Γ,Θ⊨_F {σ} (Call (p s)) (Modif σ),{}"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from ret_nrm_modif
  have "∀s t. t ∈ (Modif (init s))
        ⟶ return' s t = return s t"
    by iprover
  then
  have ret_nrm_modif': "∀s t. t ∈ (Modif (init s))
                      ⟶ return' s t = return s t"
    by simp
  have ret_abr_modif': "∀s t. t ∈ {}
                        ⟶ result_exn (return' s t) t = result_exn (return s t) t"
    by simp
   from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
     by (rule dynProc_exnModifyReturnSameFaults)
qed

lemma ProcDynModifyReturnNoAbrSameFaults:
  assumes to_prove: "Γ,Θ⊨_F P (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀s ∈ P. ∀σ. Γ,Θ⊨_F {σ} (Call (p s)) (Modif σ),{}"
          shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule ProcDyn_exnModifyReturnNoAbrSameFaults)

lemma Proc_exnProcParModifyReturn:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
 @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes ret_abr_modif: "∀s t. t ∈ (ModifAbr (init s))
                            ⟶ result_exn (return' s t) t = result_exn (return s t) t"
  assumes modif_clause:
          "∀σ. Γ,Θ⊨_UNIV {σ} (Call q) (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return' result_exn c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif
       ret_abr_modif
  have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return result_exn c) Q,A"
    by (rule dynProc_exnModifyReturn) (insert modif_clause,auto)
  from this q show ?thesis
    by (rule conseqPre)
qed


lemma ProcProcParModifyReturn:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
 @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes ret_abr_modif: "∀s t. t ∈ (ModifAbr (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
          "∀σ. Γ,Θ⊨_UNIV {σ} (Call q) (Modif σ),(ModifAbr σ)"
        shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule Proc_exnProcParModifyReturn)

lemma Proc_exnProcParModifyReturnSameFaults:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
 @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes ret_abr_modif: "∀s t. t ∈ (ModifAbr (init s))
                            ⟶ result_exn (return' s t) t = result_exn (return s t) t"
  assumes modif_clause:
          "∀σ. Γ,Θ⊨_F {σ} Call q (Modif σ),(ModifAbr σ)"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove
  have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return' result_exn c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif
       ret_abr_modif
  have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return result_exn c) Q,A"
    by (rule dynProc_exnModifyReturnSameFaults) (insert modif_clause,auto)
  from this q show ?thesis
    by (rule conseqPre)
qed

lemma ProcProcParModifyReturnSameFaults:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
 @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes ret_abr_modif: "∀s t. t ∈ (ModifAbr (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
          "∀σ. Γ,Θ⊨_F {σ} Call q (Modif σ),(ModifAbr σ)"
        shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule Proc_exnProcParModifyReturnSameFaults)

lemma Proc_exnProcParModifyReturnNoAbr:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
 first conjunction in @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀σ. Γ,Θ⊨_UNIV {σ} (Call q) (Modif σ),{}"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return' result_exn c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif
  have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return result_exn c) Q,A"
    by (rule DynProc_exnModifyReturnNoAbr) (insert modif_clause,auto)
  from this q show ?thesis
    by (rule conseqPre)
qed

lemma ProcProcParModifyReturnNoAbr:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
 first conjunction in @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀σ. Γ,Θ⊨_UNIV {σ} (Call q) (Modif σ),{}"
          shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule Proc_exnProcParModifyReturnNoAbr)

lemma Proc_exnProcParModifyReturnNoAbrSameFaults:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
 first conjunction in @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall_exn f g init p return' result_exn c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀σ. Γ,Θ⊨_F {σ} (Call q) (Modif σ),{}"
  shows "Γ,Θ⊨_F P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have
    "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return' result_exn c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif
  have "Γ,Θ⊨_F ({s. p s = q} ∩ P') (dynCall_exn f g init p return result_exn c) Q,A"
    by (rule ProcDyn_exnModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
  from this q show ?thesis
    by (rule conseqPre)
qed

lemma ProcProcParModifyReturnNoAbrSameFaults:
  assumes q: "P ⊆ {s. p s = q} ∩ P'"
   ― ‹@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
 first conjunction in @{term P'}, so the vcg can simplify it.›
  assumes to_prove: "Γ,Θ⊨_F P' (dynCall init p return' c) Q,A"
  assumes ret_nrm_modif: "∀s t. t ∈ (Modif (init s))
                            ⟶ return' s t = return s t"
  assumes modif_clause:
            "∀σ. Γ,Θ⊨_F {σ} (Call q) (Modif σ),{}"
          shows "Γ,Θ⊨_F P (dynCall init p return c) Q,A"
  using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
  by (rule Proc_exnProcParModifyReturnNoAbrSameFaults)


lemma MergeGuards_iff: "Γ,Θ⊨_F P merge_guards c Q,A = Γ,Θ⊨_F P c Q,A"
  by (auto intro: MergeGuardsI MergeGuardsD)

lemma CombineStrip':
  assumes deriv: "Γ,Θ⊨_F P c' Q,A"
  assumes deriv_strip_triv: "Γ,{}⊨_{} P c'' UNIV,UNIV"
  assumes c'': "c''= mark_guards False (strip_guards (-F) c')"
  assumes c: "merge_guards c = merge_guards (mark_guards False c')"
  shows "Γ,Θ⊨_{} P c Q,A"
proof -
  from deriv_strip_triv have deriv_strip: "Γ,Θ⊨_{} P c'' UNIV,UNIV"
    by (auto intro: hoare_augment_context)
  from deriv_strip [simplified c'']
  have "Γ,Θ⊨_{} P (strip_guards (- F) c') UNIV,UNIV"
    by (rule MarkGuardsD)
  with deriv
  have "Γ,Θ⊨_{} P c' Q,A"
    by (rule CombineStrip)
  hence "Γ,Θ⊨_{} P mark_guards False c' Q,A"
    by (rule MarkGuardsI)
  hence "Γ,Θ⊨_{} P merge_guards (mark_guards False c') Q,A"
    by (rule MergeGuardsI)
  hence "Γ,Θ⊨_{} P merge_guards c Q,A"
    by (simp add: c)
  thus ?thesis
    by (rule MergeGuardsD)
qed

lemma CombineStrip'':
  assumes deriv: "Γ,Θ⊨_{True} P c' Q,A"
  assumes deriv_strip_triv: "Γ,{}⊨_{} P c'' UNIV,UNIV"
  assumes c'': "c''= mark_guards False (strip_guards ({False}) c')"
  assumes c: "merge_guards c = merge_guards (mark_guards False c')"
  shows "Γ,Θ⊨_{} P c Q,A"
  apply (rule CombineStrip' [OF deriv deriv_strip_triv _ c])
  apply (insert c'')
  apply (subgoal_tac "- {True} = {False}")
  apply auto
  done

lemma AsmUN:
  "(∪Z. {(P Z, p, Q Z,A Z)}) ⊆ Θ
  ==>
  ∀Z. Γ,Θ⊨_F (P Z) (Call p) (Q Z),(A Z)"
  by (blast intro: hoarep.Asm)

lemma augment_context':
  "[Θ ⊆ Θ'; ∀Z. Γ,Θ⊨_F (P Z) p (Q Z),(A Z)]
   ==> ∀Z. Γ,Θ'⊨_F (P Z) p (Q Z),(A Z)"
  by (iprover intro: hoare_augment_context)


lemma hoarep_strip:
 "[∀Z. Γ,{}⊨_F (P Z) p (Q Z),(A Z); F' ⊆ -F] ==>
    ∀Z. strip F' Γ,{}⊨_F (P Z) p (Q Z),(A Z)"
  by (iprover intro: hoare_strip_Γ)

lemma augment_emptyFaults:
 "[∀Z. Γ,{}⊨_{} (P Z) p (Q Z),(A Z)] ==>
    ∀Z. Γ,{}⊨_F (P Z) p (Q Z),(A Z)"
  by (blast intro: augment_Faults)

lemma augment_FaultsUNIV:
 "[∀Z. Γ,{}⊨_F (P Z) p (Q Z),(A Z)] ==>
    ∀Z. Γ,{}⊨_UNIV (P Z) p (Q Z),(A Z)"
  by (blast intro: augment_Faults)

lemma PostConjI [trans]:
  "[Γ,Θ⊨_F P c Q,A; Γ,Θ⊨_F P c R,B] ==> Γ,Θ⊨_F P c (Q ∩ R),(A ∩ B)"
  by (rule PostConjI)

lemma PostConjI' :
  "[Γ,Θ⊨_F P c Q,A; Γ,Θ⊨_F P c Q,A ==> Γ,Θ⊨_F P c R,B]
  ==> Γ,Θ⊨_F P c (Q ∩ R),(A ∩ B)"
  by (rule PostConjI) iprover+

lemma PostConjE [consumes 1]:
  assumes conj: "Γ,Θ⊨_F P c (Q ∩ R),(A ∩ B)"
  assumes E: "[Γ,Θ⊨_F P c Q,A; Γ,Θ⊨_F P c R,B] ==> S"
  shows "S"
proof -
  from conj have "Γ,Θ⊨_F P c Q,A" by (rule conseqPost) blast+
  moreover
  from conj have "Γ,Θ⊨_F P c R,B" by (rule conseqPost) blast+
  ultimately show "S"
    by (rule E)
qed


subsection ‹Rules for Single-Step Proof \label{sec:hoare-isar}›

text ‹
 We are now ready to introduce a set of Hoare rules to be used in
 single-step structured proofs in Isabelle/Isar.

 \medskip Assertions of Hoare Logic may be manipulated in
 calculational proofs, with the inclusion expressed in terms of sets
 or predicates. Reversed order is supported as well.
 ›

lemma annotateI [trans]:
"[Γ,Θ⊨_FP anno Q,A; c = anno] ==> Γ,Θ⊨_FP c Q,A"
  by simp

lemma annotate_normI:
  assumes deriv_anno: "Γ,Θ⊨_FP anno Q,A"
  assumes norm_eq: "normalize c = normalize anno"
  shows "Γ,Θ⊨_FP c Q,A"
proof -
  from NormalizeI [OF deriv_anno] norm_eq
  have "Γ,Θ⊨_F P normalize c Q,A"
    by simp
  from NormalizeD [OF this]
  show ?thesis .
qed

lemma annotateWhile:
"[Γ,Θ⊨_F P (whileAnnoG gs b I V c) Q,A] ==> Γ,Θ⊨_F P (while gs b c) Q,A"
  by (simp add: whileAnnoG_def)


lemma reannotateWhile:
"[Γ,Θ⊨_F P (whileAnnoG gs b I V c) Q,A] ==> Γ,Θ⊨_F P (whileAnnoG gs b J V c) Q,A"
  by (simp add: whileAnnoG_def)

lemma reannotateWhileNoGuard:
"[Γ,Θ⊨_F P (whileAnno b I V c) Q,A] ==> Γ,Θ⊨_F P (whileAnno b J V c) Q,A"
  by (simp add: whileAnno_def)

lemma [trans] : "P' ⊆ P ==> Γ,Θ⊨_F P c Q,A ==> Γ,Θ⊨_F P' c Q,A"
  by (rule conseqPre)

lemma [trans]: "Q ⊆ Q' ==> Γ,Θ⊨_F P c Q,A ==> Γ,Θ⊨_F P c Q',A"
  by (rule conseqPost) blast+

lemma [trans]:
    "Γ,Θ⊨_F {s. P s} c Q,A ==> (∧s. P' s ⟶ P s) ==> Γ,Θ⊨_F {s. P' s} c Q,A"
  by (rule conseqPre) auto

lemma [trans]:
    "(∧s. P' s ⟶ P s) ==> Γ,Θ⊨_F {s. P s} c Q,A ==> Γ,Θ⊨_F {s. P' s} c Q,A"
  by (rule conseqPre) auto

lemma [trans]:
    "Γ,Θ⊨_FP c {s. Q s},A ==> (∧s. Q s ⟶ Q' s) ==> Γ,Θ⊨_FP c {s. Q' s},A"
  by (rule conseqPost) auto

lemma [trans]:
    "(∧s. Q s ⟶ Q' s) ==> Γ,Θ⊨_FP c {s. Q s},A ==> Γ,Θ⊨_FP c {s. Q' s},A"
  by (rule conseqPost) auto

lemma [intro?]: "Γ,Θ⊨_F P Skip P,A"
  by (rule Skip) auto

lemma CondInt [trans,intro?]:
  "[Γ,Θ⊨_F (P ∩ b) c1 Q,A; Γ,Θ⊨_F (P ∩ - b) c2 Q,A]
   ==>
   Γ,Θ⊨_F P (Cond b c1 c2) Q,A"
  by (rule Cond) auto

lemma CondConj [trans, intro?]:
  "[Γ,Θ⊨_F {s. P s ∧ b s} c1 Q,A; Γ,Θ⊨_F {s. P s ∧ ¬ b s} c2 Q,A]
   ==>
   Γ,Θ⊨_F {s. P s} (Cond {s. b s} c1 c2) Q,A"
  by (rule Cond) auto

lemma WhileInvInt [intro?]:
    "Γ,Θ⊨_F (P ∩ b) c P,A ==> Γ,Θ⊨_F P (whileAnno b P V c) (P ∩ -b),A"
  by (rule While) auto

lemma WhileInt [intro?]:
    "Γ,Θ⊨_F (P ∩ b) c P,A
    ==>
    Γ,Θ⊨_F P (whileAnno b {s. undefined} V c) (P ∩ -b),A"
  by (unfold whileAnno_def)
     (rule HoarePartialDef.While [THEN conseqPrePost],auto)

lemma WhileInvConj [intro?]:
  "Γ,Θ⊨_F {s. P s ∧ b s} c {s. P s},A
  ==> Γ,Θ⊨_F {s. P s} (whileAnno {s. b s} {s. P s} V c) {s. P s ∧ ¬ b s},A"
  by (simp add: While Collect_conj_eq Collect_neg_eq)

lemma WhileConj [intro?]:
  "Γ,Θ⊨_F {s. P s ∧ b s} c {s. P s},A
    ==>
\<Gamma>,Θ⊨_F {s. P s} (whileAnno {s. b s} {s. undefined} V c) {s. P s ∧ ¬ b s},A"
  by (unfold whileAnno_def)
     (simp add: HoarePartialDef.While [THEN conseqPrePost]
      Collect_conj_eq Collect_neg_eq)

(* fixme: Add rules for guarded while *)

end