Theory HoareTotal

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

theory HoareTotal imports HoareTotalProps begin

lemma conseq_no_aux:
  "⟦Γ,Θ ⊢t⇘/F⇙ P' c Q',A';
    ∀s. s ∈ P ⟶ (s∈P' ∧ (Q' ⊆ Q)∧ (A' ⊆ A))⟧
  ⟹
  Γ,Θ⊢t⇘/F⇙ P c Q,A"
  by (rule conseq [where P'="λZ. P'" and Q'="λZ. Q'" and A'="λZ. A'"]) auto

text ‹If for example a specification for a "procedure pointer" parameter
is in the precondition we can extract it with this rule›
lemma conseq_exploit_pre:
             "⟦∀s ∈ P. Γ,Θ ⊢t⇘/F⇙ ({s} ∩ P) c Q,A⟧
              ⟹
              Γ,Θ⊢t⇘/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. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),(A' Z);
              ∀s. s ∈ P ⟶ (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q)∧ (A' Z ⊆ A))⟧
              ⟹
              Γ,Θ⊢t⇘/F⇙ P c Q,A"
  by (rule Conseq') blast


lemma Lem:"⟦∀Z. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),(A' Z);
            P ⊆ {s. ∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A)}⟧
              ⟹
              Γ,Θ⊢t⇘/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. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
shows "Γ,Θ⊢t⇘/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. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),{}"
shows "Γ,Θ⊢t⇘/F⇙ P (lem x c) Q,{}"
  apply (rule Lem [OF lem])
  using conseq
  by blast

lemma TrivPost: "∀Z. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),(A' Z)
                 ⟹
                 ∀Z. Γ,Θ ⊢t⇘/F⇙ (P' Z) c UNIV,UNIV"
apply (rule allI)
apply (erule conseq)
apply auto
done

lemma TrivPostNoAbr: "∀Z. Γ,Θ ⊢t⇘/F⇙ (P' Z) c (Q' Z),{}
                 ⟹
                 ∀Z. Γ,Θ ⊢t⇘/F⇙ (P' Z) c UNIV,{}"
apply (rule allI)
apply (erule conseq)
apply auto
done

lemma DynComConseq:
  assumes "P ⊆ {s. ∃P' Q' A'.  Γ,Θ⊢t⇘/F ⇙P' (c s) Q',A' ∧ P ⊆ P' ∧ Q' ⊆ Q ∧ A' ⊆ A}"
  shows "Γ,Θ⊢t⇘/F ⇙P DynCom c Q,A"
  using assms
  apply -
  apply (rule hoaret.DynCom)
  apply clarsimp
  apply (rule hoaret.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. Γ,Θ⊢t⇘/F⇙ (P' Z) (c Z) (Q' Z),(A' Z)"
 assumes bdy_constant:  "∀Z. c Z = c undefined"
 shows   "Γ,Θ⊢t⇘/F⇙ P (specAnno P' c Q' A') Q,A"
proof -
  from spec bdy_constant
  have "∀Z. Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (P' Z) (c Z) (Q' Z),(A' Z);
   ∀Z. c Z = c undefined
  ⟧ ⟹
    Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (P' Z) (c Z) (Q' Z),{};
   ∀Z. c Z = c undefined
  ⟧ ⟹
    Γ,Θ⊢t⇘/F⇙ P (specAnno P' c Q' (λs. {})) Q,A"
apply (rule SpecAnno')
apply auto
done

lemma Skip: "P ⊆ Q ⟹ Γ,Θ⊢t⇘/F⇙ P Skip Q,A"
  by (rule hoaret.Skip [THEN conseqPre],simp)

lemma Basic: "P ⊆ {s. (f s) ∈ Q} ⟹  Γ,Θ⊢t⇘/F⇙ P (Basic f) Q,A"
  by (rule hoaret.Basic [THEN conseqPre])

lemma BasicCond:
  "⟦P ⊆ {s. (b s ⟶ f s∈Q) ∧ (¬ b s ⟶ g s∈Q)}⟧ ⟹
   Γ,Θ⊢t⇘/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)}
            ⟹ Γ,Θ⊢t⇘/F⇙ P (Spec r) Q,A"
by (rule hoaret.Spec [THEN conseqPre])

lemma SpecIf:
  "⟦P ⊆ {s. (b s ⟶ f s ∈ Q) ∧ (¬ b s ⟶ g s ∈ Q ∧ h s ∈ Q)}⟧ ⟹
   Γ,Θ⊢t⇘/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?]:
  "⟦Γ,Θ⊢t⇘/F⇙ P c1 R,A; Γ,Θ⊢t⇘/F⇙ R c2 Q,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P Seq c1 c2 Q,A"
  by (rule hoaret.Seq)

lemma SeqSwap:
  "⟦Γ,Θ⊢t⇘/F⇙ R c2 Q,A; Γ,Θ⊢t⇘/F⇙ P c1 R,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P Seq c1 c2 Q,A"
  by (rule Seq)

lemma BSeq:
  "⟦Γ,Θ⊢t⇘/F⇙ P c1 R,A; Γ,Θ⊢t⇘/F⇙ R c2 Q,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P (bseq c1 c2) Q,A"
  by (unfold bseq_def) (rule Seq)

lemma Cond:
  assumes wp: "P ⊆ {s. (s∈b ⟶ s∈P1) ∧ (s∉b ⟶ s∈P2)}"
  assumes deriv_c1: "Γ,Θ⊢t⇘/F⇙ P1 c1 Q,A"
  assumes deriv_c2: "Γ,Θ⊢t⇘/F⇙ P2 c2 Q,A"
  shows "Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) Q,A"
proof (rule hoaret.Cond [THEN conseqPre])
  from deriv_c1
  show "Γ,Θ⊢t⇘/F⇙ ({s. (s ∈ b ⟶ s ∈ P1) ∧ (s ∉ b ⟶ s ∈ P2)} ∩ b) c1 Q,A"
    by (rule conseqPre) blast
next
  from deriv_c2
  show "Γ,Θ⊢t⇘/F⇙ ({s. (s ∈ b ⟶ s ∈ P1) ∧ (s ∉ b ⟶ s ∈ P2)} ∩ - b) c2 Q,A"
    by (rule conseqPre) blast
qed (insert wp)


lemma CondSwap:
  "⟦Γ,Θ⊢t⇘/F⇙ P1 c1 Q,A; Γ,Θ⊢t⇘/F⇙ P2 c2 Q,A;
    P ⊆ {s. (s∈b ⟶ s∈P1) ∧ (s∉b ⟶ s∈P2)}⟧
   ⟹
   Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) Q,A"
  by (rule Cond)

lemma Cond':
  "⟦P ⊆ {s. (b ⊆ P1) ∧ (- b ⊆ P2)};Γ,Θ⊢t⇘/F⇙ P1 c1 Q,A; Γ,Θ⊢t⇘/F⇙ P2 c2 Q,A⟧
   ⟹
   Γ,Θ⊢t⇘/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∈P1) ∧ (s∉b ⟶ s∈P2)}"
  assumes deriv_c1: "Γ,Θ⊢t⇘/F⇙ P1 c1 Q,A"
  assumes deriv_c2: "Γ,Θ⊢t⇘/F⇙ P2 c2 Q,A"
  shows "Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) Q,A"
proof -
  from wp inv
  have "P ⊆ {s. (s∈b ⟶ s∈P1) ∧ (s∉b ⟶ s∈P2)}"
    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∈P1) ∧ (s∉b ⟶ s∈P2)}"
  assumes wp': "I ⊆ Q"
  assumes deriv_c1: "Γ,Θ⊢t⇘/F⇙ P1 c1 I,A"
  assumes deriv_c2: "Γ,Θ⊢t⇘/F⇙ P2 c2 I,A"
  shows "Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) Q,A"
proof -
  from CondInv [OF wp inv deriv_c1 deriv_c2]
  have "Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) I,A" .
  from conseqPost [OF this wp' subset_refl]
  show ?thesis .
qed


lemma switchNil:
  "P ⊆ Q ⟹ Γ,Θ⊢t⇘/F ⇙P (switch v []) Q,A"
  by (simp add: Skip)

lemma switchCons:
  "⟦P ⊆ {s. (v s ∈ V ⟶ s ∈ P1) ∧ (v s ∉ V ⟶ s ∈ P2)};
        Γ,Θ⊢t⇘/F ⇙P1 c Q,A;
        Γ,Θ⊢t⇘/F ⇙P2 (switch v vs) Q,A⟧
⟹ Γ,Θ⊢t⇘/F ⇙P (switch v ((V,c)#vs)) Q,A"
  by (simp add: Cond)


lemma Guard:
 "⟦P ⊆ g ∩ R; Γ,Θ⊢t⇘/F⇙ R c Q,A⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P Guard f g c Q,A"
apply (rule HoareTotalDef.Guard [THEN conseqPre, of _ _ _ _ R])
apply (erule conseqPre)
apply auto
done

lemma GuardSwap:
 "⟦ Γ,Θ⊢t⇘/F⇙ R c Q,A; P ⊆ g ∩ R⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P Guard f g c Q,A"
  by (rule Guard)

lemma Guarantee:
 "⟦P ⊆ {s. s ∈ g ⟶ s ∈ R}; Γ,Θ⊢t⇘/F⇙ R c Q,A; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/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:
 "⟦ Γ,Θ⊢t⇘/F⇙ R c Q,A; P ⊆ {s. s ∈ g ⟶ s ∈ R}; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P (Guard f g c) Q,A"
  by (rule Guarantee)


lemma GuardStrip:
 "⟦P ⊆ R; Γ,Θ⊢t⇘/F⇙ R c Q,A; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P (Guard f g c) Q,A"
apply (rule Guarantee [THEN conseqPre])
apply auto
done

lemma GuardStripSwap:
 "⟦Γ,Θ⊢t⇘/F⇙ R c Q,A; P ⊆ R; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P (Guard f g c) Q,A"
  by (rule GuardStrip)

lemma GuaranteeStrip:
 "⟦P ⊆ R; Γ,Θ⊢t⇘/F⇙ R c Q,A; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P (guaranteeStrip f g c) Q,A"
  by (unfold guaranteeStrip_def) (rule GuardStrip)

lemma GuaranteeStripSwap:
 "⟦Γ,Θ⊢t⇘/F⇙ R c Q,A; P ⊆ R; f ∈ F⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P (guaranteeStrip f g c) Q,A"
  by (unfold guaranteeStrip_def) (rule GuardStrip)

lemma GuaranteeAsGuard:
 "⟦P ⊆ g ∩ R; Γ,Θ⊢t⇘/F⇙ R c Q,A⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P guaranteeStrip f g c Q,A"
  by (unfold guaranteeStrip_def) (rule Guard)

lemma GuaranteeAsGuardSwap:
 "⟦ Γ,Θ⊢t⇘/F⇙ R c Q,A; P ⊆ g ∩ R⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P guaranteeStrip f g c Q,A"
  by (rule GuaranteeAsGuard)

lemma GuardsNil:
  "Γ,Θ⊢t⇘/F⇙ P c Q,A ⟹
   Γ,Θ⊢t⇘/F⇙ P (guards [] c) Q,A"
  by simp

lemma GuardsCons:
  "Γ,Θ⊢t⇘/F⇙ P Guard f g (guards gs c) Q,A ⟹
   Γ,Θ⊢t⇘/F⇙ P (guards ((f,g)#gs) c) Q,A"
  by simp

lemma GuardsConsGuaranteeStrip:
  "Γ,Θ⊢t⇘/F⇙ P guaranteeStrip f g (guards gs c) Q,A ⟹
   Γ,Θ⊢t⇘/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:
  "∀σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ I),A"
  assumes I_Q: "I ∩ -b ⊆ Q"
  assumes wf: "wf V"
  shows "Γ,Θ⊢t⇘/F⇙ P (whileAnno  b I V c) Q,A"
proof -
  from wf deriv_body P_I I_Q
  show ?thesis
    apply (unfold whileAnno_def)
    apply (erule conseqPrePost [OF HoareTotalDef.While])
    apply auto
    done
qed



lemma WhileInvPost:
  assumes P_I: "P ⊆ I"
  assumes termi_body:
  "∀σ. Γ,Θ⊢t⇘/UNIV⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ P),A"
  assumes deriv_body:
  "Γ,Θ⊢⇘/F⇙ (I ∩ b) c I,A"
  assumes I_Q: "I ∩ -b ⊆ Q"
  assumes wf: "wf V"
  shows "Γ,Θ⊢t⇘/F⇙ P (whileAnno  b I V c) Q,A"
proof -
  have "∀σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ I),A"
  proof
    fix σ
    from hoare_sound [OF deriv_body] hoaret_sound [OF termi_body [rule_format, of σ]]
    have "Γ,Θ⊨t⇘/F⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ I),A"
      by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
    then
    show "Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ I),A"
      by (rule hoaret_complete')
  qed

  from While [OF P_I this I_Q wf]
  show ?thesis .
qed

(* *)
lemma "Γ,Θ⊢⇘/F⇙ (P ∩ b) c Q,A ⟹ Γ,Θ⊢⇘/F⇙ (P ∩ b) (Seq c (Guard f Q Skip)) Q,A"
oops

text ‹@{term "J"} will be instantiated by tactic with @{term "gs' ∩ I"} for
  those guards that are not stripped.›
lemma WhileAnnoG:
  "Γ,Θ⊢t⇘/F⇙ P (guards gs
                    (whileAnno  b J V (Seq c (guards gs Skip)))) Q,A
        ⟹
        Γ,Θ⊢t⇘/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: "∀σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I ∩ b) c ({t. (t, σ) ∈ V} ∩ I),A"
  assumes I_Q: "I ∩ -b ⊆ Q"
  assumes wf: "wf V"
  shows "Γ,Θ⊢t⇘/F⇙ P (whileAnno b I V (Seq c Skip)) Q,A"
  apply (rule While [OF P_I _ I_Q wf])
  apply (rule allI)
  apply (rule Seq)
  apply  (rule deriv_body [rule_format])
  apply (rule hoaret.Skip)
  done

lemma WhileAnnoFix:
assumes consequence: "P ⊆ {s. (∃ Z. s∈I Z ∧ (I Z ∩ -b ⊆ Q)) }"
assumes bdy: "∀Z σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I Z ∩ b) (c Z) ({t. (t, σ) ∈ V Z} ∩ I Z),A"
assumes bdy_constant:  "∀Z. c Z = c undefined"
assumes wf: "∀Z. wf (V Z)"
shows "Γ,Θ⊢t⇘/F⇙ P (whileAnnoFix b I V c) Q,A"
proof -
  from bdy bdy_constant
  have bdy': "⋀Z. ∀σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I Z ∩ b) (c undefined)
               ({t. (t, σ) ∈ V Z} ∩ I Z),A"
    apply -
    apply (erule_tac x=Z in allE)
    apply (erule_tac x=Z in allE)
    apply simp
    done
  have "∀Z. Γ,Θ⊢t⇘/F⇙ (I Z) (whileAnnoFix b I V c) (I Z ∩ -b),A"
    apply rule
    apply (unfold whileAnnoFix_def)
    apply (rule hoaret.While)
    apply (rule wf [rule_format])
    apply (rule bdy')
    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 σ. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ I Z ∩ b) (c Z) ({t. (t, σ) ∈ V Z} ∩ I Z),A"
assumes bdy_constant:  "∀Z. c Z = c undefined"
assumes wf: "∀Z. wf (V Z)"
shows "Γ,Θ⊢t⇘/F⇙ P (whileAnnoFix b I V c) Q,A"
  apply (rule WhileAnnoFix [OF _ bdy bdy_constant wf])
  using consequence by blast

lemma WhileAnnoGFix:
assumes whileAnnoFix:
  "Γ,Θ⊢t⇘/F⇙ P (guards gs
                (whileAnnoFix  b J V (λZ. (Seq (c Z) (guards gs Skip))))) Q,A"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (P' s) (c (e s)) Q,A"
  shows "Γ,Θ⊢t⇘/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 HoareTotalDef.DynCom)
apply  (rule ballI)
apply  clarsimp
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. Γ,Θ⊢t⇘/F⇙ (P' s) bdy {t. return s t ∈ R s t},{t. result_exn (return s t) t ∈ A}"
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
shows "Γ,Θ⊢t⇘/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 HoareTotalDef.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 HoareTotalDef.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 HoareTotalDef.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. Γ,Θ⊢t⇘/F⇙ (P' s) bdy {t. return s t ∈ R s t},{t. return s t ∈ A}"
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
shows "Γ,Θ⊢t⇘/F⇙ P (block init bdy return c) Q,A"
  using adapt bdy c unfolding block_def by (rule Block_exn)

lemma BlockSwap:
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes bdy: "∀s. Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (block init bdy return c) Q,A"
  using adapt bdy c
  by (rule Block)

lemma Block_exnSwap:
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes bdy: "∀s. Γ,Θ⊢t⇘/F⇙ (P' s) bdy {t. return s t ∈ R s t},{t. result_exn (return s t) t ∈ A}"
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
shows "Γ,Θ⊢t⇘/F⇙ P (block_exn init bdy return result_exn c) Q,A"
  using adapt bdy c
  by (rule Block_exn)

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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes bdy: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) bdy (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/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 HoareTotalDef.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 HoareTotalDef.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 HoareTotalDef.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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes bdy: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) bdy (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/F⇙ P (block init bdy return c) Q,A"
  using adapt c bdy unfolding block_def by (rule Block_exnSpec)


lemma Throw: "P ⊆ A ⟹ Γ,Θ⊢t⇘/F⇙ P Throw Q,A"
  by (rule hoaret.Throw [THEN conseqPre])

lemmas Catch = hoaret.Catch
lemma CatchSwap: "⟦Γ,Θ⊢t⇘/F⇙ R c2 Q,A; Γ,Θ⊢t⇘/F⇙ P c1 Q,R⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P Catch c1 c2 Q,A"
  by (rule hoaret.Catch)

lemma raise: "P ⊆ {s. f s ∈ A} ⟹ Γ,Θ⊢t⇘/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: "⟦Γ,Θ⊢t⇘/F⇙ P c1 Q,((b ∩ R) ∪ (-b ∩ A));Γ,Θ⊢t⇘/F⇙ R c2 Q,A⟧
                  ⟹  Γ,Θ⊢t⇘/F⇙ P condCatch c1 b c2 Q,A"
  apply (simp add: condCatch_def)
  apply (rule Catch)
  apply  assumption
  apply (rule CondSwap)
  apply   (assumption)
  apply  (rule hoaret.Throw)
  apply blast
  done

lemma condCatchSwap: "⟦Γ,Θ⊢t⇘/F⇙ R c2 Q,A; Γ,Θ⊢t⇘/F⇙ P c1 Q,((b ∩ R) ∪ (-b ∩ A))⟧
                     ⟹  Γ,Θ⊢t⇘/F⇙ P condCatch c1 b c2 Q,A"
  by (rule condCatch)

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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/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. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                             (∀t. t ∈ A' Z ⟶ return s t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/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 ∈ Q' Z. return s t ∈ R s t) ∧
                             (∀t ∈ A' Z. result_exn (return s t) t ∈ A)}"
  assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
apply (rule Proc_exnSpec [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 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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),(A' Z)"
  shows "Γ,Θ⊢t⇘/F⇙ P (call init p return c) Q,A"
  using adapt c p unfolding call_call_exn by (rule Proc_exnSpec')


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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),{}"
  shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call p (Q' Z),{}"
  shows "Γ,Θ⊢t⇘/F⇙ P (call init p return c) Q,A"
apply (rule ProcSpec [OF _ c p])
using adapt
apply simp
done

lemma FCall:
"Γ,Θ⊢t⇘/F⇙ P (call init p return (λs t. c (result t))) Q,A
⟹ Γ,Θ⊢t⇘/F⇙ P (fcall init p return result c) Q,A"
  by (simp add: fcall_def)

lemma ProcRec:
  assumes deriv_bodies:
   "∀p∈Procs.
    ∀σ Z. Γ,Θ∪(⋃q∈Procs. ⋃Z.
       {(P q Z ∩ {s. ((s,q), σ,p) ∈ r},q,Q q Z,A q Z)})
        ⊢t⇘/F⇙ ({σ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes wf: "wf r"
  assumes Procs_defined: "Procs ⊆ dom Γ"
  shows "∀p∈Procs. ∀Z.
  Γ,Θ⊢t⇘/F⇙(P p Z) Call p (Q p Z),(A p Z)"
  by (intro strip)
     (rule HoareTotalDef.CallRec'
     [OF _  Procs_defined wf deriv_bodies],
     simp_all)

lemma ProcRec':
  assumes ctxt:
   "Θ'=(λσ p. Θ∪(⋃q∈Procs.
                   ⋃Z. {(P q Z ∩ {s. ((s,q), σ,p) ∈ r},q,Q q Z,A q Z)}))"
  assumes deriv_bodies:
   "∀p∈Procs.
    ∀σ Z. Γ,Θ' σ p⊢t⇘/F⇙ ({σ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes wf: "wf r"
  assumes Procs_defined: "Procs ⊆ dom Γ"
  shows "∀p∈Procs. ∀Z.  Γ,Θ⊢t⇘/F⇙(P p Z) Call p (Q p Z),(A p Z)"
  using ctxt deriv_bodies
  apply simp
  apply (erule ProcRec [OF _ wf Procs_defined])
  done


lemma ProcRecList:
  assumes deriv_bodies:
   "∀p∈set Procs.
    ∀σ Z. Γ,Θ∪(⋃q∈set Procs. ⋃Z.
       {(P q Z ∩ {s. ((s,q), σ,p) ∈ r},q,Q q Z,A q Z)})
        ⊢t⇘/F⇙ ({σ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  assumes wf: "wf r"
  assumes dist: "distinct Procs"
  assumes Procs_defined: "set Procs ⊆ dom Γ"
  shows "∀p∈set Procs. ∀Z.
  Γ,Θ⊢t⇘/F⇙(P p Z) Call p (Q p Z),(A p Z)"
  using deriv_bodies wf Procs_defined
  by (rule ProcRec)

lemma  ProcRecSpecs:
  "⟦∀σ. ∀(P,p,Q,A) ∈ Specs.
     Γ,Θ∪ ((λ(P,q,Q,A). (P ∩ {s. ((s,q),(σ,p)) ∈ r},q,Q,A)) ` Specs)
      ⊢t⇘/F⇙ ({σ} ∩ P) (the (Γ p)) Q,A;
    wf r;
    ∀(P,p,Q,A) ∈ Specs. p ∈ dom Γ⟧
  ⟹ ∀(P,p,Q,A) ∈ Specs. Γ,Θ⊢t⇘/F⇙ P (Call p) Q,A"
apply (rule ballI)
apply (case_tac x)
apply (rename_tac x P p Q A)
apply simp
apply (rule hoaret.CallRec)
apply auto
done

lemma ProcRec1:
  assumes deriv_body:
   "∀σ Z. Γ,Θ∪(⋃Z. {(P Z ∩ {s. ((s,p), σ,p) ∈ r},p,Q Z,A Z)})
           ⊢t⇘/F⇙ ({σ} ∩ P Z) (the (Γ p)) (Q Z),(A Z)"
  assumes wf: "wf r"
  assumes p_defined: "p ∈ dom Γ"
  shows "∀Z. Γ,Θ⊢t⇘/F⇙ (P Z) Call p (Q Z),(A Z)"
proof -
  from deriv_body wf p_defined
  have "∀p∈{p}. ∀Z. Γ,Θ⊢t⇘/F⇙ (P Z) Call p (Q Z),(A Z)"
    apply -
    apply (rule ProcRec [where  A="λp. A" and P="λp. P" and Q="λp. Q"])
    apply simp_all
    done
  thus ?thesis
    by simp
qed

lemma ProcNoRec1:
  assumes deriv_body:
   "∀Z. Γ,Θ⊢t⇘/F⇙ (P Z) (the (Γ p)) (Q Z),(A Z)"
  assumes p_defined: "p ∈ dom Γ"
  shows "∀Z. Γ,Θ⊢t⇘/F⇙ (P Z) Call p (Q Z),(A Z)"
proof -
  have "∀σ Z. Γ,Θ⊢t⇘/F⇙ ({σ} ∩ P Z) (the (Γ p)) (Q Z),(A Z)"
    by (blast intro: conseqPre deriv_body [rule_format])
  with p_defined have "∀σ Z. Γ,Θ∪(⋃Z. {(P Z ∩ {s. ((s,p), σ,p) ∈ {}},
                         p,Q Z,A Z)})
             ⊢t⇘/F⇙ ({σ} ∩ P Z) (the (Γ p)) (Q Z),(A Z)"
    by (blast intro: hoaret_augment_context)
  from this
  show ?thesis
    by (rule ProcRec1) (auto simp add: p_defined)
qed

lemma ProcBody:
 assumes WP: "P ⊆ P'"
 assumes deriv_body: "Γ,Θ⊢t⇘/F⇙ P' body Q,A"
 assumes body: "Γ p = Some body"
 shows "Γ,Θ⊢t⇘/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 hoaret_augment_context [OF deriv_body])
apply  blast
apply fastforce
done

lemma CallBody:
assumes adapt: "P ⊆ {s. init s ∈ P' s}"
assumes bdy: "∀s. Γ,Θ⊢t⇘/F⇙ (P' s) body {t. return s t ∈ R s t},{t. return s t ∈ A}"
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes body: "Γ p = Some body"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (P' s) body {t. return s t ∈ R s t},{t. result_exn (return s t) t ∈ A}"
assumes c: "∀s t. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes body: "Γ p = Some body"
shows "Γ,Θ⊢t⇘/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 = HoareTotalProps.ProcModifyReturn
lemmas ProcModifyReturnSameFaults = HoareTotalProps.ProcModifyReturnSameFaults

lemmas Proc_exnModifyReturn = HoareTotalProps.Proc_exnModifyReturn
lemmas Proc_exnModifyReturnSameFaults = HoareTotalProps.Proc_exnModifyReturnSameFaults

lemma ProcModifyReturnNoAbr:
  assumes spec: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (call init p return c) Q,A"
by (rule ProcModifyReturn [OF spec result_conform _ modifies_spec]) simp

lemma Proc_exnModifyReturnNoAbr:
  assumes spec: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
  by (rule Proc_exnModifyReturn [OF spec result_conform _ modifies_spec]) simp


lemma ProcModifyReturnNoAbrSameFaults:
  assumes spec: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (call init p return c) Q,A"
by (rule ProcModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp

lemma Proc_exnModifyReturnNoAbrSameFaults:
  assumes spec: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (call_exn init p return result_exn c) Q,A"
  by (rule Proc_exnModifyReturnSameFaults [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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊢t⇘/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 maybe_guard_UNIV call_exn_def block_exn_def guards.simps)
apply (rule HoareTotalDef.DynCom)
apply clarsimp
apply (rule HoareTotalDef.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 HoareTotalDef.DynCom)
apply clarsimp
apply (rule SeqSwap)
apply  (rule c [rule_format])
apply (rule Basic)
apply clarsimp
  done

lemma DynProc_exn_guards_cons:
  assumes p: "Γ,Θ⊢t⇘/F⇙ P dynCall_exn f UNIV init p return result_exn c Q,A"
  shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
  assumes p: "∀s∈ P. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
  shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀s∈S. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀s∈S. ∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call q (Q' Z),(A' Z)"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call q (Q' Z),(A' Z)"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call q (Q' Z),{}"
shows "Γ,Θ⊢t⇘/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. Γ,Θ⊢t⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊢t⇘/F⇙ (P' Z) Call q (Q' Z),{}"
shows "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove
  have "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/F⇙ P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
  from to_prove have
    "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/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: "Γ,Θ⊢t⇘/F⇙ P merge_guards c Q,A = Γ,Θ⊢t⇘/F⇙ P c Q,A"
  by (auto intro: MergeGuardsI MergeGuardsD)

lemma CombineStrip':
  assumes deriv: "Γ,Θ⊢t⇘/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 "Γ,Θ⊢t⇘/{}⇙ 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 HoarePartialProps.MarkGuardsD)
  with deriv
  have "Γ,Θ⊢t⇘/{}⇙ P c' Q,A"
    by (rule CombineStrip)
  hence "Γ,Θ⊢t⇘/{}⇙ P mark_guards False c' Q,A"
    by (rule MarkGuardsI)
  hence "Γ,Θ⊢t⇘/{}⇙ P merge_guards (mark_guards False c') Q,A"
    by (rule MergeGuardsI)
  hence "Γ,Θ⊢t⇘/{}⇙ P merge_guards c Q,A"
    by (simp add: c)
  thus ?thesis
    by (rule MergeGuardsD)
qed

lemma CombineStrip'':
  assumes deriv: "Γ,Θ⊢t⇘/{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 "Γ,Θ⊢t⇘/{}⇙ 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. Γ,Θ⊢t⇘/F⇙ (P Z) (Call p) (Q Z),(A Z)"
  by (blast intro: hoaret.Asm)


lemma hoaret_to_hoarep':
  "∀Z. Γ,{}⊢t⇘/F⇙ (P Z) p (Q Z),(A Z) ⟹ ∀Z. Γ,{}⊢⇘/F⇙ (P Z) p (Q Z),(A Z)"
  by (iprover intro: total_to_partial)

lemma augment_context':
  "⟦Θ ⊆ Θ'; ∀Z. Γ,Θ⊢t⇘/F⇙ (P Z)  p (Q Z),(A Z)⟧
   ⟹ ∀Z. Γ,Θ'⊢t⇘/F⇙ (P Z) p (Q Z),(A Z)"
  by (iprover intro: hoaret_augment_context)


lemma augment_emptyFaults:
 "⟦∀Z. Γ,{}⊢t⇘/{}⇙ (P Z) p (Q Z),(A Z)⟧ ⟹
    ∀Z. Γ,{}⊢t⇘/F⇙ (P Z) p (Q Z),(A Z)"
  by (blast intro: augment_Faults)

lemma augment_FaultsUNIV:
 "⟦∀Z. Γ,{}⊢t⇘/F⇙ (P Z) p (Q Z),(A Z)⟧ ⟹
    ∀Z. Γ,{}⊢t⇘/UNIV⇙ (P Z) p (Q Z),(A Z)"
  by (blast intro: augment_Faults)

lemma PostConjI [trans]:
  "⟦Γ,Θ⊢t⇘/F⇙ P c Q,A; Γ,Θ⊢t⇘/F⇙ P c R,B⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
  by (rule PostConjI)

lemma PostConjI' :
  "⟦Γ,Θ⊢t⇘/F⇙ P c Q,A; Γ,Θ⊢t⇘/F⇙ P c Q,A ⟹ Γ,Θ⊢t⇘/F⇙ P c R,B⟧
  ⟹ Γ,Θ⊢t⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
  by (rule PostConjI) iprover+

lemma PostConjE [consumes 1]:
  assumes conj: "Γ,Θ⊢t⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
  assumes E: "⟦Γ,Θ⊢t⇘/F⇙ P c Q,A; Γ,Θ⊢t⇘/F⇙ P c R,B⟧ ⟹ S"
  shows "S"
proof -
  from conj have "Γ,Θ⊢t⇘/F⇙ P c Q,A" by (rule conseqPost) blast+
  moreover
  from conj have "Γ,Θ⊢t⇘/F⇙ P c R,B" by (rule conseqPost) blast+
  ultimately show "S"
    by (rule E)
qed

subsubsection ‹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]:
"⟦Γ,Θ⊢t⇘/F⇙ P anno Q,A; c = anno⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P c Q,A"
  by (simp)

lemma annotate_normI:
  assumes deriv_anno: "Γ,Θ⊢t⇘/F⇙P anno Q,A"
  assumes norm_eq: "normalize c = normalize anno"
  shows "Γ,Θ⊢t⇘/F⇙P c Q,A"
proof -
  from HoareTotalProps.NormalizeI [OF deriv_anno] norm_eq
  have "Γ,Θ⊢t⇘/F ⇙P normalize c Q,A"
    by simp
  from NormalizeD [OF this]
  show ?thesis .
qed


lemma annotateWhile:
"⟦Γ,Θ⊢t⇘/F⇙ P (whileAnnoG gs b I V c) Q,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P (while gs b c) Q,A"
  by (simp add: whileAnnoG_def)


lemma reannotateWhile:
"⟦Γ,Θ⊢t⇘/F⇙ P (whileAnnoG gs b I V c) Q,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P (whileAnnoG gs b J V c) Q,A"
  by (simp add: whileAnnoG_def)

lemma reannotateWhileNoGuard:
"⟦Γ,Θ⊢t⇘/F⇙ P (whileAnno b I V c) Q,A⟧ ⟹ Γ,Θ⊢t⇘/F⇙ P (whileAnno b J V c) Q,A"
  by (simp add: whileAnno_def)

lemma [trans] : "P' ⊆ P ⟹ Γ,Θ⊢t⇘/F⇙ P c Q,A ⟹ Γ,Θ⊢t⇘/F⇙ P' c Q,A"
  by (rule conseqPre)

lemma [trans]: "Q ⊆ Q' ⟹ Γ,Θ⊢t⇘/F⇙ P c Q,A ⟹ Γ,Θ⊢t⇘/F⇙ P c Q',A"
  by (rule conseqPost) blast+

lemma [trans]:
    "Γ,Θ⊢t⇘/F⇙ {s. P s} c Q,A ⟹ (⋀s. P' s ⟶ P s) ⟹ Γ,Θ⊢t⇘/F⇙ {s. P' s} c Q,A"
  by (rule conseqPre) auto

lemma [trans]:
    "(⋀s. P' s ⟶ P s) ⟹ Γ,Θ⊢t⇘/F⇙ {s. P s} c Q,A ⟹ Γ,Θ⊢t⇘/F⇙ {s. P' s} c Q,A"
  by (rule conseqPre) auto

lemma [trans]:
    "Γ,Θ⊢t⇘/F⇙ P c {s. Q s},A ⟹ (⋀s. Q s ⟶ Q' s) ⟹ Γ,Θ⊢t⇘/F⇙ P c {s. Q' s},A"
  by (rule conseqPost) auto

lemma [trans]:
    "(⋀s. Q s ⟶ Q' s) ⟹ Γ,Θ⊢t⇘/F⇙ P c {s. Q s},A ⟹ Γ,Θ⊢t⇘/F⇙ P c {s. Q' s},A"
  by (rule conseqPost) auto

lemma [intro?]: "Γ,Θ⊢t⇘/F⇙ P Skip P,A"
  by (rule Skip) auto

lemma CondInt [trans,intro?]:
  "⟦Γ,Θ⊢t⇘/F⇙ (P ∩ b) c1 Q,A; Γ,Θ⊢t⇘/F⇙ (P ∩ - b) c2 Q,A⟧
   ⟹
   Γ,Θ⊢t⇘/F⇙ P (Cond b c1 c2) Q,A"
  by (rule Cond) auto

lemma CondConj [trans, intro?]:
  "⟦Γ,Θ⊢t⇘/F⇙ {s. P s ∧ b s} c1 Q,A; Γ,Θ⊢t⇘/F⇙ {s. P s ∧ ¬ b s} c2 Q,A⟧
   ⟹
   Γ,Θ⊢t⇘/F⇙ {s. P s} (Cond {s. b s} c1 c2) Q,A"
  by (rule Cond) auto
end