section {* Hoare Logic for Total Correctness *}
theory HoareTotalDef imports HoarePartialDef Termination begin
subsection {* Validity of Hoare Tuples: @{text "Γ⊨⇩t⇘/F⇙ P c Q,A"} *}
definition
validt :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] ⇒ bool"
("_⊨⇩t⇘'/_⇙/ _ _ _,_" [61,60,1000, 20, 1000,1000] 60)
where
"Γ⊨⇩t⇘/F⇙ P c Q,A ≡ Γ⊨⇘/F⇙ P c Q,A ∧ (∀s ∈ Normal ` P. Γ⊢c↓s)"
definition
cvalidt::
"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
's assn,('s,'p,'f) com,'s assn,'s assn] ⇒ bool"
("_,_⊨⇩t⇘'/_⇙/ _ _ _,_" [61,60, 60,1000, 20, 1000,1000] 60)
where
"Γ,Θ⊨⇩t⇘/F⇙ P c Q,A ≡ (∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A) ⟶ Γ ⊨⇩t⇘/F⇙ P c Q,A"
notation (ASCII)
validt ("_|=t'/_/ _ _ _,_" [61,60,1000, 20, 1000,1000] 60) and
cvalidt ("_,_|=t'/_ / _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60)
subsection {* Properties of Validity *}
lemma validtI:
"⟦⋀s t. ⟦Γ⊢⟨c,Normal s⟩ ⇒ t;s ∈ P;t ∉ Fault ` F⟧ ⟹ t ∈ Normal ` Q ∪ Abrupt ` A;
⋀s. s ∈ P ⟹ Γ⊢ c↓(Normal s) ⟧
⟹ Γ⊨⇩t⇘/F⇙ P c Q,A"
by (auto simp add: validt_def valid_def)
lemma cvalidtI:
"⟦⋀s t. ⟦∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;Γ⊢⟨c,Normal s⟩ ⇒ t;s ∈ P;
t ∉ Fault ` F⟧
⟹ t ∈ Normal ` Q ∪ Abrupt ` A;
⋀s. ⟦∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A; s∈P⟧ ⟹ Γ⊢c↓(Normal s)⟧
⟹ Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
by (auto simp add: cvalidt_def validt_def valid_def)
lemma cvalidt_postD:
"⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;Γ⊢⟨c,Normal s ⟩ ⇒ t;
s ∈ P;t ∉ Fault ` F⟧
⟹ t ∈ Normal ` Q ∪ Abrupt ` A"
by (simp add: cvalidt_def validt_def valid_def)
lemma cvalidt_termD:
"⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;s ∈ P⟧
⟹ Γ⊢c↓(Normal s)"
by (simp add: cvalidt_def validt_def valid_def)
lemma validt_augment_Faults:
assumes valid:"Γ⊨⇩t⇘/F⇙ P c Q,A"
assumes F': "F ⊆ F'"
shows "Γ⊨⇩t⇘/F'⇙ P c Q,A"
using valid F'
by (auto intro: valid_augment_Faults simp add: validt_def)
subsection {* The Hoare Rules: @{text "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A" } *}
inductive "hoaret"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
's assn,('s,'p,'f) com,'s assn,'s assn]
=> bool"
("(3_,_/⊢⇩t⇘'/_⇙ (_/ (_)/ _,_))" [61,60,60,1000,20,1000,1000]60)
for Γ::"('s,'p,'f) body"
where
Skip: "Γ,Θ⊢⇩t⇘/F⇙ Q Skip Q,A"
| Basic: "Γ,Θ⊢⇩t⇘/F⇙ {s. f s ∈ Q} (Basic f) Q,A"
| Spec: "Γ,Θ⊢⇩t⇘/F⇙ {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)} (Spec r) Q,A"
| Seq: "⟦Γ,Θ⊢⇩t⇘/F⇙ P c⇩1 R,A; Γ,Θ⊢⇩t⇘/F⇙ R c⇩2 Q,A⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P Seq c⇩1 c⇩2 Q,A"
| Cond: "⟦Γ,Θ⊢⇩t⇘/F⇙ (P ∩ b) c⇩1 Q,A; Γ,Θ⊢⇩t⇘/F⇙ (P ∩ - b) c⇩2 Q,A⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (Cond b c⇩1 c⇩2) Q,A"
| While: "⟦wf r; ∀σ. Γ,Θ⊢⇩t⇘/F⇙ ({σ} ∩ P ∩ b) c ({t. (t,σ)∈r} ∩ P),A⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (While b c) (P ∩ - b),A"
| Guard: "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) c Q,A
⟹
Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) Guard f g c Q,A"
| Guarantee: "⟦f ∈ F; Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) c Q,A⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (Guard f g c) Q,A"
| CallRec:
"⟦(P,p,Q,A) ∈ Specs;
wf r;
Specs_wf = (λp σ. (λ(P,q,Q,A). (P ∩ {s. ((s,q),(σ,p)) ∈ r},q,Q,A)) ` Specs);
∀(P,p,Q,A)∈ Specs.
p ∈ dom Γ ∧ (∀σ. Γ,Θ ∪ Specs_wf p σ⊢⇩t⇘/F⇙ ({σ} ∩ P) (the (Γ p)) Q,A)
⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (Call p) Q,A"
| DynCom: "∀s ∈ P. Γ,Θ⊢⇩t⇘/F⇙ P (c s) Q,A
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (DynCom c) Q,A"
| Throw: "Γ,Θ⊢⇩t⇘/F⇙ A Throw Q,A"
| Catch: "⟦Γ,Θ⊢⇩t⇘/F⇙ P c⇩1 Q,R; Γ,Θ⊢⇩t⇘/F⇙ R c⇩2 Q,A⟧ ⟹ Γ,Θ⊢⇩t⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"
| Conseq: "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇩t⇘/F⇙ P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A
⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
| Asm: "(P,p,Q,A) ∈ Θ
⟹
Γ,Θ⊢⇩t⇘/F⇙ P (Call p) Q,A"
| ExFalso: "⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ¬ Γ⊨⇩t⇘/F⇙ P c Q,A⟧ ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
text {* Does not work, because of rule ExFalso, the context @{text Θ} is to blame.
A weaker version with empty context can be derived from soundness
later on. *}
lemma hoaret_to_hoarep:
assumes hoaret: "Γ,Θ⊢⇩t⇘/F⇙ P p Q,A"
shows "Γ,Θ⊢⇘/F⇙ P p Q,A"
using hoaret
proof (induct)
case Skip thus ?case by (rule hoarep.intros)
next
case Basic thus ?case by (rule hoarep.intros)
next
case Seq thus ?case by - (rule hoarep.intros)
next
case Cond thus ?case by - (rule hoarep.intros)
next
case (While r Θ F P b c A)
hence "∀σ. Γ,Θ⊢⇘/F⇙ ({σ} ∩ P ∩ b) c ({t. (t, σ) ∈ r} ∩ P),A"
by iprover
hence "Γ,Θ⊢⇘/F⇙ (P ∩ b) c P,A"
by (rule HoarePartialDef.conseq) blast
then show "Γ,Θ⊢⇘/F⇙ P While b c (P ∩ - b),A"
by (rule hoarep.While)
next
case Guard thus ?case by - (rule hoarep.intros)
next
case DynCom thus ?case by (blast intro: hoarep.DynCom)
next
case Throw thus ?case by - (rule hoarep.Throw)
next
case Catch thus ?case by - (rule hoarep.Catch)
next
case Conseq thus ?case by - (rule hoarep.Conseq,blast)
next
case Asm thus ?case by (rule HoarePartialDef.Asm)
next
case (ExFalso Θ F P c Q A)
assume "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
hence "Γ,Θ⊨⇘/F⇙ P c Q,A"
oops
lemma hoaret_augment_context:
assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P p Q,A"
shows "⋀Θ'. Θ ⊆ Θ' ⟹ Γ,Θ'⊢⇩t⇘/F⇙ P p Q,A"
using deriv
proof (induct)
case (CallRec P p Q A Specs r Specs_wf Θ F Θ')
have aug: "Θ ⊆ Θ'" by fact
then
have h: "⋀τ p. Θ ∪ Specs_wf p τ
⊆ Θ' ∪ Specs_wf p τ"
by blast
have "∀(P,p,Q,A)∈Specs. p ∈ dom Γ ∧
(∀τ. Γ,Θ ∪ Specs_wf p τ⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A ∧
(∀x. Θ ∪ Specs_wf p τ
⊆ x ⟶
Γ,x⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A))" by fact
hence "∀(P,p,Q,A)∈Specs. p ∈ dom Γ ∧
(∀τ. Γ,Θ'∪ Specs_wf p τ ⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A)"
apply (clarify)
apply (rename_tac P p Q A)
apply (drule (1) bspec)
apply (clarsimp)
apply (erule_tac x=τ in allE)
apply clarify
apply (erule_tac x="Θ' ∪ Specs_wf p τ" in allE)
apply (insert aug)
apply auto
done
with CallRec show ?case by - (rule hoaret.CallRec)
next
case DynCom thus ?case by (blast intro: hoaret.DynCom)
next
case (Conseq P Θ F c Q A Θ')
from Conseq
have "∀s ∈ P. (∃P' Q' A'. (Γ,Θ' ⊢⇩t⇘/F⇙ P' c Q',A') ∧ s ∈ P'∧ Q' ⊆ Q ∧ A' ⊆ A)"
by blast
with Conseq show ?case by - (rule hoaret.Conseq)
next
case (ExFalso Θ F P c Q A Θ')
have "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A" "¬ Γ⊨⇩t⇘/F⇙ P c Q,A" "Θ ⊆ Θ'" by fact+
then show ?case
by (fastforce intro: hoaret.ExFalso simp add: cvalidt_def)
qed (blast intro: hoaret.intros)+
subsection {* Some Derived Rules *}
lemma Conseq': "∀s. s ∈ P ⟶
(∃P' Q' A'.
(∀ Z. Γ,Θ⊢⇩t⇘/F⇙ (P' Z) c (Q' Z),(A' Z)) ∧
(∃Z. s ∈ P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A)))
⟹
Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule Conseq)
apply (rule ballI)
apply (erule_tac x=s in allE)
apply (clarify)
apply (rule_tac x="P' Z" in exI)
apply (rule_tac x="Q' Z" in exI)
apply (rule_tac x="A' Z" in exI)
apply blast
done
lemma conseq:"⟦∀Z. Γ,Θ ⊢⇩t⇘/F⇙ (P' Z) c (Q' Z),(A' Z);
∀s. s ∈ P ⟶ (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q)∧ (A' Z ⊆ A))⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule Conseq) blast
theorem conseqPrePost:
"Γ,Θ⊢⇩t⇘/F⇙ P' c Q',A' ⟹ P ⊆ P' ⟹ Q' ⊆ Q ⟹ A' ⊆ A ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule conseq [where ?P'="λZ. P'" and ?Q'="λZ. Q'"]) auto
lemma conseqPre: "Γ,Θ⊢⇩t⇘/F⇙ P' c Q,A ⟹ P ⊆ P' ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule conseq) auto
lemma conseqPost: "Γ,Θ⊢⇩t⇘/F⇙ P c Q',A'⟹ Q' ⊆ Q ⟹ A' ⊆ A ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule conseq) auto
lemma Spec_wf_conv:
"(λ(P, q, Q, A). (P ∩ {s. ((s, q), τ, p) ∈ r}, q, Q, A)) `
(⋃p∈Procs. ⋃Z. {(P p Z, p, Q p Z, A p Z)}) =
(⋃q∈Procs. ⋃Z. {(P q Z ∩ {s. ((s, q), τ, p) ∈ r}, q, Q q Z, A q Z)})"
by (auto intro!: image_eqI)
lemma CallRec':
"⟦p∈Procs; Procs ⊆ dom Γ;
wf r;
∀p∈Procs. ∀τ Z.
Γ,Θ∪(⋃q∈Procs. ⋃Z.
{((P q Z) ∩ {s. ((s,q),(τ,p)) ∈ r},q,Q q Z,(A q Z))})
⊢⇩t⇘/F⇙ ({τ} ∩ (P p Z)) (the (Γ p)) (Q p Z),(A p Z)⟧
⟹
Γ,Θ⊢⇩t⇘/F⇙ (P p Z) (Call p) (Q p Z),(A p Z)"
apply (rule CallRec [where Specs="⋃p∈Procs. ⋃Z. {((P p Z),p,Q p Z,A p Z)}" and
r=r])
apply blast
apply assumption
apply (rule refl)
apply (clarsimp)
apply (rename_tac p')
apply (rule conjI)
apply blast
apply (intro allI)
apply (rename_tac Z τ)
apply (drule_tac x=p' in bspec, assumption)
apply (erule_tac x=τ in allE)
apply (erule_tac x=Z in allE)
apply (fastforce simp add: Spec_wf_conv)
done
end