# Theory Imperative_Loops

theory Imperative_Loops
imports Imperative_HOL
```(*  Title:      Imperative_Loops
Author:     Christian Sternagel
*)

section ‹Looping Constructs for Imperative HOL›

theory Imperative_Loops
imports "HOL-Imperative_HOL.Imperative_HOL"
begin

subsection ‹While Loops›

text ‹
We would have liked to restrict to read-only loop conditions using a condition of
type @{typ "heap ⇒ bool"} together with @{const tap}. However, this does not allow
for code generation due to breaking the heap-abstraction.
›
partial_function (heap) while :: "bool Heap ⇒ 'b Heap ⇒ unit Heap"
where
[code]: "while p f = do {
b ← p;
if b then f ⪢ while p f
else return ()
}"

definition "cond p h ⟷ fst (the (execute p h))"

text ‹A locale that restricts to read-only loop conditions.›
locale ro_cond =
fixes p :: "bool Heap"
assumes read_only: "success p h ⟹ snd (the (execute p h)) = h"
begin

lemma ro_cond: "ro_cond p"

lemma cond_cases [execute_simps]:
"success p h ⟹ cond p h ⟹ execute p h = Some (True, h)"
"success p h ⟹ ¬ cond p h ⟹ execute p h = Some (False, h)"
using read_only [of h] by (auto simp: cond_def success_def)

lemma execute_while_unfolds [execute_simps]:
"success p h ⟹ cond p h ⟹ execute (while p f) h = execute (f ⪢ while p f) h"
"success p h ⟹ ¬ cond p h ⟹ execute (while p f) h = execute (return ()) h"
by (auto simp: while.simps execute_simps)

lemma
success_while_cond: "success p h ⟹ cond p h ⟹ effect f h h' r ⟹ success (while p f) h' ⟹
success (while p f) h" and
success_while_not_cond: "success p h ⟹ ¬ cond p h ⟹ success (while p f) h"
by (auto simp: while.simps effect_def execute_simps intro!: success_intros)

lemma success_cond_effect:
"success p h ⟹ cond p h ⟹ effect p h h True"
using read_only [of h] by (auto simp: effect_def execute_simps)

lemma success_not_cond_effect:
"success p h ⟹ ¬ cond p h ⟹ effect p h h False"
using read_only [of h] by (auto simp: effect_def execute_simps)

end

text ‹The loop-condition does no longer hold after the loop is finished.›
lemma ro_cond_effect_while_post:
assumes "ro_cond p"
and "effect (while p f) h h' r"
shows "success p h' ∧ ¬ cond p h'"
using assms(1)
apply (induct rule: while.raw_induct [OF _ assms(2)])
apply (auto elim!: effect_elims effect_ifE simp: cond_def)
done

text ‹A rule for proving partial correctness of while loops.›
lemma ro_cond_effect_while_induct:
assumes "ro_cond p"
assumes "effect (while p f) h h' u"
and "I h"
and "⋀h h' u. I h ⟹ success p h ⟹ cond p h ⟹ effect f h h' u ⟹ I h'"
shows "I h'"
using assms(1, 3-)
proof (induction p f h h' u rule: while.raw_induct)
case (1 w p f h h' u)
obtain b
where "effect p h h b"
and *: "effect (if b then f ⪢ w p f else return ()) h h' u"
using "1.hyps" and ‹ro_cond p›
by (auto elim!: effect_elims intro: effect_intros) (metis effectE ro_cond.read_only)
then have cond: "success p h" "cond p h = b" by (auto simp: cond_def elim!: effect_elims effectE)
show ?case
proof (cases "b")
assume "¬ b"
then show ?thesis using * and ‹I h› by (auto elim: effect_elims)
next
assume "b"
moreover
with * obtain h'' and r
where "effect f h h'' r" and "effect (w p f) h'' h' u" by (auto elim: effect_elims)
moreover
ultimately
show ?thesis using 1 and cond by blast
qed
qed fact

lemma effect_success_conv:
"(∃h'. effect c h h' () ∧ I h') ⟷ success c h ∧ I (snd (the (execute c h)))"
by (auto simp: success_def effect_def)

context ro_cond
begin

lemmas
effect_while_post = ro_cond_effect_while_post [OF ro_cond] and
effect_while_induct [consumes 1, case_names base step] = ro_cond_effect_while_induct [OF ro_cond]

text ‹A rule for proving total correctness of while loops.›
lemma wf_while_induct [consumes 1, case_names success_cond success_body base step]:
assumes "wf R" ― ‹a well-founded relation on heaps proving termination of the loop›
and success_p: "⋀h. I h ⟹ success p h" ― ‹the loop-condition terminates›
and success_f: "⋀h. I h ⟹ success p h ⟹ cond p h ⟹ success f h" ― ‹the loop-body terminates›
and "I h" ― ‹the invariant holds before the loop is entered›
and step: "⋀h h' r. I h ⟹ success p h ⟹ cond p h ⟹ effect f h h' r ⟹ (h', h) ∈ R ∧ I h'"
― ‹the invariant is preserved by iterating the loop›
shows "∃h'. effect (while p f) h h' () ∧ I h'"
using ‹wf R› and ‹I h›
proof (induction h)
case (less h)
show ?case
proof (cases "cond p h")
assume "¬ cond p h" then show ?thesis
using ‹I h› and success_p [of h] by (simp add: effect_def execute_simps)
next
assume "cond p h"
with ‹I h› and success_f [of h] and step [of h] and success_p [of h]
obtain h' and r where "effect f h h' r" and "(h', h) ∈ R" and "I h'" and "success p h"
by (auto simp: success_def effect_def)
with less.IH [of h'] show ?thesis
using ‹cond p h› by (auto simp: execute_simps effect_def)
qed
qed

text ‹A rule for proving termination of while loops.›
lemmas
success_while_induct [consumes 1, case_names success_cond success_body base step] =
wf_while_induct [unfolded effect_success_conv, THEN conjunct1]

end

subsection ‹For Loops›

fun "for" :: "'a list ⇒ ('a ⇒ 'b Heap) ⇒ unit Heap"
where
"for [] f = return ()" |
"for (x # xs) f = f x ⪢ for xs f"

text ‹A rule for proving partial correctness of for loops.›
lemma effect_for_induct [consumes 2, case_names base step]:
assumes "i ≤ j"
and "effect (for [i ..< j] f) h h' u"
and "I i h"
and "⋀k h h' r. i ≤ k ⟹ k < j ⟹ I k h ⟹ effect (f k) h h' r ⟹ I (Suc k) h'"
shows "I j h'"
using assms
proof (induction "j - i" arbitrary: i h)
case 0
then show ?case by (auto elim: effect_elims)
next
case (Suc k)
show ?case
proof (cases "j = i")
case True
with Suc show ?thesis by auto
next
case False
with ‹i ≤ j› and ‹Suc k = j - i›
have "i < j" and "k = j - Suc i" and "Suc i ≤ j" by auto
then have "[i ..< j] = i # [Suc i ..< j]" by (metis upt_rec)
with ‹effect (for [i ..< j] f) h h' u› obtain h'' r
where *: "effect (f i) h h'' r" and **: "effect (for [Suc i ..< j] f) h'' h' u"
by (auto elim: effect_elims)
from Suc(6) [OF _ _ ‹I i h› *] and ‹i < j›
have "I (Suc i) h''" by auto
show ?thesis
by (rule Suc(1) [OF ‹k = j - Suc i› ‹Suc i ≤ j› ** ‹I (Suc i) h''› Suc(6)]) auto
qed
qed

text ‹A rule for proving total correctness of for loops.›
lemma for_induct [consumes 1, case_names succeed base step]:
assumes "i ≤ j"
and "⋀k h. I k h ⟹ i ≤ k ⟹ k < j ⟹ success (f k) h"
and "I i h"
and "⋀k h h' r. I k h ⟹ i ≤ k ⟹ k < j ⟹ effect (f k) h h' r ⟹ I (Suc k) h'"
shows "∃h'. effect (for [i ..< j] f) h h' () ∧ I j h'" (is "?P i h")
using assms
proof (induction "j - i" arbitrary: i h)
case 0
then show ?case by (auto simp: effect_def execute_simps)
next
case (Suc k)
show ?case
proof (cases "j = i")
assume "j = i"
with Suc show ?thesis by auto
next
assume "j ≠ i"
with ‹i ≤ j› and ‹Suc k = j - i›
have "i < j" and "k = j - Suc i" and "Suc i ≤ j" by auto
then have [simp]: "[i ..< j] = i # [Suc i ..< j]" by (metis upt_rec)
obtain h' r where *: "effect (f i) h h' r"
using Suc(4) [OF ‹I i h› le_refl ‹i < j›] by (auto elim!: success_effectE)
moreover
then have "I (Suc i) h'" using Suc by auto
moreover
have "?P (Suc i) h'"
by (rule Suc(1) [OF ‹k = j - Suc i› ‹Suc i ≤ j› Suc(4) ‹I (Suc i) h'› Suc(6)]) auto
ultimately
show ?case by (auto simp: effect_def execute_simps)
qed
qed

text ‹A rule for proving termination of for loops.›
lemmas
success_for_induct [consumes 1, case_names succeed base step] =
for_induct [unfolded effect_success_conv, THEN conjunct1]

end

```