(* 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