section {* Properties of Total Correctness Hoare Logic *}
theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin
subsection {* Soundness *}
lemma hoaret_sound:
assumes hoare: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
using hoare
proof (induct)
case (Skip Θ F P A)
show "Γ,Θ ⊨⇩t⇘/F⇙ P Skip P,A"
proof (rule cvalidtI)
fix s t
assume "Γ⊢⟨Skip,Normal s⟩ ⇒ t" "s ∈ P"
thus "t ∈ Normal ` P ∪ Abrupt ` A"
by cases auto
next
fix s show "Γ⊢Skip ↓ Normal s"
by (rule terminates.intros)
qed
next
case (Basic Θ F f P A)
show "Γ,Θ ⊨⇩t⇘/F⇙ {s. f s ∈ P} (Basic f) P,A"
proof (rule cvalidtI)
fix s t
assume "Γ⊢⟨Basic f,Normal s⟩ ⇒ t" "s ∈ {s. f s ∈ P}"
thus "t ∈ Normal ` P ∪ Abrupt ` A"
by cases auto
next
fix s show "Γ⊢Basic f ↓ Normal s"
by (rule terminates.intros)
qed
next
case (Spec Θ F r Q A)
show "Γ,Θ⊨⇩t⇘/F⇙ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A"
proof (rule cvalidtI)
fix s t
assume "Γ⊢⟨Spec r ,Normal s⟩ ⇒ t"
"s ∈ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)}"
thus "t ∈ Normal ` Q ∪ Abrupt ` A"
by cases auto
next
fix s show "Γ⊢Spec r ↓ Normal s"
by (rule terminates.intros)
qed
next
case (Seq Θ F P c1 R A c2 Q)
have valid_c1: "Γ,Θ ⊨⇩t⇘/F⇙ P c1 R,A" by fact
have valid_c2: "Γ,Θ ⊨⇩t⇘/F⇙ R c2 Q,A" by fact
show "Γ,Θ ⊨⇩t⇘/F⇙ P Seq c1 c2 Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec P obtain r where
exec_c1: "Γ⊢⟨c1,Normal s⟩ ⇒ r" and exec_c2: "Γ⊢⟨c2,r⟩ ⇒ t"
by cases auto
with t_notin_F have "r ∉ Fault ` F"
by (auto dest: Fault_end)
from valid_c1 ctxt exec_c1 P this
have r: "r ∈ Normal ` R ∪ Abrupt ` A"
by (rule cvalidt_postD)
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 cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F])
apply auto
done
next
case (Abrupt r')
with exec_c2 have "t=Abrupt r'"
by (auto elim: exec_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
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s∈P"
show "Γ⊢Seq c1 c2 ↓ Normal s"
proof -
from valid_c1 ctxt P
have "Γ⊢c1↓ Normal s"
by (rule cvalidt_termD)
moreover
{
fix r assume exec_c1: "Γ⊢⟨c1,Normal s⟩ ⇒ r"
have "Γ⊢c2 ↓ r"
proof (cases r)
case (Normal r')
with cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
have r: "r∈Normal ` R"
by auto
with cvalidt_termD [OF valid_c2 ctxt] exec_c1
show "Γ⊢c2 ↓ r"
by auto
qed auto
}
ultimately show ?thesis
by (iprover intro: terminates.intros)
qed
qed
next
case (Cond Θ F P b c1 Q A c2)
have valid_c1: "Γ,Θ ⊨⇩t⇘/F⇙ (P ∩ b) c1 Q,A" by fact
have valid_c2: "Γ,Θ ⊨⇩t⇘/F⇙ (P ∩ - b) c2 Q,A" by fact
show "Γ,Θ ⊨⇩t⇘/F⇙ P Cond b c1 c2 Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒ 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⟩ ⇒ t"
by cases auto
with P True
show ?thesis
by - (rule cvalidt_postD [OF valid_c1 ctxt _ _ t_notin_F],auto)
next
case False
with exec P have "Γ⊢⟨c2,Normal s⟩ ⇒ t"
by cases auto
with P False
show ?thesis
by - (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F],auto)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
thus "Γ⊢Cond b c1 c2 ↓ Normal s"
using cvalidt_termD [OF valid_c1 ctxt] cvalidt_termD [OF valid_c2 ctxt]
by (cases "s ∈ b") (auto intro: terminates.intros)
qed
next
case (While r Θ F P b c A)
assume wf: "wf r"
have valid_c: "∀σ. Γ,Θ⊨⇩t⇘/F⇙ ({σ} ∩ P ∩ b) c ({t. (t, σ) ∈ r} ∩ P),A"
using While.hyps by iprover
show "Γ,Θ ⊨⇩t⇘/F⇙ P (While b c) (P ∩ - b),A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume wprems: "Γ⊢⟨While b c,Normal s⟩ ⇒ t" "s ∈ P" "t ∉ Fault ` F"
from wf
have "⋀t. ⟦Γ⊢⟨While b c,Normal s⟩ ⇒ t; s ∈ P; t ∉ Fault ` F⟧
⟹ t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
proof (induct)
fix s t
assume hyp:
"⋀s' t. ⟦(s',s)∈r; Γ⊢⟨While b c,Normal s'⟩ ⇒ t; s' ∈ P; t ∉ Fault ` F⟧
⟹ t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
assume exec: "Γ⊢⟨While b c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec
show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A"
proof (cases)
fix s'
assume b: "s∈b"
assume exec_c: "Γ⊢⟨c,Normal s⟩ ⇒ s'"
assume exec_w: "Γ⊢⟨While b c,s'⟩ ⇒ t"
from exec_w t_notin_F have "s' ∉ Fault ` F"
by (auto dest: Fault_end)
from exec_c P b valid_c ctxt this
have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P) ∪ Abrupt ` A"
by (auto simp add: cvalidt_def validt_def valid_def)
show ?thesis
proof (cases s')
case Normal
with exec_w s' t_notin_F
show ?thesis
by - (rule hyp,auto)
next
case Abrupt
with exec_w have "t=s'"
by (auto dest: Abrupt_end)
with Abrupt s' show ?thesis
by blast
next
case Fault
with exec_w have "t=s'"
by (auto dest: Fault_end)
with Fault s' show ?thesis
by blast
next
case Stuck
with exec_w have "t=s'"
by (auto dest: Stuck_end)
with Stuck s' show ?thesis
by blast
qed
next
assume "s∉b" "t=Normal s" with P show ?thesis by simp
qed
qed
with wprems show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" by blast
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume "s ∈ P"
with wf
show "Γ⊢While b c ↓ Normal s"
proof (induct)
fix s
assume hyp: "⋀s'. ⟦(s',s)∈r; s' ∈ P⟧
⟹ Γ⊢While b c ↓ Normal s'"
assume P: "s ∈ P"
show "Γ⊢While b c ↓ Normal s"
proof (cases "s ∈ b")
case False with P show ?thesis
by (blast intro: terminates.intros)
next
case True
with valid_c P ctxt
have "Γ⊢c ↓ Normal s"
by (simp add: cvalidt_def validt_def)
moreover
{
fix s'
assume exec_c: "Γ⊢⟨c,Normal s⟩ ⇒ s'"
have "Γ⊢While b c ↓ s'"
proof (cases s')
case (Normal s'')
with exec_c P True valid_c ctxt
have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P)"
by (fastforce simp add: cvalidt_def validt_def valid_def)
then show ?thesis
by (blast intro: hyp)
qed auto
}
ultimately
show ?thesis
by (blast intro: terminates.intros)
qed
qed
qed
next
case (Guard Θ F g P c Q A f)
have valid_c: "Γ,Θ ⊨⇩t⇘/F⇙ (g ∩ P) c Q,A" by fact
show "Γ,Θ ⊨⇩t⇘/F⇙ (g ∩ P) Guard f g c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ ⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P:"s ∈ (g ∩ P)"
from exec P have "Γ⊢⟨c,Normal s⟩ ⇒ t"
by cases auto
from valid_c ctxt this P t_notin_F
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cvalidt_postD)
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P:"s ∈ (g ∩ P)"
thus "Γ⊢Guard f g c ↓ Normal s"
by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
qed
next
case (Guarantee f F Θ g P c Q A)
have valid_c: "Γ,Θ ⊨⇩t⇘/F⇙ (g ∩ P) c Q,A" by fact
have f_F: "f ∈ F" by fact
show "Γ,Θ ⊨⇩t⇘/F⇙ P Guard f g c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Guard f g c,Normal s⟩ ⇒ 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 g have "Γ⊢⟨c,Normal s⟩ ⇒ t"
by cases auto
from valid_c ctxt this P' t_notin_F
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cvalidt_postD)
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P:"s ∈ P"
thus "Γ⊢Guard f g c ↓ Normal s"
by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
qed
next
case (CallRec P p Q A Specs r Specs_wf Θ F)
have p: "(P,p,Q,A) ∈ Specs" by fact
have wf: "wf r" by fact
have Specs_wf:
"Specs_wf = (λp τ. (λ(P,q,Q,A). (P ∩ {s. ((s, q),τ,p) ∈ r},q,Q,A)) ` Specs)" by fact
from CallRec.hyps
have valid_body:
"∀(P, p, Q, A)∈Specs. p ∈ dom Γ ∧
(∀τ. Γ,Θ ∪ Specs_wf p τ⊨⇩t⇘/F⇙ ({τ} ∩ P) the (Γ p) Q,A)" by auto
show "Γ,Θ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
proof -
{
fix τp
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
from wf
have "⋀τ p P Q A. ⟦τp = (τ,p); (P,p,Q,A) ∈ Specs⟧ ⟹
Γ⊨⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ (p))) Q,A"
proof (induct τp rule: wf_induct [rule_format, consumes 1, case_names WF])
case (WF τp τ p P Q A)
have τp: "τp = (τ, p)" by fact
have p: "(P, p, Q, A) ∈ Specs" by fact
{
fix q P' Q' A'
assume q: "(P',q,Q',A') ∈ Specs"
have "Γ⊨⇩t⇘/F⇙ (P' ∩ {s. ((s,q), τ,p) ∈ r}) (Call q) Q',A'"
proof (rule validtI)
fix s t
assume exec_q:
"Γ⊢⟨Call q,Normal s⟩ ⇒ t"
assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}"
assume t_notin_F: "t ∉ Fault ` F"
from Pre q τp
have valid_bdy:
"Γ⊨⇩t⇘/F⇙ ({s} ∩ P') the (Γ q) Q',A'"
by - (rule WF.hyps, auto)
from Pre q
have Pre': "s ∈ {s} ∩ P'"
by auto
from exec_q show "t ∈ Normal ` Q' ∪ Abrupt ` A'"
proof (cases)
fix bdy
assume bdy: "Γ q = Some bdy"
assume exec_bdy: "Γ⊢⟨bdy,Normal s⟩ ⇒ t"
from valid_bdy [simplified bdy option.sel] t_notin_F exec_bdy Pre'
have "t ∈ Normal ` Q' ∪ Abrupt ` A'"
by (auto simp add: validt_def valid_def)
with Pre q
show ?thesis
by auto
next
assume "Γ q = None"
with q valid_body have False by auto
thus ?thesis ..
qed
next
fix s
assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}"
from Pre q τp
have valid_bdy:
"Γ ⊨⇩t⇘/F⇙ ({s} ∩ P') (the (Γ q)) Q',A'"
by - (rule WF.hyps, auto)
from Pre q
have Pre': "s ∈ {s} ∩ P'"
by auto
from valid_bdy ctxt Pre'
have "Γ⊢the (Γ q) ↓ Normal s"
by (auto simp add: validt_def)
with valid_body q
show "Γ⊢Call q↓ Normal s"
by (fastforce intro: terminates.Call)
qed
}
hence "∀(P, p, Q, A)∈Specs_wf p τ. Γ⊨⇩t⇘/F⇙ P Call p Q,A"
by (auto simp add: cvalidt_def Specs_wf)
with ctxt have "∀(P, p, Q, A)∈Θ ∪ Specs_wf p τ. Γ⊨⇩t⇘/F⇙ P Call p Q,A"
by auto
with p valid_body
show "Γ ⊨⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A"
by (simp add: cvalidt_def) blast
qed
}
note lem = this
have valid_body':
"⋀τ. ∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A ⟹
∀(P,p,Q,A)∈Specs. Γ⊨⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A"
by (auto intro: lem)
show "Γ,Θ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec_call: "Γ⊢⟨Call p,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec_call show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
fix bdy
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal s⟩ ⇒ t"
from exec_body bdy p P t_notin_F
valid_body' [of "s", OF ctxt]
ctxt
have "t ∈ Normal ` Q ∪ Abrupt ` A"
apply (simp only: cvalidt_def validt_def valid_def)
apply (drule (1) bspec)
apply auto
done
with p P
show ?thesis
by simp
next
assume "Γ p = None"
with p valid_body have False by auto
thus ?thesis by simp
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
show "Γ⊢Call p ↓ Normal s"
proof -
from ctxt P p valid_body' [of "s",OF ctxt]
have "Γ⊢(the (Γ p)) ↓ Normal s"
by (auto simp add: cvalidt_def validt_def)
with valid_body p show ?thesis
by (fastforce intro: terminates.Call)
qed
qed
qed
next
case (DynCom P Θ F c Q A)
hence valid_c: "∀s∈P. Γ,Θ⊨⇩t⇘/F⇙ P (c s) Q,A" by simp
show "Γ,Θ⊨⇩t⇘/F⇙ P DynCom c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨DynCom c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
assume "Γ⊢⟨c s,Normal s⟩ ⇒ t"
from cvalidt_postD [OF valid_c [rule_format, OF P] ctxt this P t_notin_F]
show ?thesis .
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
show "Γ⊢DynCom c ↓ Normal s"
proof -
from cvalidt_termD [OF valid_c [rule_format, OF P] ctxt P]
have "Γ⊢c s ↓ Normal s" .
thus ?thesis
by (rule terminates.intros)
qed
qed
next
case (Throw Θ F A Q)
show "Γ,Θ ⊨⇩t⇘/F⇙ A Throw Q,A"
proof (rule cvalidtI)
fix s t
assume "Γ⊢⟨Throw,Normal s⟩ ⇒ t" "s ∈ A"
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
by cases simp
next
fix s
show "Γ⊢Throw ↓ Normal s"
by (rule terminates.intros)
qed
next
case (Catch Θ F P c⇩1 Q R c⇩2 A)
have valid_c1: "Γ,Θ ⊨⇩t⇘/F⇙ P c⇩1 Q,R" by fact
have valid_c2: "Γ,Θ ⊨⇩t⇘/F⇙ R c⇩2 Q,A" by fact
show "Γ,Θ ⊨⇩t⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases)
fix s'
assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ ⇒ Abrupt s'"
assume exec_c2: "Γ⊢⟨c⇩2,Normal s'⟩ ⇒ t"
from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
have "Abrupt s' ∈ Abrupt ` R"
by auto
with cvalidt_postD [OF valid_c2 ctxt] exec_c2 t_notin_F
show ?thesis
by fastforce
next
assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ ⇒ t"
assume notAbr: "¬ isAbr t"
from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] t_notin_F
have "t ∈ Normal ` Q ∪ Abrupt ` R" .
with notAbr
show ?thesis
by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
show "Γ⊢Catch c⇩1 c⇩2 ↓ Normal s"
proof -
from valid_c1 ctxt P
have "Γ⊢c⇩1↓ Normal s"
by (rule cvalidt_termD)
moreover
{
fix r assume exec_c1: "Γ⊢⟨c⇩1,Normal s⟩ ⇒ Abrupt r"
from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
have r: "Abrupt r∈Normal ` Q ∪ Abrupt ` R"
by auto
hence "Abrupt r∈Abrupt ` R" by fast
with cvalidt_termD [OF valid_c2 ctxt] exec_c1
have "Γ⊢c⇩2 ↓ Normal r"
by fast
}
ultimately show ?thesis
by (iprover intro: terminates.intros)
qed
qed
next
case (Conseq P Θ F c Q A)
hence adapt:
"∀s ∈ P. (∃P' Q' A'. (Γ,Θ ⊨⇩t⇘/F⇙ P' c Q',A') ∧ s ∈ P'∧ Q' ⊆ Q ∧ A' ⊆ A)" by blast
show "Γ,Θ ⊨⇩t⇘/F⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
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 adapt [rule_format, OF P]
obtain P' and Q' and A' where
valid_P'_Q': "Γ,Θ ⊨⇩t⇘/F⇙ P' c Q',A'"
and weaken: "s ∈ P'" "Q' ⊆ Q" "A'⊆ A"
by blast
from exec valid_P'_Q' ctxt t_notin_F
have P'_Q': "Normal s ∈ Normal ` P' ⟶
t ∈ Normal ` Q' ∪ Abrupt ` A'"
by (unfold cvalidt_def validt_def valid_def) blast
hence "s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'"
by blast
with weaken
show ?thesis
by blast
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
show "Γ⊢c ↓ Normal s"
proof -
from P adapt
obtain P' and Q' and A' where
"Γ,Θ ⊨⇩t⇘/F⇙ P' c Q',A'"
"s ∈ P'"
by blast
with ctxt
show ?thesis
by (simp add: cvalidt_def validt_def)
qed
qed
next
case (Asm P p Q A Θ F)
assume "(P, p, Q, A) ∈ Θ"
then show "Γ,Θ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
by (auto simp add: cvalidt_def )
next
case ExFalso thus ?case by iprover
qed
lemma hoaret_sound':
"Γ,{}⊢⇩t⇘/F⇙ P c Q,A ⟹ Γ⊨⇩t⇘/F⇙ P c Q,A"
apply (drule hoaret_sound)
apply (simp add: cvalidt_def)
done
theorem total_to_partial:
assumes total: "Γ,{}⊢⇩t⇘/F⇙ P c Q,A" shows "Γ,{}⊢⇘/F⇙ P c Q,A"
proof -
from total have "Γ,{}⊨⇩t⇘/F⇙ P c Q,A"
by (rule hoaret_sound)
hence "Γ⊨⇘/F⇙ P c Q,A"
by (simp add: cvalidt_def validt_def cvalid_def)
thus ?thesis
by (rule hoare_complete)
qed
subsection {* Completeness *}
lemma MGT_valid:
"Γ⊨⇩t⇘/F ⇙{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢c↓Normal s} c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t}, {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule validtI)
fix s t
assume "Γ⊢⟨c,Normal s⟩ ⇒ t"
"s ∈ {s. s = Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢c↓Normal s}"
"t ∉ Fault ` F"
thus "t ∈ Normal ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t} ∪
Abrupt ` {t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
apply (cases t)
apply (auto simp add: final_notin_def)
done
next
fix s
assume "s ∈ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢c↓Normal s}"
thus "Γ⊢c↓Normal s"
by blast
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::'a. Γ,Θ ⊢⇩t⇘/F⇙ (P' Z::'a assn) 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 "Γ,Θ ⊢⇩t⇘/F⇙ P c Q,A"
using impl
by - (rule conseq [OF modif],blast)
lemma MGT_implies_complete:
assumes MGT: "∀Z. Γ,{}⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c↓Normal s}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
assumes valid: "Γ ⊨⇩t⇘/F⇙ P c Q,A"
shows "Γ,{} ⊢⇩t⇘/F⇙ P c Q,A"
using MGT
apply (rule ConseqMGT)
apply (insert valid)
apply (auto simp add: validt_def valid_def intro!: final_notinI)
done
lemma conseq_extract_state_indep_prop:
assumes state_indep_prop:"∀s ∈ P. R"
assumes to_show: "R ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/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. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Call p)↓Normal s}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
shows "⋀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c↓Normal s}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (induct c)
case Skip
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Skip,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Skip ↓ Normal s}
Skip
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Skip [THEN conseqPre])
(auto elim: exec_elim_cases simp add: final_notin_def
intro: exec.intros terminates.intros)
next
case (Basic f)
show "Γ,Θ⊢⇩t⇘/F ⇙{s. s=Z ∧ Γ⊢⟨Basic f,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Basic f ↓ Normal s}
Basic f
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Basic [THEN conseqPre])
(auto elim: exec_elim_cases simp add: final_notin_def
intro: exec.intros terminates.intros)
next
case (Spec r)
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Spec r,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Spec r ↓ Normal s}
Spec r
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoaret.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. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c1↓Normal s}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
have hyp_c2: "∀ Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c2↓Normal s}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
from hyp_c1
have "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Seq c1 c2↓Normal s} c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧ Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c2↓Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
elim: terminates_Normal_elim_cases
intro: exec.intros)
thus "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Seq c1 c2↓Normal s}
Seq c1 c2
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule hoaret.Seq )
show "Γ,Θ⊢⇩t⇘/F⇙ {t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢c2 ↓ Normal t}
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 (rule 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 (rule exec.intros)
qed
qed
next
case (Cond b c1 c2)
have "∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c1↓Normal s}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
hence "Γ,Θ ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Cond b c1 c2)↓Normal s}∩b)
c1
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(fastforce simp add: final_notin_def intro: exec.CondTrue
elim: terminates_Normal_elim_cases)
moreover
have "∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c2↓Normal s}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
hence "Γ,Θ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Cond b c1 c2)↓Normal s}∩-b)
c2
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT)
(fastforce simp add: final_notin_def intro: exec.CondFalse
elim: terminates_Normal_elim_cases)
ultimately
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Cond b c1 c2)↓Normal s}
(Cond b c1 c2)
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.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)) ∧
Γ⊢(While b c)↓Normal t}"
let ?A = "λZ. {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
let ?r = "{(t,s). Γ⊢(While b c)↓Normal s ∧ s∈b ∧
Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(While b c)↓Normal s}
(While b c)
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z"
and ?Q'="λ Z. ?P' Z ∩ - b"])
have wf_r: "wf ?r" by (rule wf_terminates_while)
show "∀ Z. Γ,Θ⊢⇩t⇘/F⇙ (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)"
proof (rule allI, rule hoaret.While [OF wf_r])
fix Z
from While
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c↓Normal s}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}" by iprover
show "∀σ. Γ,Θ⊢⇩t⇘/F⇙ ({σ} ∩ ?P' Z ∩ b) c
({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)"
proof (rule allI, rule ConseqMGT [OF hyp_c])
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)) ∧
Γ⊢(While b c)↓Normal t}
∩ b"
then obtain
s_eq_σ: "s=σ" and
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
while_term: "Γ⊢(While b c)↓Normal s" and
s_in_b: "s∈b"
by blast
show "s ∈ {t. t = s ∧ Γ⊢⟨c,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c↓Normal t} ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Normal t} ⟶
t ∈ {t. (t,σ) ∈ ?r} ∩
{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)) ∧
Γ⊢(While b c)↓Normal t}) ∧
(∀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 while_term show ?C1
by (blast elim: terminates_Normal_elim_cases)
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Normal t"
with s_eq_σ while_term s_in_b have "(t,σ) ∈ ?r"
by blast
moreover
from Z_s_unroll s_t s_in_b
have "(Z, t) ∈ ?unroll"
by (blast intro: rtrancl_into_rtrancl)
moreover from while_term s_t s_in_b
have "Γ⊢(While b c)↓Normal t"
by (blast elim: terminates_Normal_elim_cases)
moreover note noabort
ultimately
have "(t,σ) ∈ ?r ∧ (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)) ∧
Γ⊢(While b c)↓Normal t"
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)) ∧
Γ⊢While b c ↓ Normal s}"
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)
from noStuck_Call
have "∀s ∈ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓ Normal s}.
p ∈ dom Γ"
by (fastforce simp add: final_notin_def)
then show ?case
proof (rule conseq_extract_state_indep_prop)
assume p_defined: "p ∈ dom Γ"
with MGT_Calls show
"Γ,Θ⊢⇩t⇘/F ⇙{s. s=Z ∧
Γ⊢⟨Call p ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))∧
Γ⊢Call p↓Normal s}
(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. Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨c s',Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c s'↓Normal s} c s'
{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Abrupt t}"
using DynCom by simp
have hyp':
"Γ,Θ⊢⇩t⇘/F ⇙{s. s = Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢DynCom c↓Normal s}
(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
elim: terminates_Normal_elim_cases)
show "Γ,Θ⊢⇩t⇘/F ⇙{s. s=Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢DynCom c↓Normal s}
DynCom c
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoaret.DynCom)
apply (clarsimp)
apply (rule hyp' [simplified])
done
next
case (Guard f g c)
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c↓Normal s}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
using Guard by iprover
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Guard f g c↓ Normal s}
Guard f g c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c,Normal Z⟩ ⇒ Abrupt t}"
proof (cases "f ∈ F")
case True
from hyp_c
have "Γ,Θ⊢⇩t⇘/F ⇙(g ∩ {s. s=Z ∧
Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck}∪ Fault ` (-F))∧
Γ⊢Guard f g c↓ Normal s})
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
elim: terminates_Normal_elim_cases)
done
from True this
show ?thesis
by (rule conseqPre [OF Guarantee]) auto
next
case False
from hyp_c
have "Γ,Θ⊢⇩t⇘/F ⇙(g ∩ {s. s ∈ g ∧ s=Z ∧
Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck}∪ Fault ` (-F))∧
Γ⊢Guard f g c↓ Normal s} )
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
elim: terminates_Normal_elim_cases)
done
then show ?thesis
apply (rule conseqPre [OF hoaret.Guard])
apply clarify
apply (frule Guard_noFaultStuckD [OF _ False])
apply auto
done
qed
next
case Throw
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Throw,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Throw ↓ Normal s}
Throw
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Abrupt t}"
by (rule conseqPre [OF hoaret.Throw])
(blast intro: exec.intros terminates.intros)
next
case (Catch c⇩1 c⇩2)
have "∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨c⇩1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c⇩1 ↓ Normal s}
c⇩1
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
hence "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Catch c⇩1 c⇩2 ↓ Normal s}
c⇩1
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧ Γ⊢c⇩2 ↓ Normal t ∧
Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))}"
by (rule ConseqMGT)
(fastforce intro: exec.intros terminates.intros
elim: terminates_Normal_elim_cases
simp add: final_notin_def)
moreover
have
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢c⇩2 ↓ Normal s} c⇩2
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
hence "Γ,Θ⊢⇩t⇘/F⇙ {s. Γ⊢⟨c⇩1,Normal Z⟩ ⇒Abrupt s ∧ Γ⊢c⇩2 ↓ Normal s ∧
Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({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 terminates.intros
simp add: noFault_def')
ultimately
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Catch c⇩1 c⇩2 ↓ Normal s}
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 hoaret.Catch )
qed
lemma Call_lemma':
assumes Call_hyp:
"∀q∈dom Γ. ∀Z. Γ,Θ⊢⇩t⇘/F⇙{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c ∈ redexes c')}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (induct c)
case Skip
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Skip,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ Skip ∈ redexes c')}
Skip
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip)
next
case (Basic f)
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Basic f,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Basic f ∈ redexes c')}
Basic f
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic)
next
case (Spec r)
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Spec r,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Spec r ∈ redexes c')}
Spec r
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoaret.Spec [THEN conseqPre])
apply (clarsimp)
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. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c1 ∈ redexes c')}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c2 ∈ redexes c')}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps (2) by iprover
have c1: "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Seq c1 c2 ∈ redexes c')}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal t) ∧
c2 ∈ redexes c')},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
assume "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (blast dest: Seq_NoFaultStuckD1)
next
fix c'
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume red: "Seq c1 c2 ∈ redexes c'"
from redexes_subset [OF red] steps_c'
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c1 ∈ redexes c'"
by (auto iff: root_in_redexes)
next
fix t
assume "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (blast dest: Seq_NoFaultStuckD2)
next
fix c' t
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume red: "Seq c1 c2 ∈ redexes c'"
assume exec_c1: "Γ⊢ ⟨c1,Normal Z⟩ ⇒ Normal t"
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal t) ∧ c2 ∈ redexes c'"
proof -
note steps_c'
also
from exec_impl_steps_Normal [OF exec_c1]
have "Γ⊢ (c1, Normal Z) →⇧* (Skip, Normal t)".
from steps_redexes_Seq [OF this red]
obtain c'' where
steps_c'': "Γ⊢ (c', Normal Z) →⇧* (c'', Normal t)" and
Skip: "Seq Skip c2 ∈ redexes c''"
by blast
note steps_c''
also
have step_Skip: "Γ⊢ (Seq Skip c2,Normal t) → (c2,Normal t)"
by (rule step.SeqSkip)
from step_redexes [OF step_Skip Skip]
obtain c''' where
step_c''': "Γ⊢ (c'', Normal t) → (c''', Normal t)" and
c2: "c2 ∈ redexes c'''"
by blast
note step_c'''
finally show ?thesis
using c2
by blast
qed
next
fix t
assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.intros)
qed
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ Seq c1 c2 ∈ redexes c')}
Seq c1 c2
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]])
(blast intro: exec.intros)
next
case (Cond b c1 c2)
have hyp_c1:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c1 ∈ redexes c')}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Cond b c1 c2 ∈ redexes c')}
∩ b)
c1
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c1],safe)
assume "Z ∈ b" "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.CondTrue)
next
fix c'
assume b: "Z ∈ b"
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume redex_c': "Cond b c1 c2 ∈ redexes c'"
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c1 ∈ redexes c'"
proof -
note steps_c'
also
from b
have "Γ⊢(Cond b c1 c2, Normal Z) → (c1, Normal Z)"
by (rule step.CondTrue)
from step_redexes [OF this redex_c'] obtain c'' where
step_c'': "Γ⊢ (c', Normal Z) → (c'', Normal Z)" and
c1: "c1 ∈ redexes c''"
by blast
note step_c''
finally show ?thesis
using c1
by blast
qed
next
fix t assume "Z ∈ b" "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t"
by (blast intro: exec.CondTrue)
next
fix t assume "Z ∈ b" "Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.CondTrue)
qed
moreover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c2 ∈ redexes c')}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c', Normal s) ∧
Cond b c1 c2 ∈ redexes c')}
∩ -b)
c2
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c2],safe)
assume "Z ∉ b" "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.CondFalse)
next
fix c'
assume b: "Z ∉ b"
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume redex_c': "Cond b c1 c2 ∈ redexes c'"
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c2 ∈ redexes c'"
proof -
note steps_c'
also
from b
have "Γ⊢(Cond b c1 c2, Normal Z) → (c2, Normal Z)"
by (rule step.CondFalse)
from step_redexes [OF this redex_c'] obtain c'' where
step_c'': "Γ⊢ (c', Normal Z) → (c'', Normal Z)" and
c1: "c2 ∈ redexes c''"
by blast
note step_c''
finally show ?thesis
using c1
by blast
qed
next
fix t assume "Z ∉ b" "Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t"
by (blast intro: exec.CondFalse)
next
fix t assume "Z ∉ b" "Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.CondFalse)
qed
ultimately
show
"Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Cond b c1 c2 ∈ redexes c')}
(Cond b c1 c2)
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.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)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+
(c',Normal t) ∧ While b c ∈ redexes c')}"
let ?A = "λZ. {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
let ?r = "{(t,s). Γ⊢(While b c)↓Normal s ∧ s∈b ∧
Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
show "Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ)→⇧+(c',Normal s) ∧ While b c ∈ redexes c')}
(While b c)
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z"
and ?Q'="λ Z. ?P' Z ∩ - b"])
have wf_r: "wf ?r" by (rule wf_terminates_while)
show "∀ Z. Γ,Θ⊢⇩t⇘/F⇙ (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)"
proof (rule allI, rule hoaret.While [OF wf_r])
fix Z
from While
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c ∈ redexes c')}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}" by iprover
show "∀σ. Γ,Θ⊢⇩t⇘/F⇙ ({σ} ∩ ?P' Z ∩ b) c
({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)"
proof (rule allI, rule ConseqMGT [OF hyp_c])
fix τ s
assume asm: "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)) ∧
Γ⊢Call p↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+
(c',Normal t) ∧ While b c ∈ redexes c')}
∩ b"
then obtain c' where
s_eq_τ: "s=τ" and
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
termi: "Γ⊢Call p ↓ Normal σ" and
reach: "Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s)" and
red_c': "While b c ∈ redexes c'" and
s_in_b: "s∈b"
by blast
obtain c'' where
reach_c: "Γ⊢(Call p,Normal σ) →⇧+ (c'',Normal s)"
"Seq c (While b c) ∈ redexes c''"
proof -
note reach
also from s_in_b
have "Γ⊢(While b c,Normal s) → (Seq c (While b c),Normal s)"
by (rule step.WhileTrue)
from step_redexes [OF this red_c'] obtain c'' where
step: "Γ⊢ (c', Normal s) → (c'', Normal s)" and
red_c'': "Seq c (While b c) ∈ redexes c''"
by blast
note step
finally
show ?thesis
using red_c''
by (blast intro: that)
qed
from reach termi
have "Γ⊢c' ↓ Normal s"
by (rule steps_preserves_termination')
from redexes_preserves_termination [OF this red_c']
have termi_while: "Γ⊢While b c ↓ Normal s" .
show "s ∈ {t. t = s ∧ Γ⊢⟨c,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal t) ∧ c ∈ redexes c')} ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Normal t} ⟶
t ∈ {t. (t,τ) ∈ ?r} ∩
{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)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal t) ∧
While b c ∈ redexes c')}) ∧
(∀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 termi reach_c show ?C1
apply clarsimp
apply (drule redexes_subset)
apply simp
apply (blast intro: root_in_redexes)
done
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Normal t"
with s_eq_τ termi_while s_in_b have "(t,τ) ∈ ?r"
by blast
moreover
from Z_s_unroll s_t s_in_b
have "(Z, t) ∈ ?unroll"
by (blast intro: rtrancl_into_rtrancl)
moreover
obtain c'' where
reach_c'': "Γ⊢(Call p,Normal σ) →⇧+ (c'',Normal t)"
"(While b c) ∈ redexes c''"
proof -
note reach_c (1)
also from s_in_b
have "Γ⊢(While b c,Normal s)→ (Seq c (While b c),Normal s)"
by (rule step.WhileTrue)
have "Γ⊢ (Seq c (While b c), Normal s) →⇧+
(While b c, Normal t)"
proof -
from exec_impl_steps_Normal [OF s_t]
have "Γ⊢ (c, Normal s) →⇧* (Skip, Normal t)".
hence "Γ⊢ (Seq c (While b c), Normal s) →⇧*
(Seq Skip (While b c), Normal t)"
by (rule SeqSteps) auto
moreover
have "Γ⊢(Seq Skip (While b c), Normal t)→(While b c, Normal t)"
by (rule step.SeqSkip)
ultimately show ?thesis by (rule rtranclp_into_tranclp1)
qed
from steps_redexes' [OF this reach_c (2)]
obtain c''' where
step: "Γ⊢ (c'', Normal s) →⇧+ (c''', Normal t)" and
red_c'': "While b c ∈ redexes c'''"
by blast
note step
finally
show ?thesis
using red_c''
by (blast intro: that)
qed
moreover note noabort termi
ultimately
have "(t,τ) ∈ ?r ∧ (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)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c', Normal t) ∧
While b c ∈ redexes c')"
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)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
While b c ∈ redexes c')}"
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 q)
let ?P = "{s. s=Z ∧ Γ⊢⟨Call q ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ Call q ∈ redexes c')}"
from noStuck_Call
have "∀s ∈ ?P. q ∈ dom Γ"
by (fastforce simp add: final_notin_def)
then show ?case
proof (rule conseq_extract_state_indep_prop)
assume q_defined: "q ∈ dom Γ"
from Call_hyp have
"∀q∈dom Γ. ∀Z.
Γ,Θ⊢⇩t⇘/F⇙{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified]
terminates_Normal_Call_body)
from Call_hyp q_defined have Call_hyp':
"∀Z. Γ,Θ ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
by auto
show
"Γ,Θ⊢⇩t⇘/F⇙ ?P
(Call q)
{t. Γ⊢⟨Call q ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF Call_hyp'],safe)
fix c'
assume termi: "Γ⊢Call p ↓ Normal σ"
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume red_c': "Call q ∈ redexes c'"
show "Γ⊢Call q ↓ Normal Z"
proof -
from steps_preserves_termination' [OF steps_c' termi]
have "Γ⊢c' ↓ Normal Z" .
from redexes_preserves_termination [OF this red_c']
show ?thesis .
qed
next
fix c'
assume termi: "Γ⊢Call p ↓ Normal σ"
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume red_c': "Call q ∈ redexes c'"
from redex_redexes [OF this]
have "redex c' = Call q"
by auto
with termi steps_c'
show "((Z, q), σ, p) ∈ termi_call_steps Γ"
by (auto simp add: termi_call_steps_def)
qed
qed
next
case (DynCom c)
have hyp:
"⋀s'. ∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s = Z ∧ Γ⊢⟨c s',Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c s' ∈ redexes c')}
(c s')
{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Abrupt t}"
using DynCom by simp
have hyp':
"Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ DynCom c ∈ redexes c')}
(c Z)
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp],safe)
assume "Γ⊢⟨DynCom c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
then show "Γ⊢⟨c Z,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (fastforce simp add: final_notin_def intro: exec.intros)
next
fix c'
assume steps: "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume c': "DynCom c ∈ redexes c'"
have "Γ⊢ (DynCom c, Normal Z) → (c Z,Normal Z)"
by (rule step.DynCom)
from step_redexes [OF this c'] obtain c'' where
step: "Γ⊢ (c', Normal Z) → (c'', Normal Z)" and c'': "c Z ∈ redexes c''"
by blast
note steps also note step
finally show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c Z ∈ redexes c'"
using c'' by blast
next
fix t
assume "Γ⊢⟨c Z,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t"
by (auto intro: exec.intros)
next
fix t
assume "Γ⊢⟨c Z,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t"
by (auto intro: exec.intros)
qed
show ?case
apply (rule hoaret.DynCom)
apply safe
apply (rule hyp')
done
next
case (Guard f g c)
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c ∈ redexes c')}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
using Guard.hyps by iprover
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ Guard f g c ∈ redexes c')}
Guard f g c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (cases "f ∈ F")
case True
have "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ {s. s=Z ∧
Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Guard f g c ∈ redexes c')})
c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c], safe)
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))" "Z∈g"
thus "Γ⊢⟨c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
next
fix c'
assume steps: "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume c': "Guard f g c ∈ redexes c'"
assume "Z ∈ g"
from this have "Γ⊢(Guard f g c,Normal Z) → (c,Normal Z)"
by (rule step.Guard)
from step_redexes [OF this c'] obtain c'' where
step: "Γ⊢ (c', Normal Z) → (c'', Normal Z)" and c'': "c ∈ redexes c''"
by blast
note steps also note step
finally show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c ∈ redexes c'"
using c'' by blast
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Normal t" "Z ∈ g"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t"
by (auto simp add: final_notin_def intro: exec.intros )
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t" "Z ∈ g"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t"
by (auto simp add: final_notin_def intro: exec.intros )
qed
from True this show ?thesis
by (rule conseqPre [OF Guarantee]) auto
next
case False
have "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ {s. s=Z ∧
Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
Guard f g c ∈ redexes c')})
c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c], safe)
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros)
next
fix c'
assume steps: "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume c': "Guard f g c ∈ redexes c'"
assume "Z ∈ g"
from this have "Γ⊢(Guard f g c,Normal Z) → (c,Normal Z)"
by (rule step.Guard)
from step_redexes [OF this c'] obtain c'' where
step: "Γ⊢ (c', Normal Z) → (c'', Normal Z)" and c'': "c ∈ redexes c''"
by blast
note steps also note step
finally show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c ∈ redexes c'"
using c'' by blast
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
qed
then show ?thesis
apply (rule conseqPre [OF hoaret.Guard])
apply clarify
apply (frule Guard_noFaultStuckD [OF _ False])
apply auto
done
qed
next
case Throw
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Throw,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal σ ∧
(∃c'. Γ⊢(Call p, Normal σ) →⇧+ (c',Normal s) ∧ Throw ∈ redexes c')}
Throw
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Abrupt t}"
by (rule conseqPre [OF hoaret.Throw])
(blast intro: exec.intros terminates.intros)
next
case (Catch c⇩1 c⇩2)
have hyp_c1:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s= Z ∧ Γ⊢⟨c⇩1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧
c⇩1 ∈ redexes c')}
c⇩1
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s= Z ∧ Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal s) ∧ c⇩2 ∈ redexes c')}
c⇩2
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ)→⇧+(c',Normal s) ∧
Catch c⇩1 c⇩2 ∈ redexes c')}
c⇩1
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault`(-F)) ∧ Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal t) ∧ c⇩2 ∈ redexes c')}"
proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
assume "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c⇩1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (fastforce simp add: final_notin_def intro: exec.intros)
next
fix c'
assume steps: "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume c': "Catch c⇩1 c⇩2 ∈ redexes c'"
from steps redexes_subset [OF this]
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z) ∧ c⇩1 ∈ redexes c'"
by (auto iff: root_in_redexes)
next
fix t
assume "Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t"
by (auto intro: exec.intros)
next
fix t
assume "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
next
fix c' t
assume steps_c': "Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal Z)"
assume red: "Catch c⇩1 c⇩2 ∈ redexes c'"
assume exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal Z⟩ ⇒ Abrupt t"
show "∃c'. Γ⊢ (Call p, Normal σ) →⇧+ (c', Normal t) ∧ c⇩2 ∈ redexes c'"
proof -
note steps_c'
also
from exec_impl_steps_Normal_Abrupt [OF exec_c⇩1]
have "Γ⊢ (c⇩1, Normal Z) →⇧* (Throw, Normal t)".
from steps_redexes_Catch [OF this red]
obtain c'' where
steps_c'': "Γ⊢ (c', Normal Z) →⇧* (c'', Normal t)" and
Catch: "Catch Throw c⇩2 ∈ redexes c''"
by blast
note steps_c''
also
have step_Catch: "Γ⊢ (Catch Throw c⇩2,Normal t) → (c⇩2,Normal t)"
by (rule step.CatchThrow)
from step_redexes [OF step_Catch Catch]
obtain c''' where
step_c''': "Γ⊢ (c'', Normal t) → (c''', Normal t)" and
c2: "c⇩2 ∈ redexes c'''"
by blast
note step_c'''
finally show ?thesis
using c2
by blast
qed
qed
moreover
have "Γ,Θ⊢⇩t⇘/F⇙ {t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p ↓ Normal σ ∧
(∃c'. Γ⊢(Call p,Normal σ) →⇧+ (c',Normal t) ∧ c⇩2 ∈ redexes c')}
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 [OF hyp_c2]) (fastforce intro: exec.intros)
ultimately show ?case
by (rule hoaret.Catch)
qed
text {* To prove a procedure implementation correct it suffices to assume
only the procedure specifications of procedures that actually
occur during evaluation of the body.
*}
lemma Call_lemma:
assumes A:
"∀q ∈ dom Γ. ∀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
assumes pdef: "p ∈ dom Γ"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
({σ} ∩ {s. s=Z ∧Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal s})
the (Γ p)
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
apply (rule conseqPre)
apply (rule Call_lemma' [OF A])
using pdef
apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step Γ)", OF step.Call] root_in_redexes)
done
lemma Call_lemma_switch_Call_body:
assumes
call: "∀q ∈ dom Γ. ∀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
assumes p_defined: "p ∈ dom Γ"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
({σ} ∩ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s})
the (Γ p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined])
apply (rule conseqPre)
apply (rule Call_lemma')
apply (rule call)
using p_defined
apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step Γ)", OF step.Call]
root_in_redexes)
done
lemma MGT_Call:
"∀p ∈ dom Γ. ∀Z.
Γ,Θ ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Call p)↓Normal s}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
apply (intro ballI allI)
apply (rule CallRec' [where Procs="dom Γ" and
P="λp Z. {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s}" and
Q="λp Z. {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t}" and
A="λp Z. {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}" and
r="termi_call_steps Γ"
])
apply simp
apply simp
apply (rule wf_termi_call_steps)
apply (intro ballI allI)
apply simp
apply (rule Call_lemma_switch_Call_body [rule_format, simplified])
apply (rule hoaret.Asm)
apply fastforce
apply assumption
done
lemma CollInt_iff: "{s. P s} ∩ {s. Q s} = {s. P s ∧ Q s}"
by auto
lemma image_Un_conv: "f ` (⋃p∈dom Γ. ⋃Z. {x p Z}) = (⋃p∈dom Γ. ⋃Z. {f (x p Z)})"
by (auto iff: not_None_eq)
text {* Another proof of @{text MGT_Call}, maybe a little more readable *}
lemma
"∀p ∈ dom Γ. ∀Z.
Γ,{} ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Call p)↓Normal s}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
proof -
{
fix p Z σ
assume defined: "p ∈ dom Γ"
define Specs where "Specs = (⋃p∈dom Γ. ⋃Z.
{({s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s},
p,
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})"
define Specs_wf where "Specs_wf p σ = (λ(P,q,Q,A).
(P ∩ {s. ((s,q),σ,p) ∈ termi_call_steps Γ}, q, Q, A)) ` Specs" for p σ
have "Γ,Specs_wf p σ
⊢⇩t⇘/F⇙({σ} ∩
{s. s = Z ∧ Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal s})
(the (Γ p))
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
apply (rule Call_lemma [rule_format, OF _ defined])
apply (rule hoaret.Asm)
apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv)
apply (rule_tac x=q in bexI)
apply (rule_tac x=Z in exI)
apply (clarsimp simp add: CollInt_iff)
apply auto
done
hence "Γ,Specs_wf p σ
⊢⇩t⇘/F⇙({σ} ∩
{s. s = Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s})
(the (Γ p))
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
by (simp only: exec_Call_body' [OF defined]
noFaultStuck_Call_body' [OF defined]
terminates_Normal_Call_body [OF defined])
} note bdy=this
show ?thesis
apply (intro ballI allI)
apply (rule hoaret.CallRec [where Specs="(⋃p∈dom Γ. ⋃Z.
{({s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s},
p,
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})",
OF _ wf_termi_call_steps [of Γ] refl])
apply fastforce
apply clarify
apply (rule conjI)
apply fastforce
apply (rule allI)
apply (simp (no_asm_use) only : Un_empty_left)
apply (rule bdy)
apply auto
done
qed
theorem hoaret_complete: "Γ⊨⇩t⇘/F⇙ P c Q,A ⟹ Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call])
lemma hoaret_complete':
assumes cvalid: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
proof (cases "Γ⊨⇩t⇘/F⇙ P c Q,A")
case True
hence "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
by (rule hoaret_complete)
thus "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule hoaret_augment_context) simp
next
case False
with cvalid
show ?thesis
by (rule ExFalso)
qed
subsection {* And Now: Some Useful Rules *}
subsubsection {* Modify Return *}
lemma ProcModifyReturn_sound:
assumes valid_call: "Γ,Θ ⊨⇩t⇘/F⇙ P call init p return' c Q,A"
assumes valid_modif:
"∀σ. Γ,Θ ⊨⇘/UNIV⇙ {σ} (Call p) (Modif σ),(ModifAbr σ)"
assumes res_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 "Γ,Θ ⊨⇩t⇘/F⇙ P (call init p return c) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults)
assume exec: "Γ⊢⟨call init p return c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: exec_call_Normal_elim)
fix bdy t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ ⇒ t"
from exec_body bdy
have "Γ⊢⟨(Call p ),Normal (init s)⟩ ⇒ Normal t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
have "t' ∈ Modif (init s)"
by auto
with res_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy
have "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_call)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Abrupt t'"
assume t: "t = Abrupt (return s t')"
also from exec_body bdy
have "Γ⊢⟨(Call p),Normal (init s)⟩ ⇒ Abrupt t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "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
have "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callAbrupt)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy f
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Fault f" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callFault)
from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Stuck"
"t = Stuck"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callStuck)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
assume "Γ p = None" "t=Stuck"
hence "Γ⊢⟨call init p return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callUndefined)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults)
assume P: "s ∈ P"
from valid_call ctxt P
have call: "Γ⊢call init p return' c↓ Normal s"
by (rule cvalidt_termD)
show "Γ⊢call init p return c ↓ Normal s"
proof (cases "p ∈ dom Γ")
case True
with call obtain bdy where
bdy: "Γ p = Some bdy" and termi_bdy: "Γ⊢bdy ↓ Normal (init s)" and
termi_c: "∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶
Γ⊢c s t ↓ Normal (return' s t)"
by cases auto
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t"
hence "Γ⊢c s t ↓ Normal (return s t)"
proof -
from exec_bdy bdy
have "Γ⊢⟨(Call p ),Normal (init s)⟩ ⇒ Normal t"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
res_modif
have "return' s t = return s t"
by auto
with termi_c exec_bdy show ?thesis by auto
qed
}
with bdy termi_bdy
show ?thesis
by (iprover intro: terminates_call)
next
case False
thus ?thesis
by (auto intro: terminates_callUndefined)
qed
qed
lemma ProcModifyReturn:
assumes spec: "Γ,Θ⊢⇩t⇘/F⇙ P (call init p return' c) Q,A"
assumes res_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 modifies_spec:
"∀σ. Γ,Θ⊢⇘/UNIV⇙ {σ} (Call p) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇩t⇘/F⇙ P (call init p return c) Q,A"
apply (rule hoaret_complete')
apply (rule ProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ res_modif ret_modifAbr])
apply (rule hoaret_sound [OF spec])
using modifies_spec
apply (blast intro: hoare_sound)
done
lemma ProcModifyReturnSameFaults_sound:
assumes valid_call: "Γ,Θ ⊨⇩t⇘/F⇙ P call init p return' c Q,A"
assumes valid_modif:
"∀σ. Γ,Θ ⊨⇘/F⇙ {σ} Call p (Modif σ),(ModifAbr σ)"
assumes res_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 "Γ,Θ ⊨⇩t⇘/F⇙ P (call init p return c) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
assume exec: "Γ⊢⟨call init p return c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from exec
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: exec_call_Normal_elim)
fix bdy t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ ⇒ t"
from exec_body bdy
have "Γ⊢⟨(Call p) ,Normal (init s)⟩ ⇒ Normal t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
have "t' ∈ Modif (init s)"
by auto
with res_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy
have "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_call)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy t'
assume bdy: "Γ p = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Abrupt t'"
assume t: "t = Abrupt (return s t')"
also
from exec_body bdy
have "Γ⊢⟨Call p ,Normal (init s)⟩ ⇒ Abrupt t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "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
have "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callAbrupt)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy f
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Fault f" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init p return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callFault)
from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy
assume bdy: "Γ p = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Stuck"
"t = Stuck"
with bdy have "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callStuck)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
assume "Γ p = None" "t=Stuck"
hence "Γ⊢⟨call init p return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callUndefined)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
assume P: "s ∈ P"
from valid_call ctxt P
have call: "Γ⊢call init p return' c↓ Normal s"
by (rule cvalidt_termD)
show "Γ⊢call init p return c ↓ Normal s"
proof (cases "p ∈ dom Γ")
case True
with call obtain bdy where
bdy: "Γ p = Some bdy" and termi_bdy: "Γ⊢bdy ↓ Normal (init s)" and
termi_c: "∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶
Γ⊢c s t ↓ Normal (return' s t)"
by cases auto
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t"
hence "Γ⊢c s t ↓ Normal (return s t)"
proof -
from exec_bdy bdy
have "Γ⊢⟨(Call p ),Normal (init s)⟩ ⇒ Normal t"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
res_modif
have "return' s t = return s t"
by auto
with termi_c exec_bdy show ?thesis by auto
qed
}
with bdy termi_bdy
show ?thesis
by (iprover intro: terminates_call)
next
case False
thus ?thesis
by (auto intro: terminates_callUndefined)
qed
qed
lemma ProcModifyReturnSameFaults:
assumes spec: "Γ,Θ⊢⇩t⇘/F⇙ P (call init p return' c) Q,A"
assumes res_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 modifies_spec:
"∀σ. Γ,Θ⊢⇘/F⇙ {σ} (Call p) (Modif σ),(ModifAbr σ)"
shows "Γ,Θ⊢⇩t⇘/F⇙ P (call init p return c) Q,A"
apply (rule hoaret_complete')
apply (rule ProcModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ res_modif ret_modifAbr])
apply (rule hoaret_sound [OF spec])
using modifies_spec
apply (blast intro: hoare_sound)
done
subsubsection {* DynCall *}
lemma dynProcModifyReturn_sound:
assumes valid_call: "Γ,Θ ⊨⇩t⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
"∀s∈P. ∀σ. Γ,Θ ⊨⇘/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 "Γ,Θ ⊨⇩t⇘/F⇙ P (dynCall init p return c) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults)
assume exec: "Γ⊢⟨dynCall init p return c,Normal s⟩ ⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P: "s ∈ P"
with valid_modif
have valid_modif':
"∀σ. Γ,Θ⊨⇘/UNIV⇙ {σ} (Call (p s)) (Modif σ),(ModifAbr σ)"
by blast
from exec
have "Γ⊢⟨call init (p s) return c,Normal s⟩ ⇒ t"
by (cases rule: exec_dynCall_Normal_elim)
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: exec_call_Normal_elim)
fix bdy t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ ⇒ t"
from exec_body bdy
have "Γ⊢⟨Call (p s),Normal (init s)⟩ ⇒ Normal t'"
by (auto simp add: intro: exec.Call)
from cvalidD [OF valid_modif' [rule_format, of "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
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_call)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Abrupt t'"
assume t: "t = Abrupt (return s t')"
also from exec_body bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ ⇒ Abrupt t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif' [rule_format, of "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
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callAbrupt)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy f
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Fault f" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callFault)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by blast
next
fix bdy
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Stuck"
"t = Stuck"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callStuck)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
fix bdy
assume "Γ (p s) = None" "t=Stuck"
hence "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callUndefined)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
then have ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/UNIV⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults)
assume P: "s ∈ P"
from valid_call ctxt P
have "Γ⊢dynCall init p return' c↓ Normal s"
by (rule cvalidt_termD)
hence call: "Γ⊢call init (p s) return' c↓ Normal s"
by cases
have "Γ⊢call init (p s) return c ↓ Normal s"
proof (cases "p s ∈ dom Γ")
case True
with call obtain bdy where
bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊢bdy ↓ Normal (init s)" and
termi_c: "∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶
Γ⊢c s t ↓ Normal (return' s t)"
by cases auto
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t"
hence "Γ⊢c s t ↓ Normal (return s t)"
proof -
from exec_bdy bdy
have "Γ⊢⟨Call (p s),Normal (init s)⟩ ⇒ Normal t"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
ret_modif
have "return' s t = return s t"
by auto
with termi_c exec_bdy show ?thesis by auto
qed
}
with bdy termi_bdy
show ?thesis
by (iprover intro: terminates_call)
next
case False
thus ?thesis
by (auto intro: terminates_callUndefined)
qed
thus "Γ⊢dynCall init p return c ↓ Normal s"
by (iprover intro: terminates_dynCall)
qed
lemma dynProcModifyReturn:
assumes dyn_call: "Γ,Θ⊢⇩t⇘/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 "Γ,Θ ⊢⇩t⇘/F⇙ P (dynCall init p return c) Q,A"
apply (rule hoaret_complete')
apply (rule dynProcModifyReturn_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_sound [OF modif [rule_format]])
apply assumption
done
lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "Γ,Θ ⊨⇩t⇘/F⇙ P dynCall init p return' c Q,A"
assumes valid_modif:
"∀s∈P. ∀σ. Γ,Θ ⊨⇘/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 "Γ,Θ ⊨⇩t⇘/F⇙ P (dynCall init p return c) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
assume exec: "Γ⊢⟨dynCall init p return c,Normal s⟩ ⇒ t"
assume t_notin_F: "t ∉ Fault ` F"
assume P: "s ∈ P"
with valid_modif
have valid_modif':
"∀σ. Γ,Θ⊨⇘/F⇙ {σ} (Call (p s)) (Modif σ),(ModifAbr σ)"
by blast
from exec
have "Γ⊢⟨call init (p s) return c,Normal s⟩ ⇒ t"
by (cases rule: exec_dynCall_Normal_elim)
then show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases rule: exec_call_Normal_elim)
fix bdy t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t'"
assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ ⇒ t"
from exec_body bdy
have "Γ⊢⟨Call (p s),Normal (init s)⟩ ⇒ Normal t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif' [rule_format, of "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
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_call)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy t'
assume bdy: "Γ (p s) = Some bdy"
assume exec_body: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Abrupt t'"
assume t: "t = Abrupt (return s t')"
also from exec_body bdy
have "Γ⊢⟨Call (p s) ,Normal (init s)⟩ ⇒ Abrupt t'"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif' [rule_format, of "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
have "Γ⊢⟨call init (p s) return' c,Normal s⟩ ⇒ t"
by (auto intro: exec_callAbrupt)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy f
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Fault f" and
t: "t = Fault f"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callFault)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy
assume bdy: "Γ (p s) = Some bdy"
assume "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Stuck"
"t = Stuck"
with bdy have "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callStuck)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
fix bdy
assume "Γ (p s) = None" "t=Stuck"
hence "Γ⊢⟨call init (p s) return' c ,Normal s⟩ ⇒ t"
by (auto intro: exec_callUndefined)
hence "Γ⊢⟨dynCall init p return' c,Normal s⟩ ⇒ t"
by (rule exec_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
assume P: "s ∈ P"
from valid_call ctxt P
have "Γ⊢dynCall init p return' c↓ Normal s"
by (rule cvalidt_termD)
hence call: "Γ⊢call init (p s) return' c↓ Normal s"
by cases
have "Γ⊢call init (p s) return c ↓ Normal s"
proof (cases "p s ∈ dom Γ")
case True
with call obtain bdy where
bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊢bdy ↓ Normal (init s)" and
termi_c: "∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶
Γ⊢c s t ↓ Normal (return' s t)"
by cases auto
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t"
hence "Γ⊢c s t ↓ Normal (return s t)"
proof -
from exec_bdy bdy
have "Γ⊢⟨Call (p s),Normal (init s)⟩ ⇒ Normal t"
by (auto simp add: intro: exec.intros)
from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
ret_modif
have "return' s t = return s t"
by auto
with termi_c exec_bdy show ?thesis by auto
qed
}
with bdy termi_bdy
show ?thesis
by (iprover intro: terminates_call)
next
case False
thus ?thesis
by (auto intro: terminates_callUndefined)
qed
thus "Γ⊢dynCall init p return c ↓ Normal s"
by (iprover intro: terminates_dynCall)
qed
lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "Γ,Θ⊢⇩t⇘/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 "Γ,Θ ⊢⇩t⇘/F⇙ P (dynCall init p return c) Q,A"
apply (rule hoaret_complete')
apply (rule dynProcModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_sound [OF modif [rule_format]])
apply assumption
done
subsubsection {* Conjunction of Postcondition *}
lemma PostConjI_sound:
assumes valid_Q: "Γ,Θ ⊨⇩t⇘/F⇙ P c Q,A"
assumes valid_R: "Γ,Θ ⊨⇩t⇘/F⇙ P c R,B"
shows "Γ,Θ ⊨⇩t⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from valid_Q ctxt exec P t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` A"
by (rule cvalidt_postD)
moreover
from valid_R ctxt exec P t_notin_F have "t ∈ Normal ` R ∪ Abrupt ` B"
by (rule cvalidt_postD)
ultimately show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ B)"
by blast
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from valid_Q ctxt P
show "Γ⊢c ↓ Normal s"
by (rule cvalidt_termD)
qed
lemma PostConjI:
assumes deriv_Q: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
assumes deriv_R: "Γ,Θ⊢⇩t⇘/F⇙ P c R,B"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c (Q ∩ R),(A ∩ B)"
apply (rule hoaret_complete')
apply (rule PostConjI_sound)
apply (rule hoaret_sound [OF deriv_Q])
apply (rule hoaret_sound [OF deriv_R])
done
lemma Merge_PostConj_sound:
assumes validF: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
assumes validG: "Γ,Θ⊨⇩t⇘/G⇙ P' c R,X"
assumes F_G: "F ⊆ G"
assumes P_P': "P ⊆ P'"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
with F_G have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/G⇙ P (Call p) Q,A"
by (auto intro: validt_augment_Faults)
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ 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 cvalidt_postD [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 cvalidt_postD [OF validG [rule_format] ctxt' exec P' this]
have "t ∈ Normal ` R ∪ Abrupt ` X" .
ultimately show ?thesis by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from validF ctxt P
show "Γ⊢c ↓ Normal s"
by (rule cvalidt_termD)
qed
lemma Merge_PostConj:
assumes validF: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
assumes validG: "Γ,Θ⊢⇩t⇘/G⇙ P' c R,X"
assumes F_G: "F ⊆ G"
assumes P_P': "P ⊆ P'"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c (Q ∩ R),(A ∩ X)"
apply (rule hoaret_complete')
apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
using validF apply (blast intro:hoaret_sound)
using validG apply (blast intro:hoaret_sound)
done
subsubsection {* Guards and Guarantees *}
lemma SplitGuards_sound:
assumes valid_c1: "Γ,Θ⊨⇩t⇘/F⇙ P c⇩1 Q,A"
assumes valid_c2: "Γ,Θ⊨⇘/F⇙ P c⇩2 UNIV,UNIV"
assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨⇘/F⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ 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_exec_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ ⇒ t" by simp
from valid_c1 ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
case Abrupt
with inter_guards_exec_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ ⇒ t" by simp
from valid_c1 ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
next
case (Fault f)
assume t: "t=Fault f"
with exec inter_guards_exec_Fault [OF c]
have "Γ⊢⟨c⇩1,Normal s⟩ ⇒ Fault f ∨ Γ⊢⟨c⇩2,Normal s⟩ ⇒ Fault f"
by auto
then show ?thesis
proof (cases rule: disjE [consumes 1])
assume "Γ⊢⟨c⇩1,Normal s⟩ ⇒ Fault f"
from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F
show ?thesis
by blast
next
assume "Γ⊢⟨c⇩2,Normal s⟩ ⇒ Fault f"
from cvalidD [OF valid_c2 ctxt' this P] t t_notin_F
show ?thesis
by blast
qed
next
case Stuck
with inter_guards_exec_noFault [OF c exec]
have "Γ⊢⟨c⇩1,Normal s⟩ ⇒ t" by simp
from valid_c1 ctxt this P t_notin_F
show ?thesis
by (rule cvalidt_postD)
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
show "Γ⊢c ↓ Normal s"
proof -
from valid_c1 ctxt P
have "Γ⊢c⇩1 ↓ Normal s"
by (rule cvalidt_termD)
with c show ?thesis
by (rule inter_guards_terminates)
qed
qed
lemma SplitGuards:
assumes c: "(c⇩1 ∩⇩g c⇩2) = Some c"
assumes deriv_c1: "Γ,Θ⊢⇩t⇘/F⇙ P c⇩1 Q,A"
assumes deriv_c2: "Γ,Θ⊢⇘/F⇙ P c⇩2 UNIV,UNIV"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule SplitGuards_sound [OF _ _ c])
apply (rule hoaret_sound [OF deriv_c1])
apply (rule hoare_sound [OF deriv_c2])
done
lemma CombineStrip_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
assumes valid_strip: "Γ,Θ⊨⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
shows "Γ,Θ⊨⇩t⇘/{}⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨⇘/{}⇙ P (Call p) Q,A"
by (auto simp add: validt_def)
from ctxt have ctxt'': "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults simp add: validt_def)
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases t)
case (Normal t')
from cvalidt_postD [OF valid ctxt'' exec P] Normal
show ?thesis
by auto
next
case (Abrupt t')
from cvalidt_postD [OF valid 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⟩ ⇒ Fault f"
by (auto intro: exec_to_exec_strip_guards_Fault)
from cvalidD [OF valid_strip ctxt' this P] Fault
have False
by auto
thus ?thesis ..
next
case False
with cvalidt_postD [OF valid ctxt'' exec P] Fault
show ?thesis
by auto
qed
next
case Stuck
from cvalidt_postD [OF valid ctxt'' exec P] Stuck
show ?thesis
by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults simp add: validt_def)
assume P: "s ∈ P"
show "Γ⊢c ↓ Normal s"
proof -
from valid ctxt' P
show "Γ⊢c ↓ Normal s"
by (rule cvalidt_termD)
qed
qed
lemma CombineStrip:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
assumes deriv_strip: "Γ,Θ⊢⇘/{}⇙ P (strip_guards (-F) c) UNIV,UNIV"
shows "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule CombineStrip_sound)
apply (iprover intro: hoaret_sound [OF deriv])
apply (iprover intro: hoare_sound [OF deriv_strip])
done
lemma GuardsFlip_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
assumes validFlip: "Γ,Θ⊨⇘/-F⇙ P c UNIV,UNIV"
shows "Γ,Θ⊨⇩t⇘/{}⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
from ctxt have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults simp add: validt_def)
from ctxt have ctxtFlip: "∀(P, p, Q, A)∈Θ. Γ⊨⇘/-F⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults simp add: validt_def)
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases t)
case (Normal t')
from cvalidt_postD [OF valid ctxt' exec P] Normal
show ?thesis
by auto
next
case (Abrupt t')
from cvalidt_postD [OF valid 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 cvalidD [OF validFlip ctxtFlip exec P] Fault
have False
by auto
thus ?thesis ..
next
case False
with cvalidt_postD [OF valid ctxt' exec P] Fault
show ?thesis
by auto
qed
next
case Stuck
from cvalidt_postD [OF valid ctxt' exec P] Stuck
show ?thesis
by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
by (auto intro: valid_augment_Faults simp add: validt_def)
assume P: "s ∈ P"
show "Γ⊢c ↓ Normal s"
proof -
from valid ctxt' P
show "Γ⊢c ↓ Normal s"
by (rule cvalidt_termD)
qed
qed
lemma GuardsFlip:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
assumes derivFlip: "Γ,Θ⊢⇘/-F⇙ P c UNIV,UNIV"
shows "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule GuardsFlip_sound)
apply (iprover intro: hoaret_sound [OF deriv])
apply (iprover intro: hoare_sound [OF derivFlip])
done
lemma MarkGuardsI_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/{}⇙ P c Q,A"
shows "Γ,Θ⊨⇩t⇘/{}⇙ P mark_guards f c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨mark_guards f c,Normal s⟩ ⇒ t"
from exec_mark_guards_to_exec [OF exec] obtain t' where
exec_c: "Γ⊢⟨c,Normal s⟩ ⇒ 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 cvalidt_postD [OF valid [rule_format] ctxt exec_c P]
have "t' ∈ Normal ` Q ∪ Abrupt ` A"
by blast
with t'_noFault
show ?thesis
by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢c ↓ Normal s".
thus "Γ⊢mark_guards f c ↓ Normal s"
by (rule terminates_to_terminates_mark_guards)
qed
lemma MarkGuardsI:
assumes deriv: "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/{}⇙ P mark_guards f c Q,A"
apply (rule hoaret_complete')
apply (rule MarkGuardsI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma MarkGuardsD_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/{}⇙ P mark_guards f c Q,A"
shows "Γ,Θ⊨⇩t⇘/{}⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
show "t ∈ Normal ` Q ∪ Abrupt ` A"
proof (cases "isFault t")
case True
with exec_to_exec_mark_guards_Fault exec
obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ ⇒ Fault f'"
by (fastforce elim: isFaultE)
from cvalidt_postD [OF valid [rule_format] ctxt this P]
have False
by auto
thus ?thesis ..
next
case False
from exec_to_exec_mark_guards [OF exec False]
obtain f' where "Γ⊢⟨mark_guards f c,Normal s⟩ ⇒ t"
by auto
from cvalidt_postD [OF valid [rule_format] ctxt this P]
show ?thesis
by auto
qed
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢mark_guards f c ↓ Normal s".
thus "Γ⊢c ↓ Normal s"
by (rule terminates_mark_guards_to_terminates)
qed
lemma MarkGuardsD:
assumes deriv: "Γ,Θ⊢⇩t⇘/{}⇙ P mark_guards f c Q,A"
shows "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule MarkGuardsD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma MergeGuardsI_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P merge_guards c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ ⇒ t"
from exec_merge_guards_to_exec [OF exec_merge]
have exec: "Γ⊢⟨c,Normal s⟩ ⇒ t" .
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from cvalidt_postD [OF valid [rule_format] ctxt exec P t_notin_F]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢c ↓ Normal s".
thus "Γ⊢merge_guards c ↓ Normal s"
by (rule terminates_to_terminates_merge_guards)
qed
lemma MergeGuardsI:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P merge_guards c Q,A"
apply (rule hoaret_complete')
apply (rule MergeGuardsI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma MergeGuardsD_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P merge_guards c Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
from exec_to_exec_merge_guards [OF exec]
have exec_merge: "Γ⊢⟨merge_guards c,Normal s⟩ ⇒ t".
assume P: "s ∈ P"
assume t_notin_F: "t ∉ Fault ` F"
from cvalidt_postD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢merge_guards c ↓ Normal s".
thus "Γ⊢c ↓ Normal s"
by (rule terminates_merge_guards_to_terminates)
qed
lemma MergeGuardsD:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P merge_guards c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule MergeGuardsD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma SubsetGuards_sound:
assumes c_c': "c ⊆⇩g c'"
assumes valid: "Γ,Θ⊨⇩t⇘/{}⇙ P c' Q,A"
shows "Γ,Θ⊨⇩t⇘/{}⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
from exec_to_exec_subseteq_guards [OF c_c' exec] obtain t' where
exec_c': "Γ⊢⟨c',Normal s⟩ ⇒ t'" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
assume P: "s ∈ P"
assume t_noFault: "t ∉ Fault ` {}"
from cvalidt_postD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
show "t ∈ Normal ` Q ∪ Abrupt ` A"
by auto
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/{}⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have termi_c': "Γ⊢c' ↓ Normal s".
from cvalidt_postD [OF valid ctxt _ P]
have noFault_c': "Γ⊢⟨c',Normal s⟩ ⇒∉Fault ` UNIV"
by (auto simp add: final_notin_def)
from termi_c' c_c' noFault_c'
show "Γ⊢c ↓ Normal s"
by (rule terminates_fewer_guards)
qed
lemma SubsetGuards:
assumes c_c': "c ⊆⇩g c'"
assumes deriv: "Γ,Θ⊢⇩t⇘/{}⇙ P c' Q,A"
shows "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule SubsetGuards_sound [OF c_c'])
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma NormalizeD_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P (normalize c) Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
hence exec_norm: "Γ⊢⟨normalize c,Normal s⟩ ⇒ t"
by (rule exec_to_exec_normalize)
assume P: "s ∈ P"
assume noFault: "t ∉ Fault ` F"
from cvalidt_postD [OF valid [rule_format] ctxt exec_norm P noFault]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢normalize c ↓ Normal s".
thus "Γ⊢c ↓ Normal s"
by (rule terminates_normalize_to_terminates)
qed
lemma NormalizeD:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P (normalize c) Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule NormalizeD_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
lemma NormalizeI_sound:
assumes valid: "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P (normalize c) Q,A"
proof (rule cvalidtI)
fix s t
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume "Γ⊢⟨normalize c,Normal s⟩ ⇒ t"
hence exec: "Γ⊢⟨c,Normal s⟩ ⇒ t"
by (rule exec_normalize_to_exec)
assume P: "s ∈ P"
assume noFault: "t ∉ Fault ` F"
from cvalidt_postD [OF valid [rule_format] ctxt exec P noFault]
show "t ∈ Normal ` Q ∪ Abrupt ` A".
next
fix s
assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A"
assume P: "s ∈ P"
from cvalidt_termD [OF valid ctxt P]
have "Γ⊢ c ↓ Normal s".
thus "Γ⊢normalize c ↓ Normal s"
by (rule terminates_to_terminates_normalize)
qed
lemma NormalizeI:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P (normalize c) Q,A"
apply (rule hoaret_complete')
apply (rule NormalizeI_sound)
apply (iprover intro: hoaret_sound [OF deriv])
done
subsubsection {* Restricting the Procedure Environment *}
lemma validt_restrict_to_validt:
assumes validt_c: "Γ|⇘M⇙⊨⇩t⇘/F⇙ P c Q,A"
shows "Γ⊨⇩t⇘/F⇙ P c Q,A"
proof -
from validt_c
have valid_c: "Γ|⇘M⇙⊨⇘/F⇙ P c Q,A" by (simp add: validt_def)
hence "Γ⊨⇘/F⇙ P c Q,A" by (rule valid_restrict_to_valid)
moreover
{
fix s
assume P: "s ∈ P"
have "Γ⊢c↓Normal s"
proof -
from P validt_c have "Γ|⇘M⇙⊢c↓Normal s"
by (auto simp add: validt_def)
moreover
from P valid_c
have "Γ|⇘M⇙⊢⟨c,Normal s⟩ ⇒∉{Stuck}"
by (auto simp add: valid_def final_notin_def)
ultimately show ?thesis
by (rule terminates_restrict_to_terminates)
qed
}
ultimately show ?thesis
by (auto simp add: validt_def)
qed
lemma augment_procs:
assumes deriv_c: "Γ|⇘M⇙,{}⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
apply (rule hoaret_complete)
apply (rule validt_restrict_to_validt)
apply (insert hoaret_sound [OF deriv_c])
by (simp add: cvalidt_def)
subsubsection {* Miscellaneous *}
lemma augment_Faults:
assumes deriv_c: "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
assumes F: "F ⊆ F'"
shows "Γ,{}⊢⇩t⇘/F'⇙ P c Q,A"
apply (rule hoaret_complete)
apply (rule validt_augment_Faults [OF _ F])
apply (insert hoaret_sound [OF deriv_c])
by (simp add: cvalidt_def)
lemma TerminationPartial_sound:
assumes "termination": "∀s ∈ P. Γ⊢c↓Normal s"
assumes partial_corr: "Γ,Θ⊨⇘/F⇙ P c Q,A"
shows "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
using "termination" partial_corr
by (auto simp add: cvalidt_def validt_def cvalid_def)
lemma TerminationPartial:
assumes partial_deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes "termination": "∀s ∈ P. Γ⊢c↓Normal s"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule hoaret_complete')
apply (rule TerminationPartial_sound [OF "termination"])
apply (rule hoare_sound [OF partial_deriv])
done
lemma TerminationPartialStrip:
assumes partial_deriv: "Γ,Θ⊢⇘/F⇙ P c Q,A"
assumes "termination": "∀s ∈ P. strip F' Γ⊢strip_guards F' c↓Normal s"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
proof -
from "termination" have "∀s ∈ P. Γ⊢c↓Normal s"
by (auto intro: terminates_strip_guards_to_terminates
terminates_strip_to_terminates)
with partial_deriv
show ?thesis
by (rule TerminationPartial)
qed
lemma SplitTotalPartial:
assumes termi: "Γ,Θ⊢⇩t⇘/F⇙ P c Q',A'"
assumes part: "Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
proof -
from hoaret_sound [OF termi] hoare_sound [OF part]
have "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
thus ?thesis
by (rule hoaret_complete')
qed
lemma SplitTotalPartial':
assumes termi: "Γ,Θ⊢⇩t⇘/UNIV⇙ P c Q',A'"
assumes part: "Γ,Θ⊢⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
proof -
from hoaret_sound [OF termi] hoare_sound [OF part]
have "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
thus ?thesis
by (rule hoaret_complete')
qed
end