section {* Properties of Partial Correctness Hoare Logic *}
theory HoarePartialProps imports HoarePartialDef begin
subsection {* Soundness *}
lemma hoare_cnvalid:
assumes hoare: "Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "⋀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
using hoare
proof (induct)
case (Skip Θ F P A)
show "Γ,Θ ⊨n:⇘/F⇙ P Skip P,A"
proof (rule cnvalidI)
fix s t
assume "Γ⊢⟨Skip,Normal s⟩ =n⇒ t" "s ∈ P"
thus "t ∈ Normal ` P ∪ Abrupt ` A"
by cases auto
qed
next
case (Basic Θ F f P A)
show "Γ,Θ ⊨n:⇘/F⇙ {s. f s ∈ P} (Basic f) P,A"
proof (rule cnvalidI)
fix s t
assume "Γ⊢⟨Basic f,Normal s⟩ =n⇒ t" "s ∈ {s. f s ∈ P}"
thus "t ∈ Normal ` P ∪ Abrupt ` A"
by cases auto
qed
next
case (Spec Θ F r Q A)
show "Γ,Θ⊨n:⇘/F⇙ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A"
proof (rule cnvalidI)
fix s t
assume exec: "Γ⊢⟨Spec r,Normal s⟩ =n⇒ t"
assume P: "s ∈ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)}"
from exec P
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by cases auto
qed
next
case (Seq Θ F P c1 R A c2 Q)
have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P c1 R,A" by fact
have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ R c2 Q,A" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P Seq c1 c2 Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Seq c1 c2,Normal s⟩ =n⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P: "s ∈ P"
from exec P obtain r where
exec_c1: "Γ⊢⟨c1,Normal s⟩ =n⇒ r" and exec_c2: "Γ⊢⟨c2,r⟩ =n⇒ t"
by cases auto
with t_notin_F have "r ∉ Fault ` F"
by (auto dest: execn_Fault_end)
with valid_c1 ctxt exec_c1 P
have r: "r∈Normal ` R ∪ Abrupt ` A"
by (rule cnvalidD)
show "t∈Normal ` Q ∪ Abrupt ` A"
proof (cases r)
case (Normal r')
with exec_c2 r
show "t∈Normal ` Q ∪ Abrupt ` A"
apply -
apply (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F])
apply auto
done
next
case (Abrupt r')
with exec_c2 have "t=Abrupt r'"
by (auto elim: execn_elim_cases)
with Abrupt r show ?thesis
by auto
next
case Fault with r show ?thesis by blast
next
case Stuck with r show ?thesis by blast
qed
qed
next
case (Cond Θ F P b c1 Q A c2)
have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ b) c1 Q,A" by fact
have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ - b) c2 Q,A" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P Cond b c1 c2 Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Cond b c1 c2,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases "s∈b")
case True
with exec have "Γ⊢⟨c1,Normal s⟩ =n⇒ t"
by cases auto
with P True
show ?thesis
by - (rule cnvalidD [OF valid_c1 ctxt _ _ t_notin_F],auto)
next
case False
with exec P have "Γ⊢⟨c2,Normal s⟩ =n⇒ t"
by cases auto
with P False
show ?thesis
by - (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F],auto)
qed
qed
next
case (While Θ F P b c A n)
have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (P ∩ b) c P,A" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P While b c (P ∩ - b),A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨While b c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
proof (cases "s ∈ b")
case True
{
fix d::"('b,'a,'c) com" fix s t
assume exec: "Γ⊢⟨d,s⟩ =n⇒ t"
assume d: "d=While b c"
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
from exec d ctxt
have "⟦s ∈ Normal ` P; t ∉ Fault ` F⟧
⟹ t ∈ Normal ` (P ∩ - b) ∪ Abrupt`A"
proof (induct)
case (WhileTrue s b' c' n r t)
have t_notin_F: "t ∉ Fault ` F" by fact
have eqs: "While b' c' = While b c" by fact
note valid_c
moreover have ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A" by fact
moreover from WhileTrue
obtain "Γ⊢⟨c,Normal s⟩ =n⇒ r" and
"Γ⊢⟨While b c,r⟩ =n⇒ t" and
"Normal s ∈ Normal `(P ∩ b)" by auto
moreover with t_notin_F have "r ∉ Fault ` F"
by (auto dest: execn_Fault_end)
ultimately
have r: "r ∈ Normal ` P ∪ Abrupt ` A"
by - (rule cnvalidD,auto)
from this _ ctxt
show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A "
proof (cases r)
case (Normal r')
with r ctxt eqs t_notin_F
show ?thesis
by - (rule WhileTrue.hyps,auto)
next
case (Abrupt r')
have "Γ⊢⟨While b' c',r⟩ =n⇒ t" by fact
with Abrupt have "t=r"
by (auto dest: execn_Abrupt_end)
with r Abrupt show ?thesis
by blast
next
case Fault with r show ?thesis by blast
next
case Stuck with r show ?thesis by blast
qed
qed auto
}
with exec ctxt P t_notin_F
show ?thesis
by auto
next
case False
with exec P have "t=Normal s"
by cases auto
with P False
show ?thesis
by auto
qed
qed
next
case (Guard Θ F g P c Q A f)
have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) c Q,A" by fact
show "Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) Guard f g c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P:"s ∈ (g ∩ P)"
from exec P have "Γ⊢⟨c,Normal s⟩ =n⇒ t"
by cases auto
from valid_c ctxt this P t_notin_F
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cnvalidD)
qed
next
case (Guarantee f F Θ g P c Q A)
have valid_c: "⋀n. Γ,Θ ⊨n:⇘/F⇙ (g ∩ P) c Q,A" by fact
have f_F: "f ∈ F" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P Guard f g c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P:"s ∈ P"
from exec f_F t_notin_F have g: "s ∈ g"
by cases auto
with P have P': "s ∈ g ∩ P"
by blast
from exec P g have "Γ⊢⟨c,Normal s⟩ =n⇒ t"
by cases auto
from valid_c ctxt this P' t_notin_F
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cnvalidD)
qed
next
case (CallRec P p Q A Specs Θ F)
have p: "(P,p,Q,A) ∈ Specs" by fact
have valid_body:
"∀(P,p,Q,A) ∈ Specs. p ∈ dom Γ ∧ (∀n. Γ,Θ ∪ Specs ⊨n:⇘/F⇙ P (the (Γ p)) Q,A)"
using CallRec.hyps by blast
show "Γ,Θ⊨n:⇘/F⇙ P Call p Q,A"
proof -
{
fix n
have "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A
⟹ ∀(P,p,Q,A) ∈Specs. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
proof (induct n)
case 0
show "∀(P,p,Q,A) ∈Specs. Γ⊨0:⇘/F⇙ P (Call p) Q,A"
by (fastforce elim!: execn_elim_cases simp add: nvalid_def)
next
case (Suc m)
have hyp: "∀(P, p, Q, A)∈Θ. Γ ⊨m:⇘/F⇙ P (Call p) Q,A
⟹ ∀(P,p,Q,A) ∈Specs. Γ⊨m:⇘/F⇙ P (Call p) Q,A" by fact
have "∀(P, p, Q, A)∈Θ. Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A" by fact
hence ctxt_m: "∀(P, p, Q, A)∈Θ. Γ ⊨m:⇘/F⇙ P (Call p) Q,A"
by (fastforce simp add: nvalid_def intro: execn_Suc)
hence valid_Proc:
"∀(P,p,Q,A) ∈Specs. Γ⊨m:⇘/F⇙ P (Call p) Q,A"
by (rule hyp)
let ?Θ'= "Θ ∪ Specs"
from valid_Proc ctxt_m
have "∀(P, p, Q, A)∈?Θ'. Γ ⊨m:⇘/F⇙ P (Call p) Q,A"
by fastforce
with valid_body
have valid_body_m:
"∀(P,p,Q,A) ∈Specs. ∀n. Γ ⊨m:⇘/F⇙ P (the (Γ p)) Q,A"
by (fastforce simp add: cnvalid_def)
show "∀(P,p,Q,A) ∈Specs. Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A"
proof (clarify)
fix P p Q A assume p: "(P,p,Q,A) ∈ Specs"
show "Γ ⊨Suc m:⇘/F⇙ P (Call p) Q,A"
proof (rule nvalidI)
fix s t
assume exec_call:
"Γ⊢⟨Call p,Normal s⟩ =Suc m⇒ t"
assume Pre: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec_call
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
fix bdy m'
assume m: "Suc m = Suc m'"
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal s⟩ =m'⇒ t"
from Pre valid_body_m exec_body bdy m p t_notin_F
show ?thesis
by (fastforce simp add: nvalid_def)
next
assume "Γ p = None"
with valid_body p have False by auto
thus ?thesis ..
qed
qed
qed
qed
}
with p show ?thesis
by (fastforce simp add: cnvalid_def)
qed
next
case (DynCom P Θ F c Q A)
hence valid_c: "∀s∈P. (∀n. Γ,Θ⊨n:⇘/F⇙ P (c s) Q,A)" by auto
show "Γ,Θ⊨n:⇘/F⇙ P DynCom c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨DynCom c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_Fault: "t ∉ Fault ` F"
from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
assume "Γ⊢⟨c s,Normal s⟩ =n⇒ t"
from cnvalidD [OF valid_c [rule_format, OF P] ctxt this P t_notin_Fault]
show ?thesis .
qed
qed
next
case (Throw Θ F A Q)
show "Γ,Θ ⊨n:⇘/F⇙ A Throw Q,A"
proof (rule cnvalidI)
fix s t
assume "Γ⊢⟨Throw,Normal s⟩ =n⇒ t" "s ∈ A"
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
by cases simp
qed
next
case (Catch Θ F P c⇩1 Q R c⇩2 A)
have valid_c1: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P c⇩1 Q,R" by fact
have valid_c2: "⋀n. Γ,Θ ⊨n:⇘/F⇙ R c⇩2 Q,A" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_Fault: "t ∉ Fault ` F"
from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
fix s'
assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Abrupt s'"
assume exec_c2: "Γ⊢⟨c⇩2,Normal s'⟩ =n⇒ t"
from cnvalidD [OF valid_c1 ctxt exec_c1 P ]
have "Abrupt s' ∈ Abrupt ` R"
by auto
with cnvalidD [OF valid_c2 ctxt _ _ t_notin_Fault] exec_c2
show ?thesis
by fastforce
next
assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t"
assume notAbr: "¬ isAbr t"
from cnvalidD [OF valid_c1 ctxt exec_c1 P t_notin_Fault]
have "t ∈ Normal ` Q ∪ Abrupt ` R" .
with notAbr
show ?thesis
by auto
qed
qed
next
case (Conseq P Θ F c Q A)
hence adapt: "∀s ∈ P. (∃P' Q' A'. Γ,Θ ⊨n:⇘/F⇙ P' c Q',A' ∧
s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A)"
by blast
show "Γ,Θ ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from P adapt obtain P' Q' A' Z where
spec: "Γ,Θ⊨n:⇘/F⇙ P' c Q',A'" and
P': "s ∈ P'" and strengthen: "Q' ⊆ Q ∧ A' ⊆ A"
by auto
from spec [rule_format] ctxt exec P' t_notin_F
have "t ∈ Normal ` Q' ∪ Abrupt ` A'"
by (rule cnvalidD)
with strengthen show ?thesis
by blast
qed
qed
next
case (Asm P p Q A Θ F)
have asm: "(P, p, Q, A) ∈ Θ" by fact
show "Γ,Θ ⊨n:⇘/F⇙ P (Call p) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Call p,Normal s⟩ =n⇒ t"
from asm ctxt have "Γ ⊨n:⇘/F⇙ P Call p Q,A" by auto
moreover
assume "s ∈ P" "t ∉ Fault ` F"
ultimately
show "t ∈ Normal ` Q ∪ Abrupt ` A"
using exec
by (auto simp add: nvalid_def)
qed
next
case ExFalso thus ?case by iprover
qed
theorem hoare_sound: "Γ,Θ⊢⇘/F⇙ P c Q,A ⟹ Γ,Θ⊨⇘/F⇙ P c Q,A"
by (iprover intro: cnvalid_to_cvalid hoare_cnvalid)
subsection {* Completeness *}
lemma MGT_valid:
"Γ⊨⇘/F⇙{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t}, {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule validI)
fix s t
assume "Γ⊢⟨c,Normal s⟩ ⇒ t"
"s ∈ {s. s = Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
"t ∉ Fault ` F"
thus "t ∈ Normal ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t} ∪
Abrupt ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
by (cases t) (auto simp add: final_notin_def)
qed
text {* The consequence rule where the existential @{term Z} is instantiated
to @{term s}. Usefull in proof of @{text "MGT_lemma"}.*}
lemma ConseqMGT:
assumes modif: "∀Z. Γ,Θ ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes impl: "⋀s. s ∈ P ⟹ s ∈ P' s ∧ (∀t. t ∈ Q' s ⟶ t ∈ Q) ∧
(∀t. t ∈ A' s ⟶ t ∈ A)"
shows "Γ,Θ ⊢⇘/F⇙ P c Q,A"
using impl
by - (rule conseq [OF modif],blast)
lemma Seq_NoFaultStuckD1:
assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
shows "Γ⊢⟨c1,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
proof (rule final_notinI)
fix t
assume exec_c1: "Γ⊢⟨c1,s⟩ ⇒ t"
show "t ∉ {Stuck} ∪ Fault ` F"
proof
assume "t ∈ {Stuck} ∪ Fault ` F"
moreover
{
assume "t = Stuck"
with exec_c1
have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Stuck"
by (auto intro: exec_Seq')
with noabort have False
by (auto simp add: final_notin_def)
hence False ..
}
moreover
{
assume "t ∈ Fault ` F"
then obtain f where
t: "t=Fault f" and f: "f ∈ F"
by auto
from t exec_c1
have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Fault f"
by (auto intro: exec_Seq')
with noabort f have False
by (auto simp add: final_notin_def)
hence False ..
}
ultimately show False by auto
qed
qed
lemma Seq_NoFaultStuckD2:
assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
shows "∀t. Γ⊢⟨c1,s⟩ ⇒ t ⟶ t∉ ({Stuck} ∪ Fault ` F) ⟶
Γ⊢⟨c2,t⟩ ⇒∉({Stuck} ∪ Fault ` F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq')
lemma MGT_implies_complete:
assumes MGT: "∀Z. Γ,{}⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
assumes valid: "Γ ⊨⇘/F⇙ P c Q,A"
shows "Γ,{} ⊢⇘/F⇙ P c Q,A"
using MGT
apply (rule ConseqMGT)
apply (insert valid)
apply (auto simp add: valid_def intro!: final_notinI)
done
text {* Equipped only with the classic consequence rule @{thm "conseqPrePost"}
we can only derive this syntactically more involved version
of completeness. But semantically it is equivalent to the "real" one
(see below) *}
lemma MGT_implies_complete':
assumes MGT: "∀Z. Γ,{}⊢⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
assumes valid: "Γ ⊨⇘/F⇙ P c Q,A"
shows "Γ,{} ⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
using MGT [rule_format, of Z]
apply (rule conseqPrePost)
apply (insert valid)
apply (fastforce simp add: valid_def final_notin_def)
apply (fastforce simp add: valid_def)
apply (fastforce simp add: valid_def)
done
text {* Semantic equivalence of both kind of formulations *}
lemma valid_involved_to_valid:
assumes valid:
"∀Z. Γ⊨⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
shows "Γ ⊨⇘/F⇙ P c Q,A"
using valid
apply (simp add: valid_def)
apply clarsimp
apply (erule_tac x="x" in allE)
apply (erule_tac x="Normal x" in allE)
apply (erule_tac x=t in allE)
apply fastforce
done
text {* The sophisticated consequence rule allow us to do this
semantical transformation on the hoare-level, too.
The magic is, that it allow us to
choose the instance of @{term Z} under the assumption of an state @{term "s ∈ P"} *}
lemma
assumes deriv:
"∀Z. Γ,{}⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
shows "Γ,{} ⊢⇘/F⇙ P c Q,A"
apply (rule ConseqMGT [OF deriv])
apply auto
done
lemma valid_to_valid_involved:
"Γ ⊨⇘/F⇙ P c Q,A ⟹
Γ⊨⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
by (simp add: valid_def Collect_conv_if)
lemma
assumes deriv: "Γ,{} ⊢⇘/F⇙ P c Q,A"
shows "Γ,{}⊢⇘/F⇙ {s. s=Z ∧ s ∈ P} c {t. Z ∈ P ⟶ t ∈ Q},{t. Z ∈ P ⟶ t ∈ A}"
apply (rule conseqPrePost [OF deriv])
apply auto
done
lemma conseq_extract_state_indep_prop:
assumes state_indep_prop:"∀s ∈ P. R"
assumes to_show: "R ⟹ Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule Conseq)
apply (clarify)
apply (rule_tac x="P" in exI)
apply (rule_tac x="Q" in exI)
apply (rule_tac x="A" in exI)
using state_indep_prop to_show
by blast
lemma MGT_lemma:
assumes MGT_Calls:
"∀p∈dom Γ. ∀Z. Γ,Θ ⊢⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
shows "⋀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (induct c)
case Skip
show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Skip,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Skip
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoarep.Skip [THEN conseqPre])
(auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
case (Basic f)
show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Basic f,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Basic f
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoarep.Basic [THEN conseqPre])
(auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
next
case (Spec r)
show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Spec r,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Spec r
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoarep.Spec [THEN conseqPre])
apply (clarsimp simp add: final_notin_def)
apply (case_tac "∃t. (Z,t) ∈ r")
apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
done
next
case (Seq c1 c2)
have hyp_c1: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
have hyp_c2: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
from hyp_c1
have "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
intro: exec.Seq)
thus "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
Seq c1 c2
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule hoarep.Seq )
show "Γ,Θ⊢⇘/F⇙ {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
c2
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c2],safe)
fix r t
assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal r" "Γ⊢⟨c2,Normal r⟩ ⇒ Normal t"
then show "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t"
by (iprover intro: exec.intros)
next
fix r t
assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal r" "Γ⊢⟨c2,Normal r⟩ ⇒ Abrupt t"
then show "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (iprover intro: exec.intros)
qed
qed
next
case (Cond b c1 c2)
have "∀Z. Γ,Θ⊢⇘/F⇙{s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
hence "Γ,Θ⊢⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}∩b)
c1
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(fastforce intro: exec.CondTrue simp add: final_notin_def)
moreover
have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
hence "Γ,Θ⊢⇘/F⇙({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}∩-b)
c2
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(fastforce intro: exec.CondFalse simp add: final_notin_def)
ultimately
show "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
Cond b c1 c2
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoarep.Cond)
next
case (While b c)
let ?unroll = "({(s,t). s∈b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t})⇧*"
let ?P' = "λZ. {t. (Z,t)∈?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}"
let ?A' = "λZ. {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
show "Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
While b c
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [where ?P'="?P'"
and ?Q'="λZ. ?P' Z ∩ - b" and ?A'="?A'"])
show "∀Z. Γ,Θ⊢⇘/F⇙ (?P' Z) (While b c) (?P' Z ∩ - b),(?A' Z)"
proof (rule allI, rule hoarep.While)
fix Z
from While
have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}" by iprover
then show "Γ,Θ⊢⇘/F⇙ (?P' Z ∩ b) c (?P' Z),(?A' Z)"
proof (rule ConseqMGT)
fix s
assume "s∈ {t. (Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}
∩ b"
then obtain
Z_s_unroll: "(Z,s) ∈ ?unroll" and
noabort:"∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" and
s_in_b: "s∈b"
by blast
show "s ∈ {t. t = s ∧ Γ⊢⟨c,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Normal t} ⟶
t ∈ {t. (Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))}) ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t} ⟶
t ∈ {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t})"
(is "?C1 ∧ ?C2 ∧ ?C3")
proof (intro conjI)
from Z_s_unroll noabort s_in_b show ?C1 by blast
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Normal t"
moreover
from Z_s_unroll s_t s_in_b
have "(Z, t) ∈ ?unroll"
by (blast intro: rtrancl_into_rtrancl)
moreover note noabort
ultimately
have "(Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u))"
by iprover
}
then show ?C2 by blast
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t"
from Z_s_unroll noabort s_t s_in_b
have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t"
by blast
} thus ?C3 by simp
qed
qed
qed
next
fix s
assume P: "s ∈ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
hence WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by auto
show "s ∈ ?P' s ∧
(∀t. t∈(?P' s ∩ - b)⟶
t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t})∧
(∀t. t∈?A' s ⟶ t∈?A' Z)"
proof (intro conjI)
{
fix e
assume "(Z,e) ∈ ?unroll" "e ∈ b"
from this WhileNoFault
have "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" (is "?Prop Z e")
proof (induct rule: converse_rtrancl_induct [consumes 1])
assume e_in_b: "e ∈ b"
assume WhileNoFault: "Γ⊢⟨While b c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
with e_in_b WhileNoFault
have cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
moreover
{
fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
with e_in_b have "Γ⊢⟨While b c,Normal e⟩ ⇒ Abrupt u"
by (blast intro: exec.intros)
}
ultimately
show "?Prop e e"
by iprover
next
fix Z r
assume e_in_b: "e∈b"
assume WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
assume hyp: "⟦e∈b;Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))⟧
⟹ ?Prop r e"
assume Z_r:
"(Z, r) ∈ {(Z, r). Z ∈ b ∧ Γ⊢⟨c,Normal Z⟩ ⇒ Normal r}"
with WhileNoFault
have "Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
from hyp [OF e_in_b this] obtain
cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))" and
Abrupt_r: "∀u. Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u ⟶
Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u"
by simp
{
fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
with Abrupt_r have "Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u" by simp
moreover from Z_r obtain
"Z ∈ b" "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
by simp
ultimately have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u"
by (blast intro: exec.intros)
}
with cNoFault show "?Prop Z e"
by iprover
qed
}
with P show "s ∈ ?P' s"
by blast
next
{
fix t
assume "termination": "t ∉ b"
assume "(Z, t) ∈ ?unroll"
hence "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
proof (induct rule: converse_rtrancl_induct [consumes 1])
from "termination"
show "Γ⊢⟨While b c,Normal t⟩ ⇒ Normal t"
by (blast intro: exec.WhileFalse)
next
fix Z r
assume first_body:
"(Z, r) ∈ {(s, t). s ∈ b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
assume "(r, t) ∈ ?unroll"
assume rest_loop: "Γ⊢⟨While b c, Normal r⟩ ⇒ Normal t"
show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
proof -
from first_body obtain
"Z ∈ b" "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
by fast
moreover
from rest_loop have
"Γ⊢⟨While b c,Normal r⟩ ⇒ Normal t"
by fast
ultimately show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
by (rule exec.WhileTrue)
qed
qed
}
with P
show "(∀t. t∈(?P' s ∩ - b)
⟶t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t})"
by blast
next
from P show "∀t. t∈?A' s ⟶ t∈?A' Z" by simp
qed
qed
next
case (Call p)
let ?P = "{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
from noStuck_Call have "∀s ∈ ?P. p ∈ dom Γ"
by (fastforce simp add: final_notin_def )
then show "Γ,Θ⊢⇘/F⇙ ?P (Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
proof (rule conseq_extract_state_indep_prop)
assume p_definied: "p ∈ dom Γ"
with MGT_Calls show
"Γ,Θ⊢⇘/F⇙{s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
by (auto)
qed
next
case (DynCom c)
have hyp:
"⋀s'. ∀Z. Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨c s',Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c s'
{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Abrupt t}"
using DynCom by simp
have hyp':
"Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c Z
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT [OF hyp])
(fastforce simp add: final_notin_def intro: exec.intros)
show "Γ,Θ⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
DynCom c
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoarep.DynCom)
apply (clarsimp)
apply (rule hyp' [simplified])
done
next
case (Guard f g c)
have hyp_c: "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
using Guard by iprover
show ?case
proof (cases "f ∈ F")
case True
from hyp_c
have "Γ,Θ⊢⇘/F ⇙(g ∩ {s. s = Z ∧
Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (- F))})
c
{t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Abrupt t}"
apply (rule ConseqMGT)
apply (insert True)
apply (auto simp add: final_notin_def intro: exec.intros)
done
from True this
show ?thesis
by (rule conseqPre [OF Guarantee]) auto
next
case False
from hyp_c
have "Γ,Θ⊢⇘/F⇙
(g ∩ {s. s=Z ∧ Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))})
c
{t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Abrupt t}"
apply (rule ConseqMGT)
apply clarify
apply (frule Guard_noFaultStuckD [OF _ False])
apply (auto simp add: final_notin_def intro: exec.intros)
done
then show ?thesis
apply (rule conseqPre [OF hoarep.Guard])
apply clarify
apply (frule Guard_noFaultStuckD [OF _ False])
apply auto
done
qed
next
case Throw
show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Throw,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} Throw
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Abrupt t}"
by (rule conseqPre [OF hoarep.Throw]) (blast intro: exec.intros)
next
case (Catch c⇩1 c⇩2)
have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨c⇩1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩1
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
hence "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩1
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
by (rule ConseqMGT)
(fastforce intro: exec.intros simp add: final_notin_def)
moreover
have "∀Z. Γ,Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))} c⇩2
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
hence "Γ,Θ⊢⇘/F⇙{s. Γ⊢⟨c⇩1,Normal Z⟩ ⇒Abrupt s ∧
Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
c⇩2
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(fastforce intro: exec.intros simp add: final_notin_def)
ultimately
show "Γ,Θ⊢⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
Catch c⇩1 c⇩2
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoarep.Catch)
qed
lemma MGT_Calls:
"∀p∈dom Γ. ∀Z.
Γ,{}⊢⇘/F⇙{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
proof -
{
fix p Z
assume defined: "p ∈ dom Γ"
have
"Γ,(⋃p∈dom Γ. ⋃Z.
{({s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))},
p,
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})
⊢⇘/F⇙{s. s = Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
(the (Γ p))
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
(is "Γ,?Θ ⊢⇘/F⇙ (?Pre p Z) (the (Γ p)) (?Post p Z),(?Abr p Z)")
proof -
have MGT_Calls:
"∀p∈dom Γ. ∀Z. Γ,?Θ ⊢⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
by (intro ballI allI, rule HoarePartialDef.Asm,auto)
have "∀Z. Γ,?Θ⊢⇘/F⇙ {s. s=Z ∧ Γ⊢⟨the (Γ p) ,Normal s⟩ ⇒∉({Stuck} ∪ Fault`(-F))}
(the (Γ p))
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
by (iprover intro: MGT_lemma [OF MGT_Calls])
thus "Γ,?Θ⊢⇘/F⇙ (?Pre p Z) (the (Γ p)) (?Post p Z),(?Abr p Z)"
apply (rule ConseqMGT)
apply (clarify,safe)
proof -
assume "Γ⊢⟨Call p,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
with defined show "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (fastforce simp add: final_notin_def
intro: exec.intros)
next
fix t
assume "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t"
with defined
show "Γ⊢⟨Call p,Normal Z⟩ ⇒Normal t"
by (auto intro: exec.Call)
next
fix t
assume "Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t"
with defined
show "Γ⊢⟨Call p,Normal Z⟩ ⇒Abrupt t"
by (auto intro: exec.Call)
qed
qed
}
then show ?thesis
apply -
apply (intro ballI allI)
apply (rule CallRec' [where Procs="dom Γ" and
P="λp Z. {s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"and
Q="λp Z.
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t}" and
A="λp Z.
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"] )
apply simp+
done
qed
theorem hoare_complete: "Γ⊨⇘/F⇙ P c Q,A ⟹ Γ,{}⊢⇘/F⇙ P c Q,A"
by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Calls])
lemma hoare_complete':
assumes cvalid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
proof (cases "Γ⊨⇘/F⇙ P c Q,A")
case True
hence "Γ,{}⊢⇘/F⇙ P c Q,A"
by (rule hoare_complete)
thus "Γ,Θ⊢⇘/F ⇙P c Q,A"
by (rule hoare_augment_context) simp
next
case False
with cvalid
show ?thesis
by (rule ExFalso)
qed
lemma hoare_strip_Γ:
assumes deriv: "Γ,{}⊢⇘/F⇙ P p Q,A"
assumes F': "F' ⊆ -F"
shows "strip F' Γ,{}⊢⇘/F⇙ P p Q,A"
proof (rule hoare_complete)
from hoare_sound [OF deriv] have "Γ⊨⇘/F⇙ P p Q,A"
by (simp add: cvalid_def)
from this F'
show "strip F' Γ⊨⇘/F⇙ P p Q,A"
by (rule valid_to_valid_strip)
qed
subsection {* And Now: Some Useful Rules *}
subsubsection {* Consequence *}
lemma LiberalConseq_sound:
fixes F::"'f set"
assumes cons: "∀s ∈ P. ∀(t::('s,'f) xstate). ∃P' Q' A'. (∀n. Γ,Θ⊨n:⇘/F⇙ P' c Q',A') ∧
((s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A "
proof (rule cnvalidI)
fix s t
assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from P cons obtain P' Q' A' where
spec: "∀n. Γ,Θ⊨n:⇘/F⇙ P' c Q',A'" and
adapt: "(s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
⟶ t ∈ Normal ` Q ∪ Abrupt ` A"
apply -
apply (drule (1) bspec)
apply (erule_tac x=t in allE)
apply (elim exE conjE)
apply iprover
done
from exec spec ctxt t_notin_F
have "s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'"
by (simp add: cnvalid_def nvalid_def)
with adapt show ?thesis
by simp
qed
qed
lemma LiberalConseq:
fixes F:: "'f set"
assumes cons: "∀s ∈ P. ∀(t::('s,'f) xstate). ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
((s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule hoare_complete')
apply (rule allI)
apply (rule LiberalConseq_sound)
using cons
apply (clarify)
apply (drule (1) bspec)
apply (erule_tac x=t in allE)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply (rule conjI)
apply (blast intro: hoare_cnvalid)
apply assumption
done
lemma "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A
⟹ Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule LiberalConseq)
apply (rule ballI)
apply (drule (1) bspec)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply auto
done
lemma
fixes F:: "'f set"
assumes cons: "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
(∀(t::('s,'f) xstate). (s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule Conseq)
apply (rule ballI)
apply (insert cons)
apply (drule (1) bspec)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply (rule conjI)
apply assumption
oops
lemma LiberalConseq':
fixes F:: "'f set"
assumes cons: "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' c Q',A' ∧
(∀(t::('s,'f) xstate). (s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A')
⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule LiberalConseq)
apply (rule ballI)
apply (rule allI)
apply (insert cons)
apply (drule (1) bspec)
apply clarify
apply (rule_tac x=P' in exI)
apply (rule_tac x=Q' in exI)
apply (rule_tac x=A' in exI)
apply iprover
done
lemma LiberalConseq'':
fixes F:: "'f set"
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s (t::('s,'f) xstate).
(∀Z. s ∈ P' Z ⟶ t ∈ Normal ` Q' Z ∪ Abrupt ` A' Z)
⟶ (s ∈ P ⟶ t ∈ Normal ` Q ∪ Abrupt ` A)"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule LiberalConseq)
apply (rule ballI)
apply (rule allI)
apply (insert cons)
apply (erule_tac x=s in allE)
apply (erule_tac x=t in allE)
apply (case_tac "t ∈ Normal ` Q ∪ Abrupt ` A")
apply (insert spec)
apply iprover
apply auto
done
primrec procs:: "('s,'p,'f) com ⇒ 'p set"
where
"procs Skip = {}" |
"procs (Basic f) = {}" |
"procs (Seq c⇩1 c⇩2) = (procs c⇩1 ∪ procs c⇩2)" |
"procs (Cond b c⇩1 c⇩2) = (procs c⇩1 ∪ procs c⇩2)" |
"procs (While b c) = procs c" |
"procs (Call p) = {p}" |
"procs (DynCom c) = (⋃s. procs (c s))" |
"procs (Guard f g c) = procs c" |
"procs Throw = {}" |
"procs (Catch c⇩1 c⇩2) = (procs c⇩1 ∪ procs c⇩2)"
primrec noSpec:: "('s,'p,'f) com ⇒ bool"
where
"noSpec Skip = True" |
"noSpec (Basic f) = True" |
"noSpec (Spec r) = False" |
"noSpec (Seq c⇩1 c⇩2) = (noSpec c⇩1 ∧ noSpec c⇩2)" |
"noSpec (Cond b c⇩1 c⇩2) = (noSpec c⇩1 ∧ noSpec c⇩2)" |
"noSpec (While b c) = noSpec c" |
"noSpec (Call p) = True" |
"noSpec (DynCom c) = (∀s. noSpec (c s))" |
"noSpec (Guard f g c) = noSpec c" |
"noSpec Throw = True" |
"noSpec (Catch c⇩1 c⇩2) = (noSpec c⇩1 ∧ noSpec c⇩2)"
lemma exec_noSpec_no_Stuck:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
assumes s_no_Stuck: "s≠Stuck"
shows "t≠Stuck"
using exec noSpec_c procs_subset s_no_Stuck proof induct
case (Call p bdy s t) with noSpec_Γ procs_subset_Γ show ?case
by (auto dest!: bspec [of _ _ p])
next
case (DynCom c s t) then show ?case
by auto blast
qed auto
lemma execn_noSpec_no_Stuck:
assumes exec: "Γ⊢⟨c,s⟩ =n⇒ t"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
assumes s_no_Stuck: "s≠Stuck"
shows "t≠Stuck"
using exec noSpec_c procs_subset s_no_Stuck proof induct
case (Call p bdy n s t) with noSpec_Γ procs_subset_Γ show ?case
by (auto dest!: bspec [of _ _ p])
next
case (DynCom c s t) then show ?case
by auto blast
qed auto
lemma LiberalConseq_noguards_nothrows_sound:
assumes spec: "∀Z. ∀n. Γ,Θ⊨n:⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s t. (∀Z. s ∈ P' Z ⟶ t ∈ Q' Z )
⟶ (s ∈ P ⟶ t ∈ Q )"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A "
proof (rule cnvalidI)
fix s t
assume ctxt:"∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from execn_noguards_no_Fault [OF exec noguards_c noguards_Γ]
execn_nothrows_no_Abrupt [OF exec nothrows_c nothrows_Γ ]
execn_noSpec_no_Stuck [OF exec
noSpec_c noSpec_Γ procs_subset
procs_subset_Γ]
obtain t' where t: "t=Normal t'"
by (cases t) auto
with exec spec ctxt
have "(∀Z. s ∈ P' Z ⟶ t' ∈ Q' Z)"
by (unfold cnvalid_def nvalid_def) blast
with cons P t show ?thesis
by simp
qed
qed
lemma LiberalConseq_noguards_nothrows:
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) c (Q' Z),(A' Z)"
assumes cons: "∀s t. (∀Z. s ∈ P' Z ⟶ t ∈ Q' Z )
⟶ (s ∈ P ⟶ t ∈ Q )"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A "
apply (rule hoare_complete')
apply (rule allI)
apply (rule LiberalConseq_noguards_nothrows_sound
[OF _ cons noguards_c noguards_Γ nothrows_c nothrows_Γ
noSpec_c noSpec_Γ
procs_subset procs_subset_Γ])
apply (insert spec)
apply (intro allI)
apply (erule_tac x=Z in allE)
by (rule hoare_cnvalid)
lemma
assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙{s. s=fst Z ∧ P s (snd Z)} c {t. Q (fst Z) (snd Z) t},{}"
assumes noguards_c: "noguards c"
assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
assumes nothrows_c: "nothrows c"
assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
assumes noSpec_c: "noSpec c"
assumes noSpec_Γ: "∀p ∈ dom Γ. noSpec (the (Γ p))"
assumes procs_subset: "procs c ⊆ dom Γ"
assumes procs_subset_Γ: "∀p ∈ dom Γ. procs (the (Γ p)) ⊆ dom Γ"
shows "∀σ. Γ,Θ⊢⇘/F⇙{s. s=σ} c {t. ∀l. P σ l ⟶ Q σ l t},{}"
apply (rule allI)
apply (rule LiberalConseq_noguards_nothrows
[OF spec _ noguards_c noguards_Γ nothrows_c nothrows_Γ
noSpec_c noSpec_Γ
procs_subset procs_subset_Γ])
apply auto
done
subsubsection {* Modify Return *}
lemma ProcModifyReturn_sound:
assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call init p return' c Q,A"
assumes valid_modif:
"∀σ. ∀n. Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
assumes ret_modif:
"∀s t. t ∈ Modif (init s)
⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (call init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "Γ⊢⟨call init p return c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
assume n: "n = Suc m"
from exec_body n bdy
have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Normal t'"
by (auto simp add: intro: execn.Call)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
have "t' ∈ Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') =
Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "Γ⊢⟨call init p return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_call)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also from exec_body n bdy
have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
have "t' ∈ ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "Γ⊢⟨call init p return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_callAbrupt)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m"
"t = Fault f"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callFault)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix bdy m
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
"t = Stuck"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callStuck)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "Γ p = None"
and "n = Suc m" "t = Stuck"
then have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callUndefined)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma ProcModifyReturn:
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 return_conform:
"∀s t. t ∈ ModifAbr (init s)
⟶ (return' s t) = (return s t)"
assumes modifies_spec:
"∀σ. Γ,Θ⊢⇘/UNIV⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (call init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule ProcModifyReturn_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform] )
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
lemma ProcModifyReturnSameFaults_sound:
assumes valid_call: "∀n. Γ,Θ ⊨n:⇘/F⇙ P call init p return' c Q,A"
assumes valid_modif:
"∀σ. ∀n. Γ,Θ⊨n:⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
assumes ret_modif:
"∀s t. t ∈ Modif (init s)
⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (call init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨call init p return c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
assume n: "n = Suc m"
from exec_body n bdy
have "Γ⊢⟨Call p,Normal (init s)⟩ =n⇒ Normal t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
have "t' ∈ Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') =
Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "Γ⊢⟨call init p return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_call)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also
from exec_body n bdy
have "Γ⊢⟨Call p,Normal (init s)⟩ =n ⇒ Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
have "t' ∈ ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "Γ⊢⟨call init p return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_callAbrupt)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callFault)
from cnvalidD [OF valid_call [rule_format] ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy m
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
"t = Stuck"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callStuck)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "Γ p = None"
and "n = Suc m" "t = Stuck"
then have "Γ⊢⟨call init p return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callUndefined)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma ProcModifyReturnSameFaults:
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 return_conform:
"∀s t. t ∈ ModifAbr (init s) ⟶ (return' s t) = (return s t)"
assumes modifies_spec:
"∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (call init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule ProcModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform])
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
subsubsection {* DynCall *}
lemma dynProcModifyReturn_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
"∀s ∈ P. ∀σ. ∀n.
Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
"∀s t. t ∈ Modif (init s)
⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "Γ⊢⟨dynCall init p return c,Normal s⟩ =n⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P: "s ∈ P"
with valid_modif
have valid_modif': "∀σ. ∀n.
Γ,Θ⊨n:⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
by blast
from exec
have "Γ⊢⟨call init (p s) return c,Normal s⟩ =n⇒ t"
by (cases rule: execn_dynCall_Normal_elim)
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
assume n: "n = Suc m"
from exec_body n bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n⇒ Normal t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' ∈ Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_call)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also from exec_body n bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n⇒ Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' ∈ ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_callAbrupt)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m"
"t = Fault f"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callFault)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix bdy m
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
"t = Stuck"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callStuck)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "Γ (p s) = None"
and "n = Suc m" "t = Stuck"
hence "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callUndefined)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma dynProcModifyReturn:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall init p return' c Q,A"
assumes ret_modif:
"∀s t. t ∈ Modif (init s)
⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
⟶ return' s t = return s t"
assumes modif:
"∀s ∈ P. ∀σ.
Γ,Θ⊢⇘/UNIV⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (dynCall init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "⋀n. Γ,Θ ⊨n:⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
"∀s ∈ P. ∀σ. ∀n.
Γ,Θ⊨n:⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
assumes ret_modif:
"∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t"
shows "Γ,Θ ⊨n:⇘/F⇙ P (dynCall init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨dynCall init p return c,Normal s⟩ =n⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P: "s ∈ P"
with valid_modif
have valid_modif': "∀σ. ∀n.
Γ,Θ⊨n:⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
by blast
from exec
have "Γ⊢⟨call init (p s) return c,Normal s⟩ =n⇒ t"
by (cases rule: execn_dynCall_Normal_elim)
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
assume n: "n = Suc m"
from exec_body n bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n ⇒ Normal t'"
by (auto simp add: intro: execn.Call)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' ∈ Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_call)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also from exec_body n bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ =n ⇒ Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' ∈ ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ =n⇒ t"
by (auto intro: execn_callAbrupt)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Fault f" "n = Suc m" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callFault)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy m
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ =m⇒ Stuck" "n = Suc m"
"t = Stuck"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callStuck)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "Γ (p s) = None"
and "n = Suc m" "t = Stuck"
hence "Γ⊢⟨call init (p s) return' c ,Normal s⟩ =n⇒ t"
by (auto intro: execn_callUndefined)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ =n⇒ t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊢⇘/F⇙ P dynCall init p return' c Q,A"
assumes ret_modif:
"∀s t. t ∈ Modif (init s)
⟶ return' s t = return s t"
assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s)
⟶ return' s t = return s t"
assumes modif:
"∀s ∈ P. ∀σ. Γ,Θ⊢⇘/F⇙ {σ} Call (p s) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇘/F⇙ P (dynCall init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProcModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
subsubsection {* Conjunction of Postcondition *}
lemma PostConjI_sound:
assumes valid_Q: "∀n. Γ,Θ ⊨n:⇘/F⇙ P c Q,A"
assumes valid_R: "∀n. Γ,Θ ⊨n:⇘/F⇙ P c R,B"
shows "Γ,Θ ⊨n:⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from valid_Q [rule_format] ctxt exec P t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cnvalidD)
moreover
from valid_R [rule_format] ctxt exec P t_notin_F have "t ∈ Normal ` R ∪ Abrupt ` B"
by (rule cnvalidD)
ultimately show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ B)"
by blast
qed
lemma PostConjI:
assumes deriv_Q: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes deriv_R: "Γ,Θ⊢⇘/F⇙ P c R,B"
shows "Γ,Θ⊢⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
apply (rule hoare_complete')
apply (rule allI)
apply (rule PostConjI_sound)
using deriv_Q
apply (blast intro: hoare_cnvalid)
using deriv_R
apply (blast intro: hoare_cnvalid)
done
lemma Merge_PostConj_sound:
assumes validF: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
assumes validG: "∀n. Γ,Θ⊨n:⇘/G⇙ P' c R,X"
assumes F_G: "F ⊆ G"
assumes P_P': "P ⊆ P'"
shows "Γ,Θ⊨n:⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
with F_G have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/G⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
with P_P' have P': "s ∈ P'"
by auto
assume t_noFault: "t ∉ Fault ` F"
show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ X)"
proof -
from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault]
have "t ∈ Normal ` Q ∪ Abrupt ` A".
moreover from this have "t ∉ Fault ` G"
by auto
from cnvalidD [OF validG [rule_format] ctxt' exec P' this]
have "t ∈ Normal ` R ∪ Abrupt ` X" .
ultimately show ?thesis by auto
qed
qed
lemma Merge_PostConj:
assumes validF: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes validG: "Γ,Θ⊢⇘/G⇙ P' c R,X"
assumes F_G: "F ⊆ G"
assumes P_P': "P ⊆ P'"
shows "Γ,Θ⊢⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
using validF apply (blast intro:hoare_cnvalid)
using validG apply (blast intro:hoare_cnvalid)
done
subsubsection {* Weaken Context *}
lemma WeakenContext_sound:
assumes valid_c: "∀n. Γ,Θ'⊨n:⇘/F⇙ P c Q,A"
assumes valid_ctxt: "∀(P, p, Q, A)∈Θ'. Γ,Θ⊨n:⇘/F⇙ P (Call p) Q,A"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
with valid_ctxt
have ctxt': "∀(P, p, Q, A)∈Θ'. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
by (simp add: cnvalid_def)
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from valid_c [rule_format] ctxt' exec P t_notin_F
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cnvalidD)
qed
lemma WeakenContext:
assumes deriv_c: "Γ,Θ'⊢⇘/F⇙ P c Q,A"
assumes deriv_ctxt: "∀(P,p,Q,A)∈Θ'. Γ,Θ⊢⇘/F⇙ P (Call p) Q,A"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule WeakenContext_sound)
using deriv_c
apply (blast intro: hoare_cnvalid)
using deriv_ctxt
apply (blast intro: hoare_cnvalid)
done
subsubsection {* Guards and Guarantees *}
lemma SplitGuards_sound:
assumes valid_c1: "∀n. Γ,Θ⊨n:⇘/F⇙ P c⇩1 Q,A"
assumes valid_c2: "∀n. Γ,Θ⊨n:⇘/F⇙ P c⇩2 UNIV,UNIV"
assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases t)
case Normal
with inter_guards_execn_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
from valid_c1 [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
case Abrupt
with inter_guards_execn_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
from valid_c1 [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
case (Fault f)
with exec inter_guards_execn_Fault [OF c]
have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Fault f ∨ Γ⊢⟨c⇩2,Normal s⟩ =n⇒ Fault f"
by auto
then show ?thesis
proof (cases rule: disjE [consumes 1])
assume "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Fault f"
from Fault cnvalidD [OF valid_c1 [rule_format] ctxt this P] t_notin_F
show ?thesis
by blast
next
assume "Γ⊢⟨c⇩2,Normal s⟩ =n⇒ Fault f"
from Fault cnvalidD [OF valid_c2 [rule_format] ctxt this P] t_notin_F
show ?thesis
by blast
qed
next
case Stuck
with inter_guards_execn_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t" by simp
from valid_c1 [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma SplitGuards:
assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
assumes deriv_c1: "Γ,Θ⊢⇘/F⇙ P c⇩1 Q,A"
assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P c⇩2 UNIV,UNIV"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule SplitGuards_sound [OF _ _ c])
using deriv_c1
apply (blast intro: hoare_cnvalid)
using deriv_c2
apply (blast intro: hoare_cnvalid)
done
lemma CombineStrip_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
assumes valid_strip: "∀n. Γ,Θ⊨n:⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases t)
case (Normal t')
from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
show ?thesis
by auto
next
case (Abrupt t')
from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
show ?thesis
by auto
next
case (Fault f)
show ?thesis
proof (cases "f ∈ F")
case True
hence "f ∉ -F" by simp
with exec Fault
have "Γ⊢⟨strip_guards (-F) c,Normal s⟩ =n⇒ Fault f"
by (auto intro: execn_to_execn_strip_guards_Fault)
from cnvalidD [OF valid_strip [rule_format] ctxt this P] Fault
have False
by auto
thus ?thesis ..
next
case False
with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
show ?thesis
by auto
qed
next
case Stuck
from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
show ?thesis
by auto
qed
qed
lemma CombineStrip:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes deriv_strip: "Γ,Θ⊢⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule CombineStrip_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
apply (iprover intro: hoare_cnvalid [OF deriv_strip])
done
lemma GuardsFlip_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
assumes validFlip: "∀n. Γ,Θ⊨n:⇘/-F⇙ P c UNIV,UNIV"
shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
from ctxt have ctxtFlip: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/-F⇙ P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases t)
case (Normal t')
from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
show ?thesis
by auto
next
case (Abrupt t')
from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
show ?thesis
by auto
next
case (Fault f)
show ?thesis
proof (cases "f ∈ F")
case True
hence "f ∉ -F" by simp
with cnvalidD [OF validFlip [rule_format] ctxtFlip exec P] Fault
have False
by auto
thus ?thesis ..
next
case False
with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
show ?thesis
by auto
qed
next
case Stuck
from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
show ?thesis
by auto
qed
qed
lemma GuardsFlip:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes derivFlip: "Γ,Θ⊢⇘/-F⇙ P c UNIV,UNIV"
shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule GuardsFlip_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
apply (iprover intro: hoare_cnvalid [OF derivFlip])
done
lemma MarkGuardsI_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
shows "Γ,Θ⊨n:⇘/{}⇙ P mark_guards f c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ t"
from execn_mark_guards_to_execn [OF exec] obtain t' where
exec_c: "Γ⊢⟨c,Normal s⟩ =n⇒ t'" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from cnvalidD [OF valid [rule_format] ctxt exec_c P]
have "t' ∈ Normal ` Q ∪ Abrupt ` A"
by blast
with t'_noFault
show ?thesis
by auto
qed
qed
lemma MarkGuardsI:
assumes deriv: "Γ,Θ⊢⇘/{}⇙ P c Q,A"
shows "Γ,Θ⊢⇘/{}⇙ P mark_guards f c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MarkGuardsI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma MarkGuardsD_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P mark_guards f c Q,A"
shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases "isFault t")
case True
with execn_to_execn_mark_guards_Fault [OF exec ]
obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ Fault f'"
by (fastforce elim: isFaultE)
from cnvalidD [OF valid [rule_format] ctxt this P]
have False
by auto
thus ?thesis ..
next
case False
from execn_to_execn_mark_guards [OF exec False]
obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ =n⇒ t"
by auto
from cnvalidD [OF valid [rule_format] ctxt this P]
show ?thesis
by auto
qed
qed
lemma MarkGuardsD:
assumes deriv: "Γ,Θ⊢⇘/{}⇙ P mark_guards f c Q,A"
shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MarkGuardsD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma MergeGuardsI_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨n:⇘/F⇙ P merge_guards c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ =n⇒ t"
from execn_merge_guards_to_execn [OF exec_merge]
have exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t" .
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from cnvalidD [OF valid [rule_format] ctxt exec P t_notin_F]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed
lemma MergeGuardsI:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇘/F⇙ P merge_guards c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MergeGuardsI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma MergeGuardsD_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P merge_guards c Q,A"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
from execn_to_execn_merge_guards [OF exec]
have exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ =n⇒ t".
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from cnvalidD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed
lemma MergeGuardsD:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P merge_guards c Q,A"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule MergeGuardsD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma SubsetGuards_sound:
assumes c_c': "c ⊆⇩g c'"
assumes valid: "∀n. Γ,Θ⊨n:⇘/{}⇙ P c' Q,A"
shows "Γ,Θ⊨n:⇘/{}⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
from execn_to_execn_subseteq_guards [OF c_c' exec] obtain t' where
exec_c': "Γ⊢⟨c',Normal s⟩ =n⇒ t'" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
from cnvalidD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by auto
qed
lemma SubsetGuards:
assumes c_c': "c ⊆⇩g c'"
assumes deriv: "Γ,Θ⊢⇘/{}⇙ P c' Q,A"
shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule SubsetGuards_sound [OF c_c'])
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma NormalizeD_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P (normalize c) Q,A"
shows "Γ,Θ⊨n:⇘/F⇙ P c Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
hence exec_norm: "Γ⊢⟨normalize c,Normal s⟩ =n⇒ t"
by (rule execn_to_execn_normalize)
assume P: "s ∈ P"
assume noFault: "t ∉ Fault ` F"
from cnvalidD [OF valid [rule_format] ctxt exec_norm P noFault]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed
lemma NormalizeD:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P (normalize c) Q,A"
shows "Γ,Θ⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule NormalizeD_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
lemma NormalizeI_sound:
assumes valid: "∀n. Γ,Θ⊨n:⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨n:⇘/F⇙ P (normalize c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P (Call p) Q,A"
assume "Γ⊢⟨normalize c,Normal s⟩ =n⇒ t"
hence exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
by (rule execn_normalize_to_execn)
assume P: "s ∈ P"
assume noFault: "t ∉ Fault ` F"
from cnvalidD [OF valid [rule_format] ctxt exec P noFault]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
qed
lemma NormalizeI:
assumes deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇘/F⇙ P (normalize c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule NormalizeI_sound)
apply (iprover intro: hoare_cnvalid [OF deriv])
done
subsubsection {* Restricting the Procedure Environment *}
lemma nvalid_restrict_to_nvalid:
assumes valid_c: "Γ|⇘M⇙⊨n:⇘/F⇙ P c Q,A"
shows "Γ⊨n:⇘/F⇙ P c Q,A"
proof (rule nvalidI)
fix s t
assume exec: "Γ⊢⟨c,Normal s⟩ =n⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from execn_to_execn_restrict [OF exec]
obtain t' where
exec_res: "Γ|⇘M⇙⊢⟨c,Normal s⟩ =n⇒ t'" and
t_Fault: "∀f. t = Fault f ⟶ t' ∈ {Fault f, Stuck}" and
t'_notStuck: "t'≠Stuck ⟶ t'=t"
by blast
from t_Fault t_notin_F t'_notStuck have "t' ∉ Fault ` F"
by (cases t') auto
with valid_c exec_res P
have "t' ∈ Normal ` Q ∪ Abrupt ` A"
by (auto simp add: nvalid_def)
with t'_notStuck
show ?thesis
by auto
qed
qed
lemma valid_restrict_to_valid:
assumes valid_c: "Γ|⇘M⇙⊨⇘/F⇙ P c Q,A"
shows "Γ⊨⇘/F⇙ P c Q,A"
proof (rule validI)
fix s t
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof -
from exec_to_exec_restrict [OF exec]
obtain t' where
exec_res: "Γ|⇘M⇙⊢⟨c,Normal s⟩ ⇒ t'" and
t_Fault: "∀f. t = Fault f ⟶ t' ∈ {Fault f, Stuck}" and
t'_notStuck: "t'≠Stuck ⟶ t'=t"
by blast
from t_Fault t_notin_F t'_notStuck have "t' ∉ Fault ` F"
by (cases t') auto
with valid_c exec_res P
have "t' ∈ Normal ` Q ∪ Abrupt ` A"
by (auto simp add: valid_def)
with t'_notStuck
show ?thesis
by auto
qed
qed
lemma augment_procs:
assumes deriv_c: "Γ|⇘M⇙,{}⊢⇘/F⇙ P c Q,A"
shows "Γ,{}⊢⇘/F⇙ P c Q,A"
apply (rule hoare_complete)
apply (rule valid_restrict_to_valid)
apply (insert hoare_sound [OF deriv_c])
by (simp add: cvalid_def)
lemma augment_Faults:
assumes deriv_c: "Γ,{}⊢⇘/F⇙ P c Q,A"
assumes F: "F ⊆ F'"
shows "Γ,{}⊢⇘/F'⇙ P c Q,A"
apply (rule hoare_complete)
apply (rule valid_augment_Faults [OF _ F])
apply (insert hoare_sound [OF deriv_c])
by (simp add: cvalid_def)
end