# Theory More_Loops

```(*
File:         More_Loops.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory More_Loops
imports
"HOL-Library.Rewrite"
begin

text ‹Most theorem below have a counterpart in the Refinement Framework that is weaker (by missing
assertions for example that are critical for code generation).
›
lemma Down_id_eq:
‹⇓Id x = x›
by auto

lemma while_upt_while_direct1:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≤ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((l, x'), (i::nat, x::'a)). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done

lemma while_upt_while_direct2:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≥ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((i::nat, x::'a), (l, x')). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done

lemma while_upt_while_direct:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} = do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
using while_upt_while_direct1[of a b] while_upt_while_direct2[of a b]
unfolding order_eq_iff by fast

lemma while_nfoldli:
"do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} ≤ nfoldli l c f σ"
apply (induct l arbitrary: σ)
apply (subst WHILET_unfold)

apply (subst WHILET_unfold)
apply (auto
simp: FOREACH_cond_def FOREACH_body_def
intro: bind_mono Refine_Basic.bind_mono(1))
done
lemma nfoldli_while: "nfoldli l c f σ
≤
(WHILE⇩T⇗I⇖
(FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l, σ) ⤜
(λ(_, σ). RETURN σ))"
proof (induct l arbitrary: σ)
case Nil thus ?case by (subst WHILEIT_unfold) (auto simp: FOREACH_cond_def)
next
case (Cons x ls)
show ?case
proof (cases "c σ")
case False thus ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def
by simp
next
case [simp]: True
from Cons show ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def FOREACH_body_def
apply clarsimp
apply (rule Refine_Basic.bind_mono)
apply simp_all
done
qed
qed

lemma while_eq_nfoldli: "do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} = nfoldli l c f σ"
apply (rule antisym)
apply (rule while_nfoldli)
apply (rule order_trans[OF nfoldli_while[where I="λ_. True"]])