Theory HoareTotal

theory HoareTotal
imports HoareTotalProps
(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
    License:     LGPL
*)

(*  Title:      HoareTotal.thy
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2008 Norbert Schirmer 
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

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:
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" 
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_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. return Z 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 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 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" 
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 ⟶ return s t ∈ A)}" and Q'="λZ. Q" and 
A'="λZ. A"])
prefer 2
using adapt
apply  blast
apply (rule allI)
apply (unfold block_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. return s 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 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 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 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"
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 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

lemmas ProcModifyReturn = HoareTotalProps.ProcModifyReturn
lemmas ProcModifyReturnSameFaults = HoareTotalProps.ProcModifyReturnSameFaults

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 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 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"
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_def call_def block_def)
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': 
  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"
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 ⟶ return s t ∈ A)}"
    by blast
  from this c p show ?thesis
    by (rule DynProc)
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"
proof -
  from adapt have P_S: "P ⊆ S"
    by blast
  have "Γ,Θ⊢t/F (P ∩ S) (dynCall init p return c) Q,A"
    apply (rule DynProc [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 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 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"
proof -  
  have "P ⊆ {s. p s = q ∧ (∃ Z. init s ∈ P' Z ∧ 
                      (∀t. t ∈ Q' Z ⟶ return s t ∈ R s t) ∧
                      (∀t. t ∈ {} ⟶ return s 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 DynProcStaticSpec [where S="{s. p s = q}",simplified, OF P c])
    apply (insert spec)
    apply auto
    done
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"
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 ∈ {} 
                        ⟶ return' s t = return s t"
    by simp
  from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
    by (rule dynProcModifyReturn)
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"
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 ∈ {} 
                        ⟶ return' s t = return s t"
    by simp
  from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
    by (rule dynProcModifyReturnSameFaults)
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"
proof -
  from to_prove have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return' c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif 
       ret_abr_modif 
  have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return c) Q,A"
    by (rule dynProcModifyReturn) (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"
proof -
  from to_prove 
  have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return' c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif 
       ret_abr_modif 
  have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return c) Q,A"
    by (rule dynProcModifyReturnSameFaults) (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"
proof -
  from to_prove have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return' c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif 
  have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return c) Q,A"
    by (rule DynProcModifyReturnNoAbr) (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"
proof -
  from to_prove have 
    "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return' c) Q,A"
    by (rule conseqPre) blast
  from this ret_nrm_modif 
  have "Γ,Θ⊢t/F ({s. p s = q} ∩ P') (dynCall init p return c) Q,A"
    by (rule ProcDynModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
  from this q show ?thesis
    by (rule conseqPre) 
qed

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/FP anno Q,A" 
  assumes norm_eq: "normalize c = normalize anno" 
  shows "Γ,Θ⊢t/FP 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