Theory HoarePartial
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⟧
⟹ Γ,Θ⊢⇘/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⇩1 R,A; Γ,Θ⊢⇘/F⇙ R c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇘/F⇙ P (Seq c⇩1 c⇩2) Q,A"
by (rule hoarep.Seq)
lemma SeqSame:
"⟦Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A; Γ,Θ⊢⇘/F⇙ Q c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇘/F⇙ P (Seq c⇩1 c⇩2) 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⇩1 R,A; Γ,Θ⊢⇘/F⇙ R c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇘/F⇙ P (bseq c⇩1 c⇩2) Q,A"
by (unfold bseq_def) (rule Seq)
lemma BSeqSame:
"⟦Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A; Γ,Θ⊢⇘/F⇙ Q c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇘/F⇙ P (bseq c⇩1 c⇩2) Q,A"
by (rule BSeq)
lemma Cond:
assumes wp: "P ⊆ {s. (s∈b ⟶ s∈P⇩1) ∧ (s∉b ⟶ s∈P⇩2)}"
assumes deriv_c1: "Γ,Θ⊢⇘/F⇙ P⇩1 c⇩1 Q,A"
assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P⇩2 c⇩2 Q,A"
shows "Γ,Θ⊢⇘/F⇙ P (Cond b c⇩1 c⇩2) Q,A"
proof (rule hoarep.Cond [THEN conseqPre])
from deriv_c1
show "Γ,Θ⊢⇘/F⇙ ({s. (s ∈ b ⟶ s ∈ P⇩1) ∧ (s ∉ b ⟶ s ∈ P⇩2)} ∩ b) c⇩1 Q,A"
by (rule conseqPre) blast
next
from deriv_c2
show "Γ,Θ⊢⇘/F⇙ ({s. (s ∈ b ⟶ s ∈ P⇩1) ∧ (s ∉ b ⟶ s ∈ P⇩2)} ∩ - b) c⇩2 Q,A"
by (rule conseqPre) blast
next
show "P ⊆ {s. (s∈b ⟶ s∈P⇩1) ∧ (s∉b ⟶ s∈P⇩2)}" 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⇩1) ∧ (s∉b ⟶ s∈P⇩2)}"
assumes deriv_c1: "Γ,Θ⊢⇘/F⇙ P⇩1 c⇩1 Q,A"
assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P⇩2 c⇩2 Q,A"
shows "Γ,Θ⊢⇘/F⇙ P (Cond b c⇩1 c⇩2) Q,A"
proof -
from wp inv
have "P ⊆ {s. (s∈b ⟶ s∈P⇩1) ∧ (s∉b ⟶ s∈P⇩2)}"
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⇩1) ∧ (s∉b ⟶ s∈P⇩2)}"
assumes wp': "I ⊆ Q"
assumes deriv_c1: "Γ,Θ⊢⇘/F⇙ P⇩1 c⇩1 I,A"
assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P⇩2 c⇩2 I,A"
shows "Γ,Θ⊢⇘/F⇙ P (Cond b c⇩1 c⇩2) Q,A"
proof -
from CondInv [OF wp inv deriv_c1 deriv_c2]
have "Γ,Θ⊢⇘/F⇙ P (Cond b c⇩1 c⇩2) 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⇩1) ∧ (v s ∉ V ⟶ s ∈ P⇩2)};
Γ,Θ⊢⇘/F ⇙P⇩1 c Q,A;
Γ,Θ⊢⇘/F ⇙P⇩2 (switch v vs) Q,A⟧
⟹ Γ,Θ⊢⇘/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⇩2 Q,A; Γ,Θ⊢⇘/F⇙ P c⇩1 Q,R⟧ ⟹ Γ,Θ⊢⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"
by (rule hoarep.Catch)
lemma CatchSame: "⟦Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A; Γ,Θ⊢⇘/F⇙ A c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇘/F⇙ P Catch c⇩1 c⇩2 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⇩1 Q,((b ∩ R) ∪ (-b ∩ A));Γ,Θ⊢⇘/F⇙ R c⇩2 Q,A⟧
⟹ Γ,Θ⊢⇘/F⇙P condCatch c⇩1 b c⇩2 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⇩2 Q,A;Γ,Θ⊢⇘/F⇙ P c⇩1 Q,((b ∩ R) ∪ (-b ∩ A))⟧
⟹ Γ,Θ⊢⇘/F⇙P condCatch c⇩1 b c⇩2 Q,A"
by (rule condCatch)
lemma condCatchSame:
assumes c1: "Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A"
assumes c2: "Γ,Θ⊢⇘/F⇙ A c⇩2 Q,A"
shows "Γ,Θ⊢⇘/F⇙P condCatch c⇩1 b c⇩2 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
⟹ Γ,Θ⊢⇘/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'"
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'"
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'"
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'"
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'"
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'"
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'"
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'"
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]:
"⟦Γ,Θ⊢⇘/F⇙P anno Q,A; c = anno⟧ ⟹ Γ,Θ⊢⇘/F⇙P c Q,A"
by simp
lemma annotate_normI:
assumes deriv_anno: "Γ,Θ⊢⇘/F⇙P anno Q,A"
assumes norm_eq: "normalize c = normalize anno"
shows "Γ,Θ⊢⇘/F⇙P 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]:
"Γ,Θ⊢⇘/F⇙P c {s. Q s},A ⟹ (⋀s. Q s ⟶ Q' s) ⟹ Γ,Θ⊢⇘/F⇙P c {s. Q' s},A"
by (rule conseqPost) auto
lemma [trans]:
"(⋀s. Q s ⟶ Q' s) ⟹ Γ,Θ⊢⇘/F⇙P c {s. Q s},A ⟹ Γ,Θ⊢⇘/F⇙P 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
⟹
Γ,Θ⊢⇘/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)
end