Theory Imperative_Loops
theory Imperative_Loops
imports
"Refine_Imperative_HOL.Sepref_HOL_Bindings"
"Refine_Imperative_HOL.Pf_Mono_Prover"
"Refine_Imperative_HOL.Pf_Add"
begin
section ‹Imperative Loops›
text "An auxiliary while rule provided by Peter Lammich."
lemma heap_WHILET_rule:
assumes
"wf R"
"P ⟹⇩A I s"
"⋀s. <I s * true> bi s <λr. I s * ↑(r ⟷ b s)>⇩t"
"⋀s. b s ⟹ <I s * true> f s <λs'. I s' * ↑((s', s) ∈ R)>⇩t"
"⋀s. ¬ b s ⟹ I s ⟹⇩A Q s"
shows "<P * true> heap_WHILET bi f s <Q>⇩t"
proof -
have "<I s * true> heap_WHILET bi f s <λs'. I s' * ↑(¬ b s')>⇩t"
using assms(1)
proof (induction arbitrary:)
case (less s)
show ?case
proof (cases "b s")
case True
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3,4) less)
next
case False
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
qed
qed
then show ?thesis
apply (rule cons_rule[rotated 2])
apply (intro ent_star_mono assms(2) ent_refl)
apply clarsimp
apply (intro ent_star_mono assms(5) ent_refl)
.
qed
lemma heap_WHILET_rule':
assumes
"wf R"
"P ⟹⇩A I s si * F"
"⋀si s. <I s si * F> bi si <λr. I s si * F * ↑(r ⟷ b s)>⇩t"
"⋀si s. b s ⟹ <I s si * F> f si <λsi'. ∃⇩As'. I s' si' * F * ↑((s', s) ∈ R)>⇩t"
"⋀si s. ¬ b s ⟹ I s si * F ⟹⇩A Q s si"
shows "<P> heap_WHILET bi f si <λsi. ∃⇩As. Q s si>⇩t"
proof -
have "<I s si * F> heap_WHILET bi f si <λsi'. ∃⇩As'. I s' si' * F * ↑(¬ b s')>⇩t"
using assms(1)
proof (induction arbitrary: si)
case (less s)
show ?case
proof (cases "b s")
case True
then show ?thesis
apply (subst heap_WHILET_unfold)
apply (sep_auto heap: assms(3,4) less)
done
next
case False
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
qed
qed
then show ?thesis
apply (rule cons_rule[rotated 2])
apply (intro ent_star_mono assms(2) ent_refl)
apply clarsimp
apply (sep_auto )
apply (erule ent_frame_fwd[OF assms(5)])
apply frame_inference
by sep_auto
qed
text "I derived my own version,
simply because it was a better fit to my use case."
corollary heap_WHILET_rule'':
assumes
"wf R"
"P ⟹⇩A I s"
"⋀s. <I s * true> bi s <λr. I s * ↑(r ⟷ b s)>⇩t"
"⋀s. b s ⟹ <I s * true> f s <λs'. I s' * ↑((s', s) ∈ R)>⇩t"
"⋀s. ¬ b s ⟹ I s ⟹⇩A Q s"
shows "<P> heap_WHILET bi f s <Q>⇩t"
supply R = heap_WHILET_rule'[of R P "λs si. ↑(s = si) * I s" s _ true bi b f "λs si.↑(s = si) * Q s * true"]
thm R
using assms ent_true_drop apply(sep_auto heap: R assms)
done
end