# Theory Refine_Foreach

```section ‹Foreach Loops›
theory Refine_Foreach
imports
Refine_While
Refine_Pfun
Refine_Transfer
Refine_Heuristics
(*"../Collections/Lib/SetIterator"
"../Collections/Lib/Proper_Iterator"*)
begin

text ‹
A common pattern for loop usage is iteration over the elements of a set.
This theory provides the ‹FOREACH›-combinator, that iterates over
each element of a set.
›

subsection ‹Auxilliary Lemmas›
text ‹The following lemma is commonly used when reasoning about iterator
invariants.
It helps converting the set of elements that remain to be iterated over to
the set of elements already iterated over.›
lemma it_step_insert_iff:
"it ⊆ S ⟹ x∈it ⟹ S-(it-{x}) = insert x (S-it)" by auto

subsection ‹Definition›

text ‹
Foreach-loops come in different versions, depending on whether they have an
annotated invariant (I), a termination condition (C), and an order (O).

Note that asserting that the set is finite is not necessary to guarantee
termination. However, we currently provide only iteration over finite sets,
as this also matches the ICF concept of iterators.
›

definition "FOREACH_body f ≡ λ(xs, σ). do {
let x = hd xs; σ'←f x σ; RETURN (tl xs,σ')
}"

definition FOREACH_cond where "FOREACH_cond c ≡ (λ(xs,σ). xs≠[] ∧ c σ)"

text ‹Foreach with continuation condition, order and annotated invariant:›

definition FOREACHoci ("FOREACH⇩O⇩C⇗_,_⇖") where "FOREACHoci R Φ S c f σ0 ≡ do {
ASSERT (finite S);
xs ← SPEC (λxs. distinct xs ∧ S = set xs ∧ sorted_wrt R xs);
(_,σ) ← WHILEIT
(λ(it,σ). ∃xs'. xs = xs' @ it ∧ Φ (set it) σ) (FOREACH_cond c) (FOREACH_body f) (xs,σ0);
RETURN σ }"

text ‹Foreach with continuation condition and annotated invariant:›
definition FOREACHci ("FOREACH⇩C⇗_⇖") where "FOREACHci ≡ FOREACHoci (λ_ _. True)"

text ‹Foreach with continuation condition:›
definition FOREACHc ("FOREACH⇩C") where "FOREACHc ≡ FOREACHci (λ_ _. True)"

text ‹Foreach with annotated invariant:›
definition FOREACHi ("FOREACH⇗_⇖") where
"FOREACHi Φ S ≡ FOREACHci Φ S (λ_. True)"

text ‹Foreach with annotated invariant and order:›
definition FOREACHoi ("FOREACH⇩O⇗_,_⇖") where
"FOREACHoi R Φ S ≡ FOREACHoci R Φ S (λ_. True)"

text ‹Basic foreach›
definition "FOREACH S ≡ FOREACHc S (λ_. True)"

lemmas FOREACH_to_oci_unfold
= FOREACHci_def FOREACHc_def FOREACHi_def FOREACHoi_def FOREACH_def

subsection ‹Proof Rules›

lemma FOREACHoci_rule[refine_vcg]:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ c σ; x∈it; it⊆S; I it σ; ∀y∈it - {x}. R x y;
∀y∈S - it. R y x ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it≠{}; it⊆S; I it σ; ¬c σ;
∀x∈it. ∀y∈S - it. R y x ⟧ ⟹ P σ"
shows "FOREACHoci R I S c f σ0 ≤ SPEC P"
unfolding FOREACHoci_def
apply (intro refine_vcg)

apply (rule FIN)

apply (subgoal_tac "wf (measure (λ(xs, _). length xs))")
apply assumption
apply simp

apply (insert I0, simp add: I0) []
unfolding FOREACH_body_def FOREACH_cond_def
apply (rule refine_vcg)+
apply ((simp, elim conjE exE)+) []
apply (rename_tac xs'' s xs' σ xs)
defer
apply (simp, elim conjE exE)+
apply (rename_tac x s xs' σ xs)
defer
proof -
fix xs' σ xs

assume I_xs': "I (set xs') σ"
and sorted_xs_xs': "sorted_wrt R (xs @ xs')"
and dist: "distinct xs" "distinct xs'" "set xs ∩ set xs' = {}"
and S_eq: "S = set xs ∪ set xs'"

from S_eq have "set xs' ⊆ S" by simp
from dist S_eq have S_diff: "S - set xs' = set xs" by blast

{ assume "xs' ≠ []" "c σ"
from ‹xs' ≠ []› obtain x xs'' where xs'_eq: "xs' = x # xs''" by (cases xs', auto)

have x_in_xs': "x ∈ set xs'" and x_nin_xs'': "x ∉ set xs''"
using ‹distinct xs'› unfolding xs'_eq by simp_all

from IP[of σ x "set xs'", OF ‹c σ› x_in_xs' ‹set xs' ⊆ S› ‹I (set xs') σ›] x_nin_xs''
sorted_xs_xs' S_diff
show "f (hd xs') σ ≤ SPEC
(λx. (∃xs'a. xs @ xs' = xs'a @ tl xs') ∧
I (set (tl xs')) x)"
done
}

{ assume "xs' = [] ∨ ¬(c σ)"
show "P σ"
proof (cases "xs' = []")
case True thus "P σ" using ‹I (set xs') σ› by (simp add: II1)
next
case False note xs'_neq_nil = this
with ‹xs' = [] ∨ ¬ c σ› have "¬ c σ" by simp

from II2 [of "set xs'" σ] S_diff sorted_xs_xs'
show "P σ"
apply (simp add: xs'_neq_nil S_eq ‹¬ c σ› I_xs')
done
qed
}
qed

lemma FOREACHoi_rule[refine_vcg]:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ; ∀y∈it - {x}. R x y;
∀y∈S - it. R y x ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
shows "FOREACHoi R I S f σ0 ≤ SPEC P"
unfolding FOREACHoi_def
by (rule FOREACHoci_rule) (simp_all add: assms)

lemma FOREACHci_rule[refine_vcg]:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it≠{}; it⊆S; I it σ; ¬c σ ⟧ ⟹ P σ"
shows "FOREACHci I S c f σ0 ≤ SPEC P"
unfolding FOREACHci_def
by (rule FOREACHoci_rule) (simp_all add: assms)

subsubsection ‹Refinement:›

text ‹
Refinement rule using a coupling invariant over sets of remaining
items and the state.
›

lemma FOREACHoci_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFC: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ;
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ';
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; ∀y∈it-{x}. RR x y;
x'∈it'; ∀y'∈it'-{x'}. RR' x' y';
c σ; c' σ'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ Φ {} σ; Φ' {} σ'; (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
assumes REF_R_BRK: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
it'=α`it; ((it,σ),(it',σ'))∈R;
it≠{}; it'≠{};
¬c σ; ¬c' σ'
⟧ ⟹ (σ,σ')∈R'"
shows "FOREACHoci RR Φ S c f σ0 ≤ ⇓R' (FOREACHoci RR' Φ' S' c' f' σ0')"
(* TODO: Clean up this mess !!! *)
supply [[simproc del: defined_all]]
unfolding FOREACHoci_def
apply (refine_rcg WHILEIT_refine_genR[where
R'="{((xs,σ),(xs',σ')) .
xs'=map α xs ∧
set xs ⊆ S ∧ set xs' ⊆ S' ∧
(∀x∈S - set xs. ∀y∈set xs. RR x y) ∧
(∀x∈S' - set xs'. ∀y∈set xs'. RR' x y) ∧
((set xs,σ),(set xs',σ')) ∈ R }"
])

using REFS INJ apply (auto dest: finite_imageD) []
apply (rule intro_prgR[where R="{(xs,xs') . xs'=map α xs }"])
apply (rule SPEC_refine)
using INJ RR_OK
apply (auto
intro: sorted_wrt_mono_rel[of _ RR]) []
using REF0 apply auto []

apply simp apply (rule conjI)
using INJ apply clarsimp
apply (erule map_eq_appendE)
apply clarsimp
apply (rule_tac x=l in exI)
apply simp
apply (subst inj_on_map_eq_map[where f=α,symmetric])
apply (rule subset_inj_on, assumption, blast)
apply assumption

apply (simp split: prod.split_asm, elim conjE)
apply (rule REFPHI, auto) []

apply (simp add: FOREACH_cond_def split: prod.split prod.split_asm,
intro allI impI conj_cong) []
apply auto []
apply (rule REFC, auto) []

unfolding FOREACH_body_def
apply refine_rcg
apply (rule REFSTEP) []
prefer 3 apply auto []
prefer 3 apply auto []
apply simp_all[13]
apply auto []
apply (rename_tac a b d e f g h i)
apply (case_tac h, auto simp: FOREACH_cond_def) []
apply auto []
apply (auto simp: FOREACH_cond_def) []
apply (clarsimp simp: FOREACH_cond_def)
apply (rule ccontr)
apply (rename_tac a b d e f)
apply (case_tac b)
apply (auto simp: sorted_wrt_append) [2]

apply (auto simp: FOREACH_cond_def) []
apply (rename_tac a b d e)
apply (case_tac b)
apply (auto) [2]

apply (clarsimp simp: FOREACH_cond_def)
apply (rule ccontr)
apply (rename_tac a b d e f)
apply (case_tac b)
apply (auto simp: sorted_wrt_append) [2]

apply (clarsimp simp: FOREACH_cond_def)
apply (clarsimp simp: FOREACH_cond_def)

apply (clarsimp simp: map_tl)
apply (intro conjI)

apply (rename_tac a b d e f g)
apply (case_tac b, auto) []
apply (rename_tac a b d e f g)
apply (case_tac b, auto) []
apply (rename_tac a b d e f g)
apply (case_tac b, auto simp: sorted_wrt_append) []
apply (rename_tac a b d e f g)
apply (case_tac b, auto simp: sorted_wrt_append) []
apply (rename_tac a b d e f g)
apply (case_tac b, auto) []

apply (rule introR[where R="{((xs,σ),(xs',σ')).
xs'=map α xs ∧ Φ (set xs) σ ∧ Φ' (set xs') σ' ∧
set xs ⊆ S ∧ set xs' ⊆ S' ∧
(∀x∈S - set xs. ∀y∈set xs. RR x y) ∧
(∀x∈S' - set xs'. ∀y∈set xs'. RR' x y) ∧
((set xs,σ),(set xs',σ')) ∈ R ∧
¬ FOREACH_cond c (xs,σ) ∧ ¬ FOREACH_cond c' (xs',σ')
}
"])
apply auto []
apply (simp add: FOREACH_cond_def, elim conjE)
apply (elim disjE1, simp_all) []
using REF_R_DONE apply auto []
using REF_R_BRK apply auto []
done

lemma FOREACHoci_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ';  Φ'' it σ it' σ'; Φ it σ; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦∀y∈it-{x}. RR x y;
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACHoci RR Φ S c f σ0 ≤ ⇓R (FOREACHoci RR' Φ' S' c' f' σ0')"

apply (rule FOREACHoci_refine_genR[
where R = "{((it,σ),(it',σ')). (σ,σ')∈R ∧ Φ'' it σ it' σ'}"
])
apply fact
apply fact
apply fact
using REF0 REFPHI0 apply blast
using REFC apply auto []
using REFPHI apply auto []
using REFSTEP apply auto []
apply auto []
apply auto []
done

lemma FOREACHoci_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦ ∀y∈it-{x}. RR x y;
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHoci RR Φ S c f σ0 ≤ ⇓R (FOREACHoci RR' Φ' S' c' f' σ0')"
apply (rule FOREACHoci_refine[where Φ''="λ_ _ _ _. True"])
apply (rule assms)+
using assms by simp_all

lemma FOREACHoci_weaken:
assumes IREF: "⋀it σ. it⊆S ⟹ I it σ ⟹ I' it σ"
shows "FOREACHoci RR I' S c f σ0 ≤ FOREACHoci RR I S c f σ0"
apply (rule FOREACHoci_refine_rcg[where α=id and R=Id, simplified])
apply (auto intro: IREF)
done

lemma FOREACHoci_weaken_order:
assumes RRREF: "⋀x y. x ∈ S ⟹ y ∈ S ⟹ RR x y ⟹ RR' x y"
shows "FOREACHoci RR I S c f σ0 ≤ FOREACHoci RR' I S c f σ0"
apply (rule FOREACHoci_refine_rcg[where α=id and R=Id, simplified])
apply (auto intro: RRREF)
done

subsubsection ‹Rules for Derived Constructs›

lemma FOREACHoi_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ';
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
∀x∈S-it. ∀y∈it. RR x y; ∀x∈S'-it'. ∀y∈it'. RR' x y;
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; ∀y∈it-{x}. RR x y;
x'∈it'; ∀y'∈it'-{x'}. RR' x' y'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ Φ {} σ; Φ' {} σ'; (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
shows "FOREACHoi RR Φ S f σ0 ≤ ⇓R' (FOREACHoi RR' Φ' S' f' σ0')"
unfolding FOREACHoi_def
apply (rule FOREACHoci_refine_genR)
apply (fact | simp)+
using REFSTEP apply auto []
apply (fact | simp)+
done

lemma FOREACHoi_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦∀y∈it-{x}. RR x y;
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACHoi RR Φ S f σ0 ≤ ⇓R (FOREACHoi RR' Φ' S' f' σ0')"
unfolding FOREACHoi_def
apply (rule FOREACHoci_refine [of α _ _ _ _ _ _ _ Φ''])
done

lemma FOREACHoi_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes RR_OK: "⋀x y. ⟦x ∈ S; y ∈ S; RR x y⟧ ⟹ RR' (α x) (α y)"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦ ∀y∈it-{x}. RR x y;
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHoi RR Φ S f σ0 ≤ ⇓R (FOREACHoi RR' Φ' S' f' σ0')"
apply (rule FOREACHoi_refine[where Φ''="λ_ _ _ _. True"])
apply (rule assms)+
using assms by simp_all

lemma FOREACHci_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFC: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ;
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ';
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; x'∈it';
c σ; c' σ'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ Φ {} σ; Φ' {} σ'; (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
assumes REF_R_BRK: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
it'=α`it; ((it,σ),(it',σ'))∈R;
it≠{}; it'≠{};
¬c σ; ¬c' σ'
⟧ ⟹ (σ,σ')∈R'"
shows "FOREACHci Φ S c f σ0 ≤ ⇓R' (FOREACHci Φ' S' c' f' σ0')"
unfolding FOREACHci_def
apply (rule FOREACHoci_refine_genR)
apply (fact|simp)+
using REFC apply auto []
using REFPHI apply auto []
using REFSTEP apply auto []
apply (fact|simp)+
using REF_R_BRK apply auto []
done

lemma FOREACHci_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ';  Φ'' it σ it' σ'; Φ it σ; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ';  Φ'' it σ it' σ'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACHci Φ S c f σ0 ≤ ⇓R (FOREACHci Φ' S' c' f' σ0')"
unfolding FOREACHci_def
apply (rule FOREACHoci_refine [of α _ _ _ _ _ _ _ Φ''])
done

lemma FOREACHci_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ it σ; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHci Φ S c f σ0 ≤ ⇓R (FOREACHci Φ' S' c' f' σ0')"
apply (rule FOREACHci_refine[where Φ''="λ_ _ _ _. True"])
apply (rule assms)+
using assms by auto

lemma FOREACHci_weaken:
assumes IREF: "⋀it σ. it⊆S ⟹ I it σ ⟹ I' it σ"
shows "FOREACHci I' S c f σ0 ≤ FOREACHci I S c f σ0"
apply (rule FOREACHci_refine_rcg[where α=id and R=Id, simplified])
apply (auto intro: IREF)
done

lemma FOREACHi_rule[refine_vcg]:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
shows "FOREACHi I S f σ0 ≤ SPEC P"
unfolding FOREACHi_def
apply (rule FOREACHci_rule[of S I])
using assms by auto

lemma FOREACHc_rule:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it≠{}; it⊆S; I it σ; ¬c σ ⟧ ⟹ P σ"
shows "FOREACHc S c f σ0 ≤ SPEC P"
unfolding FOREACHc_def
apply (rule order_trans[OF FOREACHci_weaken], rule TrueI)
apply (rule FOREACHci_rule[where I=I])
using assms by auto

lemma FOREACH_rule:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II: "⋀σ. ⟦I {} σ⟧ ⟹ P σ"
shows "FOREACH S f σ0 ≤ SPEC P"
unfolding FOREACH_def FOREACHc_def
apply (rule order_trans[OF FOREACHci_weaken], rule TrueI)
apply (rule FOREACHci_rule[where I=I])
using assms by auto

lemma FOREACHc_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFC: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S';
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S';
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; x'∈it';
c σ; c' σ'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
assumes REF_R_BRK: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S';
it'=α`it; ((it,σ),(it',σ'))∈R;
it≠{}; it'≠{};
¬c σ; ¬c' σ'
⟧ ⟹ (σ,σ')∈R'"
shows "FOREACHc S c f σ0 ≤ ⇓R' (FOREACHc S' c' f' σ0')"
unfolding FOREACHc_def
apply (rule FOREACHci_refine_genR)
apply simp_all
apply (fact|simp)+
using REFC apply auto []
using REFSTEP apply auto []
using REF_R_DONE apply auto []
using REF_R_BRK apply auto []
done

lemma FOREACHc_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ'' it σ it' σ'; c σ; c' σ'; (σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACHc S c f σ0 ≤ ⇓R (FOREACHc S' c' f' σ0')"
unfolding FOREACHc_def
apply (rule FOREACHci_refine[where Φ''=Φ'', OF INJ REFS REF0 REFPHI0])
apply (erule (4) REFC)
apply (rule TrueI)
apply (erule (9) REFSTEP)
done

lemma FOREACHc_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHc S c f σ0 ≤ ⇓R (FOREACHc S' c' f' σ0')"
unfolding FOREACHc_def
apply (rule FOREACHci_refine_rcg)
apply (rule assms)+
using assms by auto

lemma FOREACHi_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it⊆S; it'⊆S'; Φ' it' σ';
it'=α`it; ((it,σ),(it',σ'))∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S'; Φ it σ; Φ' it' σ';
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; x'∈it'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ Φ {} σ; Φ' {} σ'; (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
shows "FOREACHi Φ S f σ0 ≤ ⇓R' (FOREACHi Φ' S' f' σ0')"
unfolding FOREACHi_def
apply (rule FOREACHci_refine_genR)
apply (fact|simp)+
using REFSTEP apply auto []
apply (fact|simp)+
done

lemma FOREACHi_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ';  Φ'' it σ it' σ';
(σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACHi Φ S f σ0 ≤ ⇓R (FOREACHi Φ' S' f' σ0')"
unfolding FOREACHi_def
apply (rule FOREACHci_refine[where Φ''=Φ'', OF INJ REFS REF0 REFPHI0])
apply (rule refl)
apply (erule (5) REFPHI)
apply (erule (9) REFSTEP)
done

lemma FOREACHi_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFPHI: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ Φ it σ"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ it σ; Φ' it' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHi Φ S f σ0 ≤ ⇓R (FOREACHi Φ' S' f' σ0')"
unfolding FOREACHi_def
apply (rule FOREACHci_refine_rcg)
apply (rule assms)+
using assms apply auto
done

lemma FOREACH_refine_genR:
fixes α :: "'S ⇒ 'Sa" ― ‹Abstraction mapping of elements›
fixes S :: "'S set" ― ‹Concrete set›
fixes S' :: "'Sa set" ― ‹Abstract set›
fixes σ0 :: "'σ"
fixes σ0' :: "'σa"
fixes R :: "(('S set × 'σ) × ('Sa set × 'σa)) set"
assumes INJ: "inj_on α S"
assumes REFS[simp]: "S' = α`S"
assumes REF0: "((S,σ0),(α`S,σ0')) ∈ R"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
it⊆S; it'⊆S';
x'=α x; it'=α`it; ((it,σ),(it',σ'))∈R;
x∈it; x'∈it'
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). ((it-{x},σ),(it'-{x'},σ'))∈R}) (f' x' σ')"
assumes REF_R_DONE: "⋀σ σ'. ⟦ (({},σ),({},σ'))∈R ⟧
⟹ (σ,σ')∈R'"
shows "FOREACH S f σ0 ≤ ⇓R' (FOREACH S' f' σ0')"
unfolding FOREACH_def
apply (rule FOREACHc_refine_genR)
apply (fact|simp)+
using REFSTEP apply auto []
apply (fact|simp)+
done

lemma FOREACH_refine:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFPHI0: "Φ'' S σ0 (α`S) σ0'"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ'' it σ it' σ'; (σ,σ')∈R
⟧ ⟹ f x σ
≤ ⇓({(σ, σ'). (σ, σ') ∈ R ∧ Φ'' (it - {x}) σ (it' - {x'}) σ'}) (f' x' σ')"
shows "FOREACH S f σ0 ≤ ⇓R (FOREACH S' f' σ0')"
unfolding FOREACH_def
apply (rule FOREACHc_refine[where Φ''=Φ'', OF INJ REFS REF0 REFPHI0])
apply (rule refl)
apply (erule (7) REFSTEP)
done

lemma FOREACH_refine_rcg[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACH S f σ0 ≤ ⇓R (FOREACH S' f' σ0')"
unfolding FOREACH_def
apply (rule FOREACHc_refine_rcg)
apply (rule assms)+
using assms by auto

lemma FOREACHci_refine_rcg'[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFC: "⋀it σ it' σ'. ⟦
it'=α`it; it⊆S; it'⊆S'; Φ' it' σ'; (σ,σ')∈R
⟧ ⟹ c σ ⟷ c' σ'"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ' it' σ'; c σ; c' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACHc S c f σ0 ≤ ⇓R (FOREACHci Φ' S' c' f' σ0')"
unfolding FOREACHc_def
apply (rule FOREACHci_refine_rcg)
apply (rule assms)
apply (rule assms)
apply (rule assms)
apply (erule (4) REFC)
apply (rule TrueI)
apply (rule REFSTEP, assumption+)
done

lemma FOREACHi_refine_rcg'[refine]:
fixes α :: "'S ⇒ 'Sa"
fixes S :: "'S set"
fixes S' :: "'Sa set"
assumes INJ: "inj_on α S"
assumes REFS: "S' = α`S"
assumes REF0: "(σ0,σ0')∈R"
assumes REFSTEP: "⋀x it σ x' it' σ'. ⟦
x'=α x; x∈it; x'∈it'; it'=α`it; it⊆S; it'⊆S';
Φ' it' σ';
(σ,σ')∈R
⟧ ⟹ f x σ ≤ ⇓R (f' x' σ')"
shows "FOREACH S f σ0 ≤ ⇓R (FOREACHi Φ' S' f' σ0')"
unfolding FOREACH_def FOREACHi_def
apply (rule FOREACHci_refine_rcg')
apply (rule assms)+
apply simp
apply (rule REFSTEP, assumption+)
done

subsubsection ‹Alternative set of FOREACHc-rules›
text ‹Here, we provide an alternative set of FOREACH rules with
interruption. In some cases, they are easier to use, as they avoid
redundancy between the final cases for interruption and non-interruption›

lemma FOREACHoci_rule':
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ c σ; x∈it; it⊆S; I it σ; ∀y∈it - {x}. R x y;
∀y∈S - it. R y x ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ; c σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it⊆S; I it σ; ¬c σ;
∀x∈it. ∀y∈S - it. R y x ⟧ ⟹ P σ"
shows "FOREACHoci R I S c f σ0 ≤ SPEC P"
apply (rule FOREACHoci_rule[OF FIN, where I=I, OF I0])
apply (rule IP, assumption+)
apply (case_tac "c σ")
apply (blast intro: II1)
apply (blast intro: II2)
apply (blast intro: II2)
done

lemma FOREACHci_rule'[refine_vcg]:
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ; c σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it⊆S; I it σ; ¬c σ ⟧ ⟹ P σ"
shows "FOREACHci I S c f σ0 ≤ SPEC P"
unfolding FOREACHci_def
by (rule FOREACHoci_rule') (simp_all add: assms)

lemma FOREACHc_rule':
assumes FIN: "finite S"
assumes I0: "I S σ0"
assumes IP:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (it-{x}))"
assumes II1: "⋀σ. ⟦I {} σ; c σ⟧ ⟹ P σ"
assumes II2: "⋀it σ. ⟦ it⊆S; I it σ; ¬c σ ⟧ ⟹ P σ"
shows "FOREACHc S c f σ0 ≤ SPEC P"
unfolding FOREACHc_def
apply (rule order_trans[OF FOREACHci_weaken], rule TrueI)
apply (rule FOREACHci_rule'[where I=I])
using assms by auto

subsection ‹FOREACH with empty sets›

lemma FOREACHoci_emp [simp] :
"FOREACHoci R Φ {} c f σ = do {ASSERT (Φ {} σ); RETURN σ}"
by (simp add: FOREACHoci_def FOREACH_cond_def bind_RES)

lemma FOREACHoi_emp [simp] :
"FOREACHoi R Φ {} f σ = do {ASSERT (Φ {} σ); RETURN σ}"

lemma FOREACHci_emp [simp] :
"FOREACHci Φ {} c f σ = do {ASSERT (Φ {} σ); RETURN σ}"

lemma FOREACHc_emp [simp] :
"FOREACHc {} c f σ = RETURN σ"

lemma FOREACH_emp [simp] :
"FOREACH {} f σ = RETURN σ"

lemma FOREACHi_emp [simp] :
"FOREACHi Φ {} f σ = do {ASSERT (Φ {} σ); RETURN σ}"

subsection "Monotonicity"

(* TODO: Move to RefineG_Domain *)
definition "lift_refl P c f g == ∀x. P c (f x) (g x)"
definition "lift_mono P c f g == ∀x y. c x y ⟶ P c (f x) (g y)"
definition "lift_mono1 P c f g == ∀x y. (∀a. c (x a) (y a)) ⟶ P c (f x) (g y)"
definition "lift_mono2 P c f g == ∀x y. (∀a b. c (x a b) (y a b)) ⟶ P c (f x) (g y)"

definition "trimono_spec L f == ((L id (≤) f f) ∧ (L id flat_ge f f))"

lemmas trimono_atomize = atomize_imp atomize_conj atomize_all
lemmas trimono_deatomize = trimono_atomize[symmetric]

lemmas trimono_spec_defs = trimono_spec_def lift_refl_def[abs_def] comp_def id_def
lift_mono_def[abs_def] lift_mono1_def[abs_def] lift_mono2_def[abs_def]
trimono_deatomize

locale trimono_spec begin
abbreviation "R ≡ lift_refl"
abbreviation "M ≡ lift_mono"
abbreviation "M1 ≡ lift_mono1"
abbreviation "M2 ≡ lift_mono2"
end

context begin interpretation trimono_spec .

lemma FOREACHoci_mono[unfolded trimono_spec_defs,refine_mono]:
"trimono_spec (R o R o R o R o M2 o R) FOREACHoci"
"trimono_spec (R o R o R o M2 o R) FOREACHoi"
"trimono_spec (R o R o R o M2 o R) FOREACHci"
"trimono_spec (R o R o M2 o R) FOREACHc"
"trimono_spec (R o R o M2 o R) FOREACHi"
"trimono_spec (R o M2 o R) FOREACH"
apply (unfold trimono_spec_defs)
apply -
unfolding FOREACHoci_def FOREACH_to_oci_unfold FOREACH_body_def
apply (refine_mono)+
done

end

subsection ‹Nres-Fold with Interruption (nfoldli)›
text ‹
A foreach-loop can be conveniently expressed as an operation that converts
the set to a list, followed by folding over the list.

This representation is handy for automatic refinement, as the complex
foreach-operation is expressed by two relatively simple operations.
›

text ‹We first define a fold-function in the nres-monad›
partial_function (nrec) nfoldli where
"nfoldli l c f s = (case l of
[] ⇒ RETURN s
| x#ls ⇒ if c s then do { s←f x s; nfoldli ls c f s} else RETURN s
)"

lemma nfoldli_simps[simp]:
"nfoldli [] c f s = RETURN s"
"nfoldli (x#ls) c f s =
(if c s then do { s←f x s; nfoldli ls c f s} else RETURN s)"
apply (subst nfoldli.simps, simp)+
done

lemma param_nfoldli[param]:
shows "(nfoldli,nfoldli) ∈
⟨Ra⟩list_rel → (Rb→Id) → (Ra→Rb→⟨Rb⟩nres_rel) → Rb → ⟨Rb⟩nres_rel"
apply (intro fun_relI)
proof goal_cases
case (1 l l' c c' f f' s s')
thus ?case
apply (induct arbitrary: s s')
apply (simp only: nfoldli_simps True_implies_equals)
apply parametricity
apply (simp only: nfoldli_simps True_implies_equals)
apply (parametricity)
done
qed

lemma nfoldli_no_ctd[simp]: "¬ctd s ⟹ nfoldli l ctd f s = RETURN s"
by (cases l) auto

lemma nfoldli_append[simp]: "nfoldli (l1@l2) ctd f s = nfoldli l1 ctd f s ⤜ nfoldli l2 ctd f"
by (induction l1 arbitrary: s) (auto simp: pw_eq_iff refine_pw_simps)

lemma nfoldli_map: "nfoldli (map f l) ctd g s = nfoldli l ctd (g o f) s"
apply (induction l arbitrary: s)
by (auto simp: pw_eq_iff refine_pw_simps)

lemma nfoldli_nfoldli_prod_conv:
"nfoldli l2 ctd (λi. nfoldli l1 ctd (f i)) s = nfoldli (List.product l2 l1) ctd (λ(i,j). f i j) s"
proof -
have [simp]: "nfoldli (map (Pair a) l) ctd (λ(x, y). f x y) s = nfoldli l ctd (f a) s"
for a l s
apply (induction l arbitrary: s)
by (auto simp: pw_eq_iff refine_pw_simps)

show ?thesis
by (induction l2 arbitrary: l1 s) auto
qed

text ‹The fold-function over the nres-monad is transfered to a plain
foldli function›
lemma nfoldli_transfer_plain[refine_transfer]:
assumes "⋀x s. RETURN (f x s) ≤ f' x s"
shows "RETURN (foldli l c f s) ≤ (nfoldli l c f' s)"
using assms
apply (induct l arbitrary: s)
apply (auto)
by (metis (lifting) plain_bind)

lemma nfoldli_transfer_dres[refine_transfer]:
fixes l :: "'a list" and c:: "'b ⇒ bool"
assumes FR: "⋀x s. nres_of (f x s) ≤ f' x s"
shows "nres_of
(foldli l (case_dres False False c) (λx s. s⤜f x) (dRETURN s))
≤ (nfoldli l c f' s)"
proof (induct l arbitrary: s)
case Nil thus ?case by auto
next
case (Cons a l)
thus ?case
apply (auto)
apply (cases "f a s")
apply (cases l, simp_all) []
apply simp
apply (rule order_trans[rotated])
apply (rule bind_mono)
apply (rule FR)
apply assumption
apply simp
apply simp
using FR[of a s]
apply simp
done
qed

lemma nfoldli_mono[refine_mono]:
"⟦ ⋀x s. f x s ≤ f' x s ⟧ ⟹ nfoldli l c f σ ≤ nfoldli l c f' σ"
"⟦ ⋀x s. flat_ge (f x s) (f' x s) ⟧ ⟹ flat_ge (nfoldli l c f σ) (nfoldli l c f' σ)"
apply (induct l arbitrary: σ)
apply auto
apply refine_mono

apply (induct l arbitrary: σ)
apply auto
apply refine_mono
done

text ‹We relate our fold-function to the while-loop that we used in
the original definition of the foreach-loop›
lemma nfoldli_while: "nfoldli l c f σ
≤
(WHILE⇩T⇗I⇖
(FOREACH_cond c) (FOREACH_body f) (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_nfoldli:
"do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (FOREACH_body f) (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)
done

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

lemma nfoldli_rule:
assumes I0: "I [] l0 σ0"
assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (l1@[x]) l2)"
assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"
assumes FC: "⋀σ. ⟦ I l0 [] σ; c σ ⟧ ⟹ P σ"
shows "nfoldli l0 c f σ0 ≤ SPEC P"
apply (rule order_trans[OF nfoldli_while[
where I="λ(l2,σ). ∃l1. l0=l1@l2 ∧ I l1 l2 σ"]])
unfolding FOREACH_cond_def FOREACH_body_def
apply (refine_rcg WHILEIT_rule[where R="measure (length o fst)"] refine_vcg)
apply simp
using I0 apply simp

apply (case_tac a, simp)
apply simp
apply (elim exE conjE)
apply (rule order_trans[OF IS], assumption+)
apply auto []

apply simp
apply (elim exE disjE2)
using FC apply auto []
using FNC apply auto []
done

lemma nfoldli_leof_rule:
assumes I0: "I [] l0 σ0"
assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤⇩n SPEC (I (l1@[x]) l2)"
assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"
assumes FC: "⋀σ. ⟦ I l0 [] σ; c σ ⟧ ⟹ P σ"
shows "nfoldli l0 c f σ0 ≤⇩n SPEC P"
proof -
{
fix l1 l2 σ
assume "l0=l1@l2" "I l1 l2 σ"
hence "nfoldli l2 c f σ ≤⇩n SPEC P"
proof (induction l2 arbitrary: l1 σ)
case Nil thus ?case
apply simp
apply (cases "c σ")
apply (rule FC; auto; fail)
apply (rule FNC[of l1 "[]"]; auto; fail)
done
next
case (Cons x l2)
note [refine_vcg] = Cons.IH[of "l1@[x]",THEN leof_trans] IS[of l1 x l2 σ,THEN leof_trans]

show ?case
apply (simp split del: if_split)
apply refine_vcg
using Cons.prems FNC by auto
qed
} from this[of "[]" l0 σ0] I0 show ?thesis by auto
qed

lemma nfoldli_refine[refine]:
assumes "(li, l) ∈ ⟨S⟩list_rel"
and "(si, s) ∈ R"
and CR: "(ci, c) ∈ R → bool_rel"
and [refine]: "⋀xi x si s. ⟦ (xi,x)∈S; (si,s)∈R; c s ⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
shows "nfoldli li ci fi si ≤ ⇓ R (nfoldli l c f s)"
using assms(1,2)
proof (induction arbitrary: si s rule: list_rel_induct)
case Nil thus ?case by simp
next
case (Cons xi x li l)
note [refine] = Cons

show ?case
apply (simp split del: if_split)
apply refine_rcg
using CR Cons.prems by (auto dest: fun_relD)
qed

(* Refine, establishing additional invariant *)
lemma nfoldli_invar_refine:
assumes "(li,l)∈⟨S⟩list_rel"
assumes "(si,s)∈R"
assumes "I [] li si"
assumes COND: "⋀l1i l2i l1 l2 si s. ⟦
li=l1i@l2i; l=l1@l2; (l1i,l1)∈⟨S⟩list_rel; (l2i,l2)∈⟨S⟩list_rel;
I l1i l2i si; (si,s)∈R⟧ ⟹ (ci si, c s)∈bool_rel"
assumes INV: "⋀l1i xi l2i si. ⟦li=l1i@xi#l2i; I l1i (xi#l2i) si⟧ ⟹ fi xi si ≤⇩n SPEC (I (l1i@[xi]) l2i)"
assumes STEP: "⋀l1i xi l2i l1 x l2 si s. ⟦
li=l1i@xi#l2i; l=l1@x#l2; (l1i,l1)∈⟨S⟩list_rel; (xi,x)∈S; (l2i,l2)∈⟨S⟩list_rel;
I l1i (xi#l2i) si; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
shows "nfoldli li ci fi si ≤ ⇓R (nfoldli l c f s)"
proof -
{
have [refine_dref_RELATES]: "RELATES R" "RELATES S" by (auto simp: RELATES_def)

note [refine del] = nfoldli_refine

fix l1i l2i l1 l2 si s
assume "(l2i,l2) ∈ ⟨S⟩list_rel" "(l1i,l1) ∈ ⟨S⟩list_rel"
and "li=l1i@l2i" "l=l1@l2"
and "(si,s)∈R" "I l1i l2i si"
hence "nfoldli l2i ci fi si ≤ ⇓R (nfoldli l2 c f s)"
proof (induction arbitrary: si s l1i l1 rule: list_rel_induct)
case Nil thus ?case by auto
next
case (Cons xi x l2i l2)

show ?case
apply (simp split del: if_split)
apply (refine_rcg bind_refine')
apply (refine_dref_type)
subgoal using COND[of l1i "xi#l2i" l1 "x#l2" si s] Cons.prems Cons.hyps by auto
subgoal apply (rule STEP) using Cons.prems Cons.hyps by auto
subgoal for si' s'
apply (rule Cons.IH[of "l1i@[xi]" "l1@[x]"])
using Cons.prems Cons.hyps
apply (auto simp: list_rel_append1) apply force
using INV[of l1i xi l2i si]
by (auto simp: pw_leof_iff)
subgoal using Cons.prems by simp
done
qed
}
from this[of li l "[]" "[]" si s] assms(1,2,3) show ?thesis by auto
qed

lemma foldli_mono_dres_aux1:
fixes σ :: "'a :: {order_bot, order_top}"
assumes COND: "⋀σ σ'. σ≤σ' ⟹ c σ ≠ c σ' ⟹ σ=bot ∨ σ'=top "
assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
assumes B: "σ≤σ'"
assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
shows "foldli l c f σ ≤ foldli l c f' σ'"
proof -
{ fix l
have "foldli l c f bot = bot" by (induct l) (auto simp: STRICT)
} note [simp] = this
{ fix l
have "foldli l c f' top = top" by (induct l) (auto simp: STRICT)
} note [simp] = this

show ?thesis
using B
apply (induct l arbitrary: σ σ')
apply (auto simp: A STRICT dest!: COND)
done
qed

lemma foldli_mono_dres_aux2:
assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
shows "foldli l (case_dres False False c) f σ
≤ foldli l (case_dres False False c) f' σ"
apply (rule foldli_mono_dres_aux1)
apply (simp_all split: dres.split_asm add: STRICT A)
done

lemma foldli_mono_dres[refine_mono]:
assumes A: "⋀a x. f a x ≤ f' a x"
shows "foldli l (case_dres False False c) (λx s. dbind s (f x)) σ
≤ foldli l (case_dres False False c) (λx s. dbind s (f' x)) σ"
apply (rule foldli_mono_dres_aux2)
apply (simp_all)
apply (rule dbind_mono)
done

partial_function (drec) dfoldli where
"dfoldli l c f s = (case l of
[] ⇒ dRETURN s
| x#ls ⇒ if c s then do { s←f x s; dfoldli ls c f s} else dRETURN s
)"

lemma dfoldli_simps[simp]:
"dfoldli [] c f s = dRETURN s"
"dfoldli (x#ls) c f s =
(if c s then do { s←f x s; dfoldli ls c f s} else dRETURN s)"
apply (subst dfoldli.simps, simp)+
done

lemma dfoldli_mono[refine_mono]:
"⟦ ⋀x s. f x s ≤ f' x s ⟧ ⟹ dfoldli l c f σ ≤ dfoldli l c f' σ"
"⟦ ⋀x s. flat_ge (f x s) (f' x s) ⟧ ⟹ flat_ge (dfoldli l c f σ) (dfoldli l c f' σ)"
apply (induct l arbitrary: σ)
apply auto
apply refine_mono

apply (induct l arbitrary: σ)
apply auto
apply refine_mono
done

lemma foldli_dres_pres_FAIL[simp]:
"foldli l (case_dres False False c) (λx s. dbind s (f x)) dFAIL = dFAIL"
by (cases l) auto

lemma foldli_dres_pres_SUCCEED[simp]:
"foldli l (case_dres False False c) (λx s. dbind s (f x)) dSUCCEED = dSUCCEED"
by (cases l) auto

lemma dfoldli_by_foldli: "dfoldli l c f σ
= foldli l (case_dres False False c) (λx s. dbind s (f x)) (dRETURN σ)"
apply (induction l arbitrary: σ)
apply simp
apply (clarsimp intro!: ext)
apply (rename_tac a l x)
apply (case_tac "f a x")
apply auto
done

lemma foldli_mono_dres_flat[refine_mono]:
assumes A: "⋀a x. flat_ge (f a x) (f' a x)"
shows "flat_ge (foldli l (case_dres False False c) (λx s. dbind s (f x)) σ)
(foldli l (case_dres False False c) (λx s. dbind s (f' x)) σ)"
apply (cases σ)
using A apply refine_mono
done

lemma dres_foldli_ne_bot[refine_transfer]:
assumes 1: "σ ≠ dSUCCEED"
assumes 2: "⋀x σ. f x σ ≠ dSUCCEED"
shows "foldli l c (λx s. s ⤜ f x) σ ≠ dSUCCEED"
using 1 apply (induct l arbitrary: σ)
apply simp
apply (simp split: dres.split, intro allI impI)
apply rprems
using 2
done

subsection ‹LIST FOREACH combinator›
text ‹
Foreach-loops are mapped to the combinator ‹LIST_FOREACH›, that
takes as first argument an explicit ‹to_list› operation.
This mapping is done during operation identification.
It is then the responsibility of the various implementations to further map
the ‹to_list› operations to custom ‹to_list› operations, like
‹set_to_list›, ‹map_to_list›, ‹nodes_to_list›, etc.
›

text ‹We define a relation between distinct lists and sets.›
definition [to_relAPP]: "list_set_rel R ≡ ⟨R⟩list_rel O br set distinct"

lemma autoref_nfoldli[autoref_rules]:
shows "(nfoldli, nfoldli)
∈ ⟨Ra⟩list_rel → (Rb → bool_rel) → (Ra → Rb → ⟨Rb⟩nres_rel) → Rb → ⟨Rb⟩nres_rel"
by (rule param_nfoldli)

text ‹This constant is a placeholder to be converted to
custom operations by pattern rules›
definition "it_to_sorted_list R s
≡ SPEC (λl. distinct l ∧ s = set l ∧ sorted_wrt R l)"

definition "LIST_FOREACH Φ tsl c f σ0 ≡ do {
xs ← tsl;
(_,σ) ← WHILE⇩T⇗λ(it, σ). ∃xs'. xs = xs' @ it ∧ Φ (set it) σ⇖
(FOREACH_cond c) (FOREACH_body f) (xs, σ0);
RETURN σ}"

lemma FOREACHoci_by_LIST_FOREACH:
"FOREACHoci R Φ S c f σ0 = do {
ASSERT (finite S);
LIST_FOREACH Φ (it_to_sorted_list R S) c f σ0
}"
unfolding OP_def FOREACHoci_def LIST_FOREACH_def it_to_sorted_list_def
by simp

text ‹Patterns that convert FOREACH-constructs
to ‹LIST_FOREACH›
›
context begin interpretation autoref_syn .

lemma FOREACH_patterns[autoref_op_pat_def]:
"FOREACH⇗I⇖ s f ≡ FOREACH⇩O⇩C⇗λ_ _. True,I⇖ s (λ_. True) f"
"FOREACHci I s c f ≡ FOREACHoci (λ_ _. True) I s c f"
"FOREACH⇩O⇩C⇗R,Φ⇖ s c f ≡ λσ. do {
ASSERT (finite s);
Autoref_Tagging.OP (LIST_FOREACH Φ) (it_to_sorted_list R s) c f σ
}"
"FOREACH s f ≡ FOREACHoci (λ_ _. True) (λ_ _. True) s (λ_. True) f"
"FOREACHoi R I s f ≡ FOREACHoci R I s (λ_. True) f"
"FOREACHc s c f ≡ FOREACHoci (λ_ _. True) (λ_ _. True) s c f"
unfolding
FOREACHoci_by_LIST_FOREACH[abs_def]
FOREACHc_def[abs_def]
FOREACH_def[abs_def]
FOREACHci_def[abs_def]
FOREACHi_def[abs_def]
FOREACHoi_def[abs_def]
by simp_all

(*lemma FOREACH_patterns[autoref_op_pat]:
"FOREACHoci R Φ s c f σ ≡ do {
ASSERT (finite s);
OP (LIST_FOREACH Φ) (it_to_sorted_list R s) c f σ
}"
"FOREACHc s c f σ ≡ FOREACHoci (λ_ _. True) (λ_ _. True) s c f σ"
"FOREACH s f σ ≡ FOREACHoci (λ_ _. True) (λ_ _. True) s (λ_. True) f σ"
"FOREACHci I s c f σ ≡ FOREACHoci (λ_ _. True) I s c f σ"
"FOREACHi I s f σ ≡ FOREACHoci (λ_ _. True) I s (λ_. True) f σ"
"FOREACHoi R I s f σ ≡ FOREACHoci R I s (λ_. True) f σ"
unfolding
FOREACHoci_by_LIST_FOREACH[abs_def]
FOREACHc_def[abs_def]
FOREACH_def[abs_def]
FOREACHci_def[abs_def]
FOREACHi_def[abs_def]
FOREACHoi_def[abs_def]
by simp_all*)
end
definition "LIST_FOREACH' tsl c f σ ≡ do {xs ← tsl; nfoldli xs c f σ}"

lemma LIST_FOREACH'_param[param]:
shows "(LIST_FOREACH',LIST_FOREACH')
∈ (⟨⟨Rv⟩list_rel⟩nres_rel → (Rσ→bool_rel)
→ (Rv → Rσ → ⟨Rσ⟩nres_rel) → Rσ → ⟨Rσ⟩nres_rel)"
unfolding LIST_FOREACH'_def[abs_def]
by parametricity

lemma LIST_FOREACH_autoref[autoref_rules]:
shows "(LIST_FOREACH', LIST_FOREACH Φ) ∈
(⟨⟨Rv⟩list_rel⟩nres_rel → (Rσ→bool_rel)
→ (Rv → Rσ → ⟨Rσ⟩nres_rel) → Rσ → ⟨Rσ⟩nres_rel)"
proof (intro fun_relI nres_relI)
fix tsl tsl' c c' f f' σ σ'
assume [param]:
"(tsl,tsl')∈⟨⟨Rv⟩list_rel⟩nres_rel"
"(c,c')∈Rσ→bool_rel"
"(f,f')∈Rv→Rσ→⟨Rσ⟩nres_rel"
"(σ,σ')∈Rσ"

have "LIST_FOREACH' tsl c f σ ≤ ⇓Rσ (LIST_FOREACH' tsl' c' f' σ')"
apply (rule nres_relD)
by parametricity
also have "LIST_FOREACH' tsl' c' f' σ'
≤ LIST_FOREACH Φ tsl' c' f' σ'"
apply (rule refine_IdD)
unfolding LIST_FOREACH_def LIST_FOREACH'_def
apply refine_rcg
apply simp
apply (rule nfoldli_while)
done
finally show
"LIST_FOREACH' tsl c f σ ≤ ⇓ Rσ (LIST_FOREACH Φ tsl' c' f' σ')"
.
qed

context begin interpretation trimono_spec .

lemma LIST_FOREACH'_mono[unfolded trimono_spec_defs,refine_mono]:
"trimono_spec (R o R o M2 o R) LIST_FOREACH'"
apply (unfold trimono_spec_defs)
apply -
unfolding LIST_FOREACH'_def
by refine_mono+

end

lemma LIST_FOREACH'_transfer_plain[refine_transfer]:
assumes "RETURN tsl ≤ tsl'"
assumes "⋀x σ. RETURN (f x σ) ≤ f' x σ"
shows "RETURN (foldli tsl c f σ) ≤ LIST_FOREACH' tsl' c f' σ"
apply (rule order_trans[rotated])
unfolding LIST_FOREACH'_def
using assms
apply refine_transfer
by simp

thm refine_transfer

lemma LIST_FOREACH'_transfer_nres[refine_transfer]:
assumes "nres_of tsl ≤ tsl'"
assumes "⋀x σ. nres_of (f x σ) ≤ f' x σ"
shows "nres_of (
do {
xs←tsl;
foldli xs (case_dres False False c) (λx s. s⤜f x) (dRETURN σ)
}) ≤ LIST_FOREACH' tsl' c f' σ"
unfolding LIST_FOREACH'_def
using assms
by refine_transfer

text ‹Simplification rules to summarize iterators›
lemma [refine_transfer_post_simp]:
"do {
xs ← dRETURN tsl;
foldli xs c f σ
} = foldli tsl c f σ"
by simp

lemma [refine_transfer_post_simp]:
"(let xs = tsl in foldli xs c f σ) = foldli tsl c f σ"
by simp

lemma LFO_pre_refine: (* TODO: Generalize! *)
assumes "(li,l)∈⟨A⟩list_set_rel"
assumes "(ci,c)∈R → bool_rel"
assumes "(fi,f)∈A→R→⟨R⟩nres_rel"
assumes "(s0i,s0)∈R"
shows "LIST_FOREACH' (RETURN li) ci fi s0i ≤ ⇓R (FOREACHci I l c f s0)"
proof -
from assms(1) have [simp]: "finite l" by (auto simp: list_set_rel_def br_def)
show ?thesis
unfolding FOREACHc_def FOREACHci_def FOREACHoci_by_LIST_FOREACH
apply simp
apply (rule LIST_FOREACH_autoref[param_fo, THEN nres_relD])
using assms
apply auto
apply (auto simp: it_to_sorted_list_def nres_rel_def pw_le_iff refine_pw_simps
list_set_rel_def br_def)
done
qed

lemma LFOci_refine: (* TODO: Generalize! *)
assumes "(li,l)∈⟨A⟩list_set_rel"
assumes "⋀s si. (si,s)∈R ⟹ ci si ⟷ c s"
assumes "⋀x xi s si. ⟦(xi,x)∈A; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
assumes "(s0i,s0)∈R"
shows "nfoldli li ci fi s0i ≤ ⇓R (FOREACHci I l c f s0)"
proof -
from assms LFO_pre_refine[of li l A ci c R fi f s0i s0] show ?thesis
unfolding fun_rel_def nres_rel_def LIST_FOREACH'_def
apply blast+
done
qed

lemma LFOc_refine: (* TODO: Generalize! *)
assumes "(li,l)∈⟨A⟩list_set_rel"
assumes "⋀s si. (si,s)∈R ⟹ ci si ⟷ c s"
assumes "⋀x xi s si. ⟦(xi,x)∈A; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
assumes "(s0i,s0)∈R"
shows "nfoldli li ci fi s0i ≤ ⇓R (FOREACHc l c f s0)"
unfolding FOREACHc_def
by (rule LFOci_refine[OF assms])

lemma LFO_refine: (* TODO: Generalize! *)
assumes "(li,l)∈⟨A⟩list_set_rel"
assumes "⋀x xi s si. ⟦(xi,x)∈A; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
assumes "(s0i,s0)∈R"
shows "nfoldli li (λ_. True) fi s0i ≤ ⇓R (FOREACH l f s0)"
unfolding FOREACH_def
apply (rule LFOc_refine)
apply (rule assms | simp)+
done

lemma LFOi_refine: (* TODO: Generalize! *)
assumes "(li,l)∈⟨A⟩list_set_rel"
assumes "⋀x xi s si. ⟦(xi,x)∈A; (si,s)∈R⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
assumes "(s0i,s0)∈R"
shows "nfoldli li (λ_. True) fi s0i ≤ ⇓R (FOREACHi I l f s0)"
unfolding FOREACHi_def
apply (rule LFOci_refine)
apply (rule assms | simp)+
done

lemma LIST_FOREACH'_refine: "LIST_FOREACH' tsl' c' f' σ' ≤ LIST_FOREACH Φ tsl' c' f' σ'"
apply (rule refine_IdD)
unfolding LIST_FOREACH_def LIST_FOREACH'_def
apply refine_rcg
apply simp
apply (rule nfoldli_while)
done

lemma LIST_FOREACH'_eq: "LIST_FOREACH (λ_ _. True) tsl' c' f' σ' = (LIST_FOREACH' tsl' c' f' σ')"
apply (rule antisym)
subgoal
apply (rule refine_IdD)
unfolding LIST_FOREACH_def LIST_FOREACH'_def while_eq_nfoldli[symmetric]
apply (refine_rcg WHILEIT_refine_new_invar)
unfolding WHILET_def
apply (rule WHILEIT_refine_new_invar)

apply refine_dref_type
apply clarsimp_all
unfolding FOREACH_body_def FOREACH_cond_def
apply refine_vcg
apply (auto simp: refine_pw_simps pw_le_iff neq_Nil_conv)
done
subgoal by (rule LIST_FOREACH'_refine)
done

subsection ‹FOREACH with duplicates›

definition "FOREACHcd S c f σ ≡ do {
ASSERT (finite S);
l ← SPEC (λl. set l = S);
nfoldli l c f σ
}"

lemma FOREACHcd_rule:
assumes "finite S⇩0"
assumes I0: "I {} S⇩0 σ⇩0"
assumes STEP: "⋀S1 S2 x σ. ⟦ S⇩0 = insert x (S1∪S2); I S1 (insert x S2) σ; c σ ⟧ ⟹ f x σ ≤ SPEC (I (insert x S1) S2)"
assumes INTR: "⋀S1 S2 σ. ⟦ S⇩0 = S1∪S2; I S1 S2 σ; ¬c σ ⟧ ⟹ Φ σ"
assumes COMPL: "⋀σ. ⟦ I S⇩0 {} σ; c σ ⟧ ⟹ Φ σ"
shows "FOREACHcd S⇩0 c f σ⇩0 ≤ SPEC Φ"
unfolding FOREACHcd_def
apply refine_vcg
apply fact
apply (rule nfoldli_rule[where I = "λl1 l2 σ. I (set l1) (set l2) σ"])
subgoal using I0 by auto
subgoal using STEP by auto
subgoal using INTR by auto
subgoal using COMPL by auto
done

```