# Theory SetIteratorOperations

```(*  Title:       Operations on Iterators over Finite Sets
Author:      Thomas Tuerk <tuerk@in.tum.de>
Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹Operations on Set Iterators›
theory SetIteratorOperations
imports Main SetIterator
begin

text‹Many operations on sets can be lifted to iterators over sets. This theory tries to introduce
the most useful such operations.›

subsection ‹Empty set›

text ‹Iterators over empty sets and singleton sets are very easy to define.›
definition set_iterator_emp :: "('a,'σ) set_iterator" where
"set_iterator_emp c f σ0 = σ0"

lemma set_iterator_emp_foldli_conv :
"set_iterator_emp = foldli []"

lemma set_iterator_genord_emp_correct :
"set_iterator_genord set_iterator_emp {} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[]"])
done

lemma set_iterator_emp_correct :
"set_iterator set_iterator_emp {}"
using set_iterator_intro [OF set_iterator_genord_emp_correct] .

lemma (in linorder) set_iterator_linord_emp_correct :
"set_iterator_linord set_iterator_emp {}"
unfolding set_iterator_linord_def
by (fact set_iterator_genord_emp_correct)

lemma (in linorder) set_iterator_rev_linord_emp_correct :
"set_iterator_rev_linord set_iterator_emp {}"
unfolding set_iterator_rev_linord_def
by (fact set_iterator_genord_emp_correct)

lemma (in linorder) map_iterator_linord_emp_correct :
"map_iterator_linord set_iterator_emp Map.empty"
"set_iterator_map_linord set_iterator_emp {}"
unfolding set_iterator_map_linord_def

lemma (in linorder) map_iterator_rev_linord_emp_correct :
"map_iterator_rev_linord set_iterator_emp Map.empty"
"set_iterator_map_rev_linord set_iterator_emp {}"
unfolding set_iterator_map_rev_linord_def

subsection‹Singleton Sets›

definition set_iterator_sng :: "'a ⇒ ('a,'σ) set_iterator" where
"set_iterator_sng x c f σ0 = (if c σ0 then f x σ0 else σ0)"

lemma set_iterator_sng_foldli_conv :
"set_iterator_sng x = foldli [x]"

lemma set_iterator_genord_sng_correct :
"set_iterator_genord (set_iterator_sng (x::'a)) {x} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[x]"])
done

lemma set_iterator_sng_correct :
"set_iterator (set_iterator_sng x) {x}"
unfolding set_iterator_def
by (rule set_iterator_genord_sng_correct)

lemma (in linorder) set_iterator_linord_sng_correct :
"set_iterator_linord (set_iterator_sng x) {x}"
unfolding set_iterator_linord_def

lemma (in linorder) set_iterator_rev_linord_sng_correct :
"set_iterator_rev_linord (set_iterator_sng x) {x}"
unfolding set_iterator_rev_linord_def

lemma (in linorder) map_iterator_linord_sng_correct :
"map_iterator_linord (set_iterator_sng (k,v)) (Map.empty (k ↦ v))"
unfolding set_iterator_map_linord_def

lemma (in linorder) map_iterator_rev_linord_sng_correct :
"map_iterator_rev_linord (set_iterator_sng (k,v)) (Map.empty (k ↦ v))"
unfolding set_iterator_map_rev_linord_def

subsection ‹Union›

text ‹Iterators over disjoint sets can be combined by first iterating over one and then the
other set. The result is an iterator over the union of the original sets.›

definition set_iterator_union ::
"('a,'σ) set_iterator ⇒ ('a, 'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
"set_iterator_union it_a it_b ≡ λc f σ0. (it_b c f (it_a c f σ0))"

lemma set_iterator_union_foldli_conv :
"set_iterator_union (foldli as) (foldli bs) = foldli (as @ bs)"
by (simp add: fun_eq_iff set_iterator_union_def foldli_append)

lemma set_iterator_genord_union_correct :
fixes it_a :: "('a,'σ) set_iterator"
fixes it_b :: "('a,'σ) set_iterator"
fixes R S_a S_b
assumes it_a: "set_iterator_genord it_a S_a R"
assumes it_b: "set_iterator_genord it_b S_b R"
assumes dist_Sab: "S_a ∩ S_b = {}"
assumes R_OK: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ R a b"
shows "set_iterator_genord (set_iterator_union it_a it_b) (S_a ∪ S_b) R"
proof -
from it_a obtain as where
dist_as: "distinct as" and S_a_eq: "S_a = set as" and
sorted_as: "sorted_wrt R as" and it_a_eq: "it_a = foldli as"
unfolding set_iterator_genord_foldli_conv by blast

from it_b obtain bs where
dist_bs: "distinct bs" and S_b_eq: "S_b = set bs" and
sorted_bs: "sorted_wrt R bs" and it_b_eq: "it_b = foldli bs"
unfolding set_iterator_genord_foldli_conv by blast

show ?thesis
proof (rule set_iterator_genord_I [of "as @ bs"])
from dist_Sab S_a_eq S_b_eq dist_as dist_bs
show "distinct (as @ bs)" by simp
next
from S_a_eq S_b_eq
show "S_a ∪ S_b = set (as @ bs)" by simp
next
from sorted_as sorted_bs R_OK S_a_eq S_b_eq
show "sorted_wrt R (as @ bs)"
next
show "set_iterator_union it_a it_b = (foldli (as @ bs))"
unfolding it_a_eq it_b_eq set_iterator_union_foldli_conv by simp
qed
qed

lemma set_iterator_union_emp [simp] :
"set_iterator_union (set_iterator_emp) it = it"
"set_iterator_union it (set_iterator_emp) = it"
unfolding set_iterator_emp_def set_iterator_union_def
by simp_all

lemma set_iterator_union_correct :
assumes it_a: "set_iterator it_a S_a"
assumes it_b: "set_iterator it_b S_b"
assumes dist_Sab: "S_a ∩ S_b = {}"
shows "set_iterator (set_iterator_union it_a it_b) (S_a ∪ S_b)"
proof -
note res' = set_iterator_genord_union_correct [OF it_a[unfolded set_iterator_def]
it_b[unfolded set_iterator_def] dist_Sab]
from set_iterator_intro [OF res']
show ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_union_correct :
assumes it_a: "set_iterator_linord it_a S_a"
assumes it_b: "set_iterator_linord it_b S_b"
assumes ord_Sab: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ a < b"
shows "set_iterator_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_linord_def
apply (rule_tac set_iterator_genord_union_correct[
OF it_a[unfolded set_iterator_linord_def] it_b[unfolded set_iterator_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) set_iterator_rev_linord_union_correct :
assumes it_a: "set_iterator_rev_linord it_a S_a"
assumes it_b: "set_iterator_rev_linord it_b S_b"
assumes ord_Sab: "⋀a b. ⟦a ∈ S_a; b ∈ S_b⟧ ⟹ a > b"
shows "set_iterator_rev_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_rev_linord_def
apply (rule_tac set_iterator_genord_union_correct[
OF it_a[unfolded set_iterator_rev_linord_def] it_b[unfolded set_iterator_rev_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) map_iterator_linord_union_correct :
assumes it_a: "set_iterator_map_linord it_a S_a"
assumes it_b: "set_iterator_map_linord it_b S_b"
assumes ord_Sab: "⋀kv kv'. ⟦kv ∈ S_a; kv' ∈ S_b⟧ ⟹ fst kv < fst kv'"
shows "set_iterator_map_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_map_linord_def
apply (rule set_iterator_genord_union_correct [OF
it_a[unfolded set_iterator_map_linord_def]
it_b[unfolded set_iterator_map_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le)
done

lemma (in linorder) map_iterator_rev_linord_union_correct :
assumes it_a: "set_iterator_map_rev_linord it_a S_a"
assumes it_b: "set_iterator_map_rev_linord it_b S_b"
assumes ord_Sab: "⋀kv kv'. ⟦kv ∈ S_a; kv' ∈ S_b⟧ ⟹ fst kv > fst kv'"
shows "set_iterator_map_rev_linord (set_iterator_union it_a it_b) (S_a ∪ S_b)"
unfolding set_iterator_map_rev_linord_def
apply (rule set_iterator_genord_union_correct [OF
it_a[unfolded set_iterator_map_rev_linord_def]
it_b[unfolded set_iterator_map_rev_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le)
done

subsection ‹Product›

definition set_iterator_product ::
"('a,'σ) set_iterator ⇒ ('a ⇒ ('b,'σ) set_iterator) ⇒ ('a × 'b ,'σ) set_iterator" where
"set_iterator_product it_a it_b ≡ λc f σ0.
it_a c (
λa σ. it_b a c (λb σ. f (a,b) σ) σ
) σ0"

lemma set_iterator_product_foldli_conv:
"set_iterator_product (foldli as) (λa. foldli (bs a)) =
foldli (concat (map (λa. map (λb. (a, b)) (bs a)) as))"
apply (induct as)
apply (simp add: set_iterator_product_def foldli_append foldli_map o_def fun_eq_iff)
done

lemma set_iterator_product_it_b_cong:
assumes it_a_OK: "set_iterator it_a S_a"
and it_b_b': "⋀a. a ∈ S_a ⟹ it_b a = it_b' a"
shows "set_iterator_product it_a it_b =
set_iterator_product it_a it_b'"
proof -
from it_a_OK obtain as where
dist_as: "distinct as" and S_a_eq: "S_a = set as" and
it_a_eq: "it_a = foldli as"
unfolding set_iterator_foldli_conv by blast

from it_b_b'[unfolded S_a_eq]
show ?thesis unfolding it_a_eq
by (induct as)
qed

definition set_iterator_product_order ::
"('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ 'b ⇒ bool) ⇒
('a × 'b) ⇒ ('a × 'b) ⇒ bool" where
"set_iterator_product_order R_a R_b ab ab' ⟷
(if (fst ab = fst ab') then R_b (fst ab) (snd ab) (snd ab') else
R_a (fst ab) (fst ab'))"

lemma set_iterator_genord_product_correct :
fixes it_a :: "('a,'σ) set_iterator"
fixes it_b :: "'a ⇒ ('b,'σ) set_iterator"
assumes it_a: "set_iterator_genord it_a S_a R_a"
assumes it_b: "⋀a. a ∈ S_a ⟹ set_iterator_genord (it_b a) (S_b a) (R_b a)"
shows "set_iterator_genord (set_iterator_product it_a it_b) (Sigma S_a S_b)
(set_iterator_product_order R_a R_b)"
proof -
from it_a obtain as where
dist_as: "distinct as" and S_a_eq: "S_a = set as" and
sorted_as: "sorted_wrt R_a as" and it_a_eq: "it_a = foldli as"
unfolding set_iterator_genord_foldli_conv by blast

from it_b obtain bs where
dist_bs: "⋀a. a ∈ set as ⟹ distinct (bs a)" and S_b_eq: "⋀a. a ∈ set as ⟹  S_b a = set (bs a)" and
sorted_bs: "⋀a. a ∈ set as ⟹ sorted_wrt (R_b a) (bs a)" and
it_b_eq: "⋀a. a ∈ set as ⟹ it_b a = foldli (bs a)"
unfolding set_iterator_genord_foldli_conv by (metis S_a_eq)

let ?abs = "concat (map (λa. map (λb. (a, b)) (bs a)) as)"

show ?thesis
proof (rule set_iterator_genord_I[of ?abs])
from set_iterator_product_it_b_cong[of it_a S_a it_b,
OF set_iterator_intro[OF it_a] it_b_eq] it_a_eq S_a_eq
have "set_iterator_product it_a it_b =
set_iterator_product (foldli as) (λa. foldli (bs a))" by simp
thus "set_iterator_product it_a it_b = foldli ?abs"
next
show "distinct ?abs"
using dist_as dist_bs[unfolded S_a_eq]
by (induct as)
(simp_all add: distinct_map inj_on_def dist_bs set_eq_iff image_iff)
next
show "Sigma S_a S_b = set ?abs"
unfolding S_a_eq using S_b_eq
by (induct as) auto
next
from sorted_as sorted_bs dist_as
show "sorted_wrt
(set_iterator_product_order R_a R_b)
(concat (map (λa. map (Pair a) (bs a)) as))"
proof (induct as rule: list.induct)
case Nil thus ?case by simp
next
case (Cons a as)
from Cons(2) have R_a_as: "⋀a'. a' ∈ set as ⟹ R_a a a'" and
sorted_as: "sorted_wrt R_a as" by simp_all
from Cons(3) have sorted_bs_a: "sorted_wrt (R_b a) (bs a)"
and sorted_bs_as: "⋀a. a ∈ set as ⟹ sorted_wrt (R_b a) (bs a)" by simp_all
from Cons(4) have dist_as: "distinct as" and a_nin_as: "a ∉ set as" by simp_all
note ind_hyp = Cons(1)[OF sorted_as sorted_bs_as dist_as]

define bs_a where "bs_a = bs a"
from sorted_bs_a
have sorted_prod_a : "sorted_wrt (set_iterator_product_order R_a R_b) (map (Pair a) (bs a))"
unfolding bs_a_def[symmetric]
apply (induct bs_a rule: list.induct)
apply (simp_all add: set_iterator_product_order_def Ball_def image_iff)
done

show ?case
apply (simp add: sorted_wrt_append ind_hyp sorted_prod_a)
apply (simp add: set_iterator_product_order_def R_a_as a_nin_as)
done
qed
qed
qed

lemma set_iterator_product_correct :
assumes it_a: "set_iterator it_a S_a"
assumes it_b: "⋀a. a ∈ S_a ⟹ set_iterator (it_b a) (S_b a)"
shows "set_iterator (set_iterator_product it_a it_b) (Sigma S_a S_b)"
proof -
note res' = set_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def],
of it_b S_b "λ_ _ _. True", OF it_b[unfolded set_iterator_def]]
note res = set_iterator_intro [OF res']
thus ?thesis by simp
qed

subsection ‹Filter and Image›

text ‹Filtering and applying an injective function on iterators is easily defineable as well.
In contrast to sets the function really has to be injective, because an iterator guarentees to
visit each element only once.›

definition set_iterator_image_filter ::
"('a ⇒ 'b option) ⇒ ('a,'σ) set_iterator ⇒ ('b,'σ) set_iterator" where
"set_iterator_image_filter g it ≡ λc f σ0. (it c
(λx σ. (case (g x) of Some x' ⇒ f x' σ | None ⇒ σ)) σ0)"

lemma set_iterator_image_filter_foldli_conv :
"set_iterator_image_filter g (foldli xs) =
foldli (List.map_filter g xs)"
by (induct xs) (auto simp add: List.map_filter_def set_iterator_image_filter_def fun_eq_iff)

lemma set_iterator_genord_image_filter_correct :
fixes it :: "('a,'σ) set_iterator"
fixes g :: "'a ⇒ 'b option"
assumes it_OK: "set_iterator_genord it S R"
assumes g_inj_on: "inj_on g (S ∩ dom g)"
assumes R'_prop: "⋀x y x' y'. ⟦x ∈ S; g x = Some x'; y ∈ S; g y = Some y'; R x y⟧ ⟹ R' x' y'"
shows "set_iterator_genord (set_iterator_image_filter g it) {y. ∃x. x ∈ S ∧ g x = Some y} R'"
proof -
from it_OK obtain xs where
dist_xs: "distinct xs" and S_eq: "S = set xs" and
sorted_xs: "sorted_wrt R xs" and it_eq: "it = foldli xs"
unfolding set_iterator_genord_foldli_conv by blast

show ?thesis
proof (rule set_iterator_genord_I [of "List.map_filter g xs"])
show "set_iterator_image_filter g it =
foldli (List.map_filter g xs)"
unfolding it_eq  set_iterator_image_filter_foldli_conv by simp
next
from dist_xs g_inj_on[unfolded S_eq]
show "distinct (List.map_filter g xs)"
apply (induct xs)
apply (simp add: List.map_filter_def image_iff inj_on_def Ball_def dom_def)
apply (metis not_Some_eq option.sel)
done
next
show "{y. ∃x. x ∈ S ∧ g x = Some y} =
set (List.map_filter g xs)"
unfolding S_eq set_map_filter by simp
next
from sorted_xs R'_prop[unfolded S_eq]
show "sorted_wrt R' (List.map_filter g xs)"
proof (induct xs rule: list.induct)
case Nil thus ?case by (simp add: List.map_filter_simps)
next
case (Cons x xs)
note sort_x_xs = Cons(2)
note R'_x_xs = Cons(3)

from Cons have ind_hyp: "sorted_wrt R' (List.map_filter g xs)" by auto

show ?case
apply (cases "g x")
apply (simp add: List.map_filter_simps set_map_filter Ball_def ind_hyp)
apply (insert R'_x_xs[of x] sort_x_xs)
apply metis
done
qed
qed
qed

lemma set_iterator_image_filter_correct :
fixes it :: "('a,'σ) set_iterator"
fixes g :: "'a ⇒ 'b option"
assumes it_OK: "set_iterator it S"
assumes g_inj_on: "inj_on g (S ∩ dom g)"
shows "set_iterator (set_iterator_image_filter g it) {y. ∃x. x ∈ S ∧ g x = Some y}"
proof -
note res' = set_iterator_genord_image_filter_correct [OF it_OK[unfolded set_iterator_def],
of g "λ_ _. True"]
note res = set_iterator_intro [OF res']
with g_inj_on show ?thesis by simp
qed

text ‹Special definitions for only filtering or only appling a function are handy.›
definition set_iterator_filter ::
"('a ⇒ bool) ⇒ ('a,'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
"set_iterator_filter P ≡ set_iterator_image_filter (λx. if P x then Some x else None)"

lemma set_iterator_filter_foldli_conv :
"set_iterator_filter P (foldli xs) = foldli (filter P xs)"
apply (rule cong) apply simp
apply (induct xs)
done

lemma set_iterator_filter_alt_def [code] :
"set_iterator_filter P it = (λc f. it c (λ(x::'a) (σ::'b). if P x then f x σ else σ))"
proof -
have "⋀f. (λ(x::'a) (σ::'b).
case if P x then Some x else None of None ⇒ σ
| Some x' ⇒ f x' σ) =
(λx σ. if P x then f x σ else σ)"
by auto
thus ?thesis
unfolding set_iterator_filter_def
set_iterator_image_filter_def[abs_def]
by simp
qed

lemma set_iterator_genord_filter_correct :
fixes it :: "('a,'σ) set_iterator"
assumes it_OK: "set_iterator_genord it S R"
shows "set_iterator_genord (set_iterator_filter P it) {x. x ∈ S ∧ P x} R"
proof -
let ?g = "λx. if P x then Some x else None"
have in_dom_g: "⋀x. x ∈ dom ?g ⟷ P x" unfolding dom_def by auto

from set_iterator_genord_image_filter_correct [OF it_OK, of ?g R, folded set_iterator_filter_def]
show ?thesis
by (simp add: if_split_eq1 inj_on_def Ball_def in_dom_g)
qed

lemma set_iterator_filter_correct :
assumes it_OK: "set_iterator it S"
shows "set_iterator (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
proof -
note res' = set_iterator_genord_filter_correct [OF it_OK[unfolded set_iterator_def],
of P]
note res = set_iterator_intro [OF res']
thus ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_filter_correct :
assumes it_OK: "set_iterator_linord it S"
shows "set_iterator_linord (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
using assms
unfolding set_iterator_linord_def
by (rule set_iterator_genord_filter_correct)

lemma (in linorder) set_iterator_rev_linord_filter_correct :
assumes it_OK: "set_iterator_rev_linord it S"
shows "set_iterator_rev_linord (set_iterator_filter P it) {x. x ∈ S ∧ P x}"
using assms
unfolding set_iterator_rev_linord_def
by (rule set_iterator_genord_filter_correct)

definition set_iterator_image ::
"('a ⇒ 'b) ⇒ ('a,'σ) set_iterator ⇒ ('b,'σ) set_iterator" where
"set_iterator_image g ≡ set_iterator_image_filter (λx. Some (g x))"

lemma set_iterator_image_foldli_conv :
"set_iterator_image g (foldli xs) = foldli (map g xs)"
apply (rule cong) apply simp
apply (induct xs)
done

lemma set_iterator_image_alt_def [code] :
"set_iterator_image g it = (λc f. it c (λx. f (g x)))"
unfolding set_iterator_image_def
set_iterator_image_filter_def[abs_def]
by simp

lemma set_iterator_genord_image_correct :
fixes it :: "('a,'σ) set_iterator"
assumes it_OK: "set_iterator_genord it S R"
assumes g_inj: "inj_on g S"
assumes R'_prop: "⋀x y. ⟦x ∈ S; y ∈ S; R x y⟧ ⟹ R' (g x) (g y)"
shows "set_iterator_genord (set_iterator_image g it) (g ` S) R'"
proof -
let ?g = "λx. Some (g x)"
have set_eq: "⋀S. {y . ∃x. x ∈ S ∧ ?g x = Some y} = g ` S" by auto

show ?thesis
apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of ?g R',
folded set_iterator_image_def set_eq[symmetric]])
apply (insert g_inj, simp add: inj_on_def) []
apply (insert R'_prop, auto)
done
qed

lemma set_iterator_image_correct :
assumes it_OK: "set_iterator it S"
assumes g_inj: "inj_on g S"
assumes S'_OK: "S' = g ` S"
shows "set_iterator (set_iterator_image g it) S'"
proof -
note res' = set_iterator_genord_image_correct [OF it_OK[unfolded set_iterator_def] g_inj,
of "λ_ _. True"]
note res = set_iterator_intro [OF res', folded S'_OK]
thus ?thesis by simp
qed

subsection ‹Construction from list (foldli)›

text ‹Iterators correspond by definition to iteration over distinct lists. They fix an order
in which the elements are visited. Therefore, it is trivial to construct an iterator from a
distinct list.›

lemma set_iterator_genord_foldli_correct :
"distinct xs ⟹ sorted_wrt R xs ⟹ set_iterator_genord (foldli xs) (set xs) R"
by (rule set_iterator_genord_I[of xs]) (simp_all)

lemma set_iterator_foldli_correct :
"distinct xs ⟹ set_iterator (foldli xs) (set xs)"
by (rule set_iterator_I[of xs]) (simp_all)

lemma (in linorder) set_iterator_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of xs]) (simp_all)

lemma (in linorder) set_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_rev_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of xs]) (simp_all)

lemma map_iterator_genord_foldli_correct :
"distinct (map fst xs) ⟹ sorted_wrt R xs ⟹ map_iterator_genord (foldli xs) (map_of xs) R"
by (rule map_iterator_genord_I[of xs]) simp_all

lemma map_iterator_foldli_correct :
"distinct (map fst xs) ⟹ map_iterator (foldli xs) (map_of xs)"
by (rule map_iterator_I[of xs]) (simp_all)

lemma (in linorder) map_iterator_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of xs]) (simp_all)

lemma (in linorder) map_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_rev_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of xs]) (simp_all)

subsection ‹Construction from list (foldri)›

lemma set_iterator_genord_foldri_correct :
"distinct xs ⟹ sorted_wrt R (rev xs) ⟹ set_iterator_genord (foldri xs) (set xs) R"
by (rule set_iterator_genord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma set_iterator_foldri_correct :
"distinct xs ⟹ set_iterator (foldri xs) (set xs)"
by (rule set_iterator_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_rev_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma map_iterator_genord_foldri_correct :
"distinct (map fst xs) ⟹ sorted_wrt R (rev xs) ⟹ map_iterator_genord (foldri xs) (map_of xs) R"
by (rule map_iterator_genord_I[of "rev xs"])

lemma map_iterator_foldri_correct :
"distinct (map fst xs) ⟹ map_iterator (foldri xs) (map_of xs)"
by (rule map_iterator_I[of "rev xs"])

lemma (in linorder) map_iterator_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of "rev xs"])

lemma (in linorder) map_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_rev_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of "rev xs"])

subsection ‹Iterators over Maps›

text ‹In the following iterator over the key-value pairs of a finite map are called
iterators over maps. Operations for such iterators are presented.›

subsubsection‹Domain Iterator›

text ‹One very simple such operation is iterating over only the keys of the map.›

definition map_iterator_dom where
"map_iterator_dom it = set_iterator_image fst it"

lemma map_iterator_dom_foldli_conv :
"map_iterator_dom (foldli kvs) = foldli (map fst kvs)"
unfolding map_iterator_dom_def set_iterator_image_foldli_conv by simp

lemma map_iterator_genord_dom_correct :
assumes it_OK: "map_iterator_genord it m R"
assumes R'_prop: "⋀k v k' v'. ⟦m k = Some v; m k' = Some v'; R (k, v) (k', v')⟧ ⟹ R' k k'"
shows "set_iterator_genord (map_iterator_dom it) (dom m) R'"
proof -
have pre1: "inj_on fst (map_to_set m)"
unfolding inj_on_def map_to_set_def by simp

from set_iterator_genord_image_correct[OF it_OK pre1, of R'] R'_prop
show ?thesis
unfolding map_iterator_dom_def map_to_set_dom[symmetric]
qed

lemma map_iterator_dom_correct :
assumes it_OK: "map_iterator it m"
shows "set_iterator (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_dom_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_correct :
assumes it_OK: "map_iterator_linord it m"
shows "set_iterator_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_linord_def set_iterator_map_linord_def
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done

lemma (in linorder) map_iterator_rev_linord_dom_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "set_iterator_rev_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_rev_linord_def set_iterator_map_rev_linord_def
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done

subsubsection‹Domain Iterator with Filter›

text ‹More complex is iterating over only the keys such that the key-value pairs satisfy some
property.›

definition map_iterator_dom_filter ::
"('a × 'b ⇒ bool) ⇒ ('a × 'b,'σ) set_iterator ⇒ ('a,'σ) set_iterator" where
"map_iterator_dom_filter P it ≡ set_iterator_image_filter
(λxy. if P xy then Some (fst xy) else None) it"

lemma map_iterator_dom_filter_alt_def [code] :
"map_iterator_dom_filter P it =
(λc f. it c (λkv σ. if P kv then f (fst kv) σ else σ))"
unfolding map_iterator_dom_filter_def set_iterator_image_filter_def
apply (rule ext)
apply (rule ext)
apply (rule arg_cong2[where f="it"])
apply (simp)
apply (simp add: fun_eq_iff split: option.splits)
done

lemma map_iterator_genord_dom_filter_correct :
fixes it :: "('a × 'b, 'σ) set_iterator"
assumes it_OK: "set_iterator_genord it (map_to_set m) R"
assumes R'_prop: "⋀k1 v1 k2 v2.
⟦m k1 = Some v1; P (k1, v1);
m k2 = Some v2; P (k2, v2); R (k1, v1) (k2, v2)⟧ ⟹ R' k1 k2"
shows "set_iterator_genord (map_iterator_dom_filter P it) {k . ∃v. m k = Some v ∧ P (k, v)} R'"
proof -
define g where "g xy = (if P xy then Some (fst xy) else None)" for xy :: "'a × 'b"

note set_iterator_genord_image_filter_correct [OF it_OK, of g R']

have g_eq_Some: "⋀kv k. g kv = Some k ⟷ ((k = fst kv) ∧ P kv)"
unfolding g_def by (auto split: prod.splits option.splits)

have "⋀x1 x2 y. x1 ∈ map_to_set m ⟹ x2 ∈ map_to_set m ⟹
g x1 = Some y ⟹ g x2 = Some y ⟹ x1 = x2"
proof -
fix x1 x2 y
assume x1_in: "x1 ∈ map_to_set m"
and x2_in: "x2 ∈ map_to_set m"
and g1_eq: "g x1 = Some y"
and g2_eq: "g x2 = Some y"

obtain k1 v1 where x1_eq[simp] : "x1 = (k1, v1)" by (rule prod.exhaust)
obtain k2 v2 where x2_eq[simp] : "x2 = (k2, v2)" by (rule prod.exhaust)

from g1_eq g2_eq g_eq_Some have k1_eq: "k1 = k2" by simp
with x1_in x2_in have v1_eq: "v1 = v2"
unfolding map_to_set_def by simp
from k1_eq v1_eq show "x1 = x2" by simp
qed
hence g_inj_on: "inj_on g (map_to_set m ∩ dom g)"
unfolding inj_on_def dom_def by auto

have g_eq_Some: "⋀x y. (g x = Some y) ⟷ (P x ∧ y = (fst x))"
unfolding g_def by auto

have "set_iterator_genord (set_iterator_image_filter g it)
{y. ∃x. x ∈ map_to_set m ∧ g x = Some y} R'"
apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of g R', OF g_inj_on])
apply (insert R'_prop)
apply (auto simp add: g_eq_Some map_to_set_def)
done
thus ?thesis
unfolding map_iterator_dom_filter_def g_def[symmetric]
qed

lemma map_iterator_dom_filter_correct :
assumes it_OK: "map_iterator it m"
shows "set_iterator (map_iterator_dom_filter P it) {k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_dom_filter_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_filter_correct :
assumes it_OK: "map_iterator_linord it m"
shows "set_iterator_linord (map_iterator_dom_filter P it) {k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_map_linord_def set_iterator_linord_def
apply (rule_tac map_iterator_genord_dom_filter_correct
[where R = "λ(k,_) (k',_). k≤k'"])
done

lemma (in linorder) set_iterator_rev_linord_map_filter_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "set_iterator_rev_linord (map_iterator_dom_filter P it)
{k. ∃v. m k = Some v ∧ P (k, v)}"
using assms
unfolding set_iterator_map_rev_linord_def set_iterator_rev_linord_def
apply (rule_tac map_iterator_genord_dom_filter_correct
[where R = "λ(k,_) (k',_). k≥k'"])
done

subsubsection‹Product for Maps›

definition map_iterator_product where
"map_iterator_product it_a it_b =
set_iterator_image (λkvv'. (fst (fst kvv'), snd kvv'))
(set_iterator_product it_a (λkv. it_b (snd kv)))"

lemma map_iterator_product_foldli_conv :
"map_iterator_product (foldli as) (λa. foldli (bs a)) =
foldli (concat (map (λ(k, v). map (Pair k) (bs v)) as))"
unfolding map_iterator_product_def set_iterator_product_foldli_conv set_iterator_image_foldli_conv
by (simp add: map_concat o_def split_def)

lemma map_iterator_product_alt_def [code] :
"map_iterator_product it_a it_b =
(λc f. it_a c (λa. it_b (snd a) c (λb. f (fst a, b))))"
unfolding map_iterator_product_def set_iterator_product_def set_iterator_image_alt_def
by simp

lemma map_iterator_genord_product_correct :
fixes it_a :: "(('k × 'v),'σ) set_iterator"
fixes it_b :: "'v ⇒ ('e,'σ) set_iterator"
fixes S_a S_b R_a R_b m
assumes it_a: "map_iterator_genord it_a m R_a"
assumes it_b: "⋀k v. m k = Some v ⟹ set_iterator_genord (it_b v) (S_b v) (R_b v)"
assumes R'_prop: "⋀k v u k' v' u'.
m k = Some v ⟹
u ∈ S_b v ⟹
m k' = Some v' ⟹
u' ∈ S_b v' ⟹
if k = k' then R_b v u u'
else R_a (k, v) (k', v') ⟹
R_ab (k, u) (k', u')"
shows "set_iterator_genord (map_iterator_product it_a it_b)
{(k, e) . (∃v. m k = Some v ∧ e ∈ S_b v)} R_ab"
proof -
from it_b have it_b': "⋀kv. kv ∈ map_to_set m ⟹
set_iterator_genord (it_b (snd kv)) (S_b (snd kv)) (R_b (snd kv))"
unfolding map_to_set_def by (case_tac kv, simp)

have "(⋃x∈{(k, v). m k = Some v}. ⋃y∈S_b (snd x). {(x, y)}) = {((k,v), e) .
(m k = Some v) ∧ e ∈ S_b v}" by (auto)
with set_iterator_genord_product_correct [OF it_a, of "λkv. it_b (snd kv)"
"λkv. S_b (snd kv)" "λkv. R_b (snd kv)", OF it_b']
have it_ab': "set_iterator_genord (set_iterator_product it_a (λkv. it_b (snd kv)))
{((k,v), e) . (m k = Some v) ∧ e ∈ S_b v}
(set_iterator_product_order R_a
(λkv. R_b (snd kv)))"
(is "set_iterator_genord ?it_ab' ?S_ab' ?R_ab'")
unfolding map_to_set_def

let ?g = "λkvv'. (fst (fst kvv'), snd kvv')"
have inj_g: "inj_on ?g ?S_ab'"
unfolding inj_on_def by simp

have R_ab_OK: "⋀x y.
x ∈ {((k, v), e). m k = Some v ∧ e ∈ S_b v} ⟹
y ∈ {((k, v), e). m k = Some v ∧ e ∈ S_b v} ⟹
set_iterator_product_order R_a (λkv. R_b (snd kv)) x y ⟹
R_ab (fst (fst x), snd x) (fst (fst y), snd y)"
apply clarify
apply (simp)
apply (unfold fst_conv snd_conv)
apply (metis R'_prop option.inject)
done

have "(?g ` {((k, v), e). m k = Some v ∧ e ∈ S_b v}) = {(k, e). ∃v. m k = Some v ∧ e ∈ S_b v}"
with set_iterator_genord_image_correct [OF it_ab' inj_g, of R_ab, OF R_ab_OK]
show ?thesis
qed

lemma map_iterator_product_correct :
assumes it_a: "map_iterator it_a m"
assumes it_b: "⋀k v. m k = Some v ⟹ set_iterator (it_b v) (S_b v)"
shows "set_iterator (map_iterator_product it_a it_b)
{(k, e) . (∃v. m k = Some v ∧ e ∈ S_b v)}"
proof -
note res' = map_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def],
of it_b S_b "λ_ _ _. True"]
note res = set_iterator_intro [OF res']
with it_b show ?thesis unfolding set_iterator_def by simp
qed

subsubsection‹Key Filter›

definition map_iterator_key_filter ::
"('a ⇒ bool) ⇒ ('a × 'b,'σ) set_iterator ⇒ ('a × 'b,'σ) set_iterator" where
"map_iterator_key_filter P ≡ set_iterator_filter (P ∘ fst)"

lemma map_iterator_key_filter_foldli_conv :
"map_iterator_key_filter P (foldli kvs) =  foldli (filter (λ(k, v). P k) kvs)"
unfolding map_iterator_key_filter_def set_iterator_filter_foldli_conv o_def split_def
by simp

lemma map_iterator_key_filter_alt_def [code] :
"map_iterator_key_filter P it = (λc f. it c (λx σ. if P (fst x) then f x σ else σ))"
unfolding map_iterator_key_filter_def set_iterator_filter_alt_def
set_iterator_image_filter_def by simp

lemma map_iterator_genord_key_filter_correct :
fixes it :: "('a × 'b, 'σ) set_iterator"
assumes it_OK: "map_iterator_genord it m R"
shows "map_iterator_genord (map_iterator_key_filter P it) (m |` {k . P k}) R"
proof -
from set_iterator_genord_filter_correct [OF it_OK, of "P ∘ fst",
folded map_iterator_key_filter_def]
have step1: "set_iterator_genord (map_iterator_key_filter P it)
{x ∈ map_to_set m. (P ∘ fst) x} R"
by simp

have "{x ∈ map_to_set m. (P ∘ fst) x} = map_to_set (m |` {k . P k})"
unfolding map_to_set_def restrict_map_def
by (auto split: if_splits)
with step1 show ?thesis by simp
qed

lemma map_iterator_key_filter_correct :
assumes it_OK: "map_iterator it m"
shows "set_iterator (map_iterator_key_filter P it) (map_to_set (m |` {k . P k}))"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_key_filter_correct)
apply simp_all
done

end

```