Theory Imperative_Loops

(*  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"
  using read_only by (simp add: ro_cond_def)

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)
  apply (metis effectE ro_cond.read_only)+
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