Theory Loops
section ‹The Loop Rules›
theory Loops imports WellDefined begin
text_raw ‹\label{s:loop_rules}›
text ‹Given a well-defined body, we can annotate a loop using an invariant, just as in the
classical setting.›
subsection ‹Liberal and Strict Invariants.›
text ‹A probabilistic invariant generalises a boolean one: it \emph{entails} itself, given
the loop guard.›
definition
wp_inv :: "('s ⇒ bool) ⇒ 's prog ⇒ ('s ⇒ real) ⇒ bool"
where
"wp_inv G body I ⟷ (∀s. «G» s * I s ≤ wp body I s)"
lemma wp_invI:
"⋀I. (⋀s. «G» s * I s ≤ wp body I s) ⟹ wp_inv G body I"
by(simp add:wp_inv_def)
definition
wlp_inv :: "('s ⇒ bool) ⇒ 's prog ⇒ ('s ⇒ real) ⇒ bool"
where
"wlp_inv G body I ⟷ (∀s. «G» s * I s ≤ wlp body I s)"
lemma wlp_invI:
"⋀I. (⋀s. «G» s * I s ≤ wlp body I s) ⟹ wlp_inv G body I"
by(simp add:wlp_inv_def)
lemma wlp_invD:
"wlp_inv G body I ⟹ «G» s * I s ≤ wlp body I s"
by(simp add:wlp_inv_def)
text ‹For standard invariants, the multiplication reduces to conjunction.›
lemma wp_inv_stdD:
assumes inv: "wp_inv G body «I»"
and hb: "healthy (wp body)"
shows "«G» && «I» ⊩ wp body «I»"
proof(rule le_funI)
fix s
show "(«G» && «I») s ≤ wp body «I» s"
proof(cases "G s")
case False
with hb show ?thesis
by(auto simp:exp_conj_def)
next
case True
hence "(«G» && «I») s = «G» s * «I» s"
by(simp add:exp_conj_def)
also from inv have "«G» s * «I» s ≤ wp body «I» s"
by(simp add:wp_inv_def)
finally show ?thesis .
qed
qed
subsection ‹Partial Correctness›
text ‹Partial correctness for loops\<^citep>‹‹Lemma 7.2.2, \S7, p.~185› in "McIver_M_04"›.›
lemma wlp_Loop:
assumes wd: "well_def body"
and uI: "unitary I"
and inv: "wlp_inv G body I"
shows "I ≤ wlp do G ⟶ body od (λs. «𝒩 G» s * I s)"
(is "I ≤ wlp do G ⟶ body od ?P")
proof -
let "?f Q s" = "«G» s * wlp body Q s + «𝒩 G» s * ?P s"
have "I ⊩ gfp_exp ?f"
proof(rule gfp_exp_upperbound[OF _ uI])
have "I = (λs. («G» s + «𝒩 G» s) * I s)" by(simp add:negate_embed)
also have "... = (λs. «G» s * I s + «𝒩 G» s * I s)"
by(simp add:algebra_simps)
also have "... = (λs. «G» s * («G» s * I s) + «𝒩 G» s * («𝒩 G» s * I s))"
by(simp add:embed_bool_idem algebra_simps)
also have "... ⊩ (λs. «G» s * wlp body I s + «𝒩 G» s * («𝒩 G» s * I s))"
using inv by(auto dest:wlp_invD intro:add_mono mult_left_mono)
finally show "I ⊩ (λs. «G» s * wlp body I s + «𝒩 G» s * («𝒩 G» s * I s))" .
qed
also from uI well_def_wlp_nearly_healthy[OF wd] have "... = wlp do G ⟶ body od ?P"
by(auto intro!:wlp_Loop1[symmetric] unitary_intros)
finally show ?thesis .
qed
subsection ‹Total Correctness›
text_raw ‹\label{s:loop_total}›
text ‹The first total correctness lemma for loops which terminate with probability 1\<^citep>‹‹Lemma
7.3.1, \S7, p.~186› in "McIver_M_04"›.›
lemma wp_Loop:
assumes wd: "well_def body"
and inv: "wlp_inv G body I"
and unit: "unitary I"
shows "I && wp (do G ⟶ body od) (λs. 1) ⊩ wp (do G ⟶ body od) (λs. «𝒩 G» s * I s)"
(is "I && ?T ⊩ wp ?loop ?X")
proof -
txt ‹We first appeal to the \emph{liberal} loop rule:›
from assms have "I && ?T ⊩ wlp ?loop ?X && ?T"
by(blast intro:exp_conj_mono_left wlp_Loop)
txt ‹Next, by sub-conjunctivity:›
also {
from wd have sdp_loop: "sub_distrib_pconj (do G ⟶ body od)"
by(blast intro:sdp_intros)
from wd unit have "wlp ?loop ?X && ?T ⊩ wp ?loop (?X && (λs. 1))"
by(blast intro:sub_distrib_pconjD sdp_intros unitary_intros)
}
txt ‹Finally, the conjunction collapses:›
finally show ?thesis
by(simp add:exp_conj_1_right sound_intros sound_nneg unit unitary_sound)
qed
subsection ‹Unfolding›
lemma wp_loop_unfold:
fixes body :: "'s prog"
assumes sP: "sound P"
and h: "healthy (wp body)"
shows "wp (do G ⟶ body od) P =
(λs. «𝒩 G» s * P s + «G» s * wp body (wp (do G ⟶ body od) P) s)"
proof (simp only: wp_eval)
let "?X t" = "wp (body ;; Embed t ⇘« G »⇙⊕ Skip)"
have "equiv_trans (lfp_trans ?X)
(wp (body ;; Embed (lfp_trans ?X) ⇘« G »⇙⊕ Skip))"
proof(intro lfp_trans_unfold)
fix t::"'s trans" and P::"'s expect"
assume st: "⋀Q. sound Q ⟹ sound (t Q)"
and sP: "sound P"
with h show "sound (?X t P)"
by(rule wp_loop_step_sound)
next
fix t u::"'s trans"
assume "le_trans t u" "(⋀P. sound P ⟹ sound (t P))"
"(⋀P. sound P ⟹ sound (u P))"
with h show "le_trans (wp (body ;; Embed t ⇘« G »⇙⊕ Skip))
(wp (body ;; Embed u ⇘« G »⇙⊕ Skip))"
by(iprover intro:wp_loop_step_mono)
next
let ?v = "λP s. bound_of P"
from h show "le_trans (wp (body ;; Embed ?v ⇘« G »⇙⊕ Skip)) ?v"
by(intro le_transI, simp add:wp_eval lfp_loop_fp[unfolded negate_embed])
fix P::"'s expect"
assume "sound P" thus "sound (?v P)" by(auto)
qed
also have "equiv_trans ...
(λP s. «𝒩 G» s * P s + «G» s * wp body (wp (Embed (lfp_trans ?X)) P) s)"
by(rule equiv_transI, simp add:wp_eval algebra_simps negate_embed)
finally show "lfp_trans ?X P =
(λs. «𝒩 G» s * P s + «G» s * wp body (lfp_trans ?X P) s)"
using sP unfolding wp_eval by(blast)
qed
lemma wp_loop_nguard:
"⟦ healthy (wp body); sound P; ¬ G s ⟧ ⟹ wp do G ⟶ body od P s = P s"
by(subst wp_loop_unfold, simp_all)
lemma wp_loop_guard:
"⟦ healthy (wp body); sound P; G s ⟧ ⟹
wp do G ⟶ body od P s = wp (body ;; do G ⟶ body od) P s"
by(subst wp_loop_unfold, simp_all add:wp_eval)
end