# Theory Sorted_List_Operations

section ‹\isaheader{Operations on sorted Lists}›
theory Sorted_List_Operations
imports Main Automatic_Refinement.Misc
begin

fun inter_sorted :: "'a::{linorder} list ⇒ 'a list ⇒ 'a list" where
"inter_sorted [] l2 = []"
| "inter_sorted l1 [] = []"
| "inter_sorted (x1 # l1) (x2 # l2) =
(if (x1 < x2) then (inter_sorted l1 (x2 # l2)) else
(if (x1 = x2) then x1 # (inter_sorted l1 l2) else inter_sorted (x1 # l1) l2))"

lemma inter_sorted_correct :
assumes l1_OK: "distinct l1 ∧ sorted l1"
assumes l2_OK: "distinct l2 ∧ sorted l2"
shows "distinct (inter_sorted l1 l2) ∧ sorted (inter_sorted l1 l2) ∧
set (inter_sorted l1 l2) = set l1 ∩ set l2"
using assms
proof (induct l1 arbitrary: l2)
case Nil thus ?case by simp
next
case (Cons x1 l1 l2)
note x1_l1_props = Cons(2)
note l2_props = Cons(3)

from x1_l1_props have l1_props: "distinct l1 ∧ sorted l1"
and x1_nin_l1: "x1 ∉ set l1"
and x1_le: "⋀x. x ∈ set l1 ⟹ x1 ≤ x"

note ind_hyp_l1 = Cons(1)[OF l1_props]

show ?case
using l2_props
proof (induct l2)
case Nil with x1_l1_props show ?case by simp
next
case (Cons x2 l2)
note x2_l2_props = Cons(2)
from x2_l2_props have l2_props: "distinct l2 ∧ sorted l2"
and x2_nin_l2: "x2 ∉ set l2"
and x2_le: "⋀x. x ∈ set l2 ⟹ x2 ≤ x"

note ind_hyp_l2 = Cons(1)[OF l2_props]
show ?case
proof (cases "x1 < x2")
case True note x1_less_x2 = this

from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
show ?thesis
apply (metis linorder_not_le)
done
next
case False note x2_le_x1 = this

show ?thesis
proof (cases "x1 = x2")
case True note x1_eq_x2 = this

from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
show ?thesis by (simp add: x1_eq_x2 Ball_def)
next
case False note x1_neq_x2 = this
with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

from ind_hyp_l2 x2_le_x1 x1_neq_x2 x2_le x2_nin_l2 x1_le
show ?thesis
apply (auto simp add: x2_less_x1 Ball_def)
apply (metis linorder_not_le x2_less_x1)
done
qed
qed
qed
qed

fun diff_sorted :: "'a::{linorder} list ⇒ 'a list ⇒ 'a list" where
"diff_sorted [] l2 = []"
| "diff_sorted l1 [] = l1"
| "diff_sorted (x1 # l1) (x2 # l2) =
(if (x1 < x2) then x1 # (diff_sorted l1 (x2 # l2)) else
(if (x1 = x2) then (diff_sorted l1 l2) else diff_sorted (x1 # l1) l2))"

lemma diff_sorted_correct :
assumes l1_OK: "distinct l1 ∧ sorted l1"
assumes l2_OK: "distinct l2 ∧ sorted l2"
shows "distinct (diff_sorted l1 l2) ∧ sorted (diff_sorted l1 l2) ∧
set (diff_sorted l1 l2) = set l1 - set l2"
using assms
proof (induct l1 arbitrary: l2)
case Nil thus ?case by simp
next
case (Cons x1 l1 l2)
note x1_l1_props = Cons(2)
note l2_props = Cons(3)

from x1_l1_props have l1_props: "distinct l1 ∧ sorted l1"
and x1_nin_l1: "x1 ∉ set l1"
and x1_le: "⋀x. x ∈ set l1 ⟹ x1 ≤ x"

note ind_hyp_l1 = Cons(1)[OF l1_props]

show ?case
using l2_props
proof (induct l2)
case Nil with x1_l1_props show ?case by simp
next
case (Cons x2 l2)
note x2_l2_props = Cons(2)
from x2_l2_props have l2_props: "distinct l2 ∧ sorted l2"
and x2_nin_l2: "x2 ∉ set l2"
and x2_le: "⋀x. x ∈ set l2 ⟹ x2 ≤ x"

note ind_hyp_l2 = Cons(1)[OF l2_props]
show ?case
proof (cases "x1 < x2")
case True note x1_less_x2 = this

from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
show ?thesis
apply simp
apply (metis linorder_not_le order_less_imp_not_eq2)
done
next
case False note x2_le_x1 = this

show ?thesis
proof (cases "x1 = x2")
case True note x1_eq_x2 = this

from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
show ?thesis by (simp add: x1_eq_x2 Ball_def)
next
case False note x1_neq_x2 = this
with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

from x2_less_x1 x1_le have x2_nin_l1: "x2 ∉ set l1"
by (metis linorder_not_less)

from ind_hyp_l2 x1_le x2_nin_l1
show ?thesis
apply (simp add: x2_less_x1 x1_neq_x2 x2_le_x1 x1_nin_l1 Ball_def set_eq_iff)
apply (metis x1_neq_x2)
done
qed
qed
qed
qed

fun subset_sorted :: "'a::{linorder} list ⇒ 'a list ⇒ bool" where
"subset_sorted [] l2 = True"
| "subset_sorted (x1 # l1) [] = False"
| "subset_sorted (x1 # l1) (x2 # l2) =
(if (x1 < x2) then False else
(if (x1 = x2) then (subset_sorted l1 l2) else subset_sorted (x1 # l1) l2))"

lemma subset_sorted_correct :
assumes l1_OK: "distinct l1 ∧ sorted l1"
assumes l2_OK: "distinct l2 ∧ sorted l2"
shows "subset_sorted l1 l2 ⟷ set l1 ⊆ set l2"
using assms
proof (induct l1 arbitrary: l2)
case Nil thus ?case by simp
next
case (Cons x1 l1 l2)
note x1_l1_props = Cons(2)
note l2_props = Cons(3)

from x1_l1_props have l1_props: "distinct l1 ∧ sorted l1"
and x1_nin_l1: "x1 ∉ set l1"
and x1_le: "⋀x. x ∈ set l1 ⟹ x1 ≤ x"

note ind_hyp_l1 = Cons(1)[OF l1_props]

show ?case
using l2_props
proof (induct l2)
case Nil with x1_l1_props show ?case by simp
next
case (Cons x2 l2)
note x2_l2_props = Cons(2)
from x2_l2_props have l2_props: "distinct l2 ∧ sorted l2"
and x2_nin_l2: "x2 ∉ set l2"
and x2_le: "⋀x. x ∈ set l2 ⟹ x2 ≤ x"

note ind_hyp_l2 = Cons(1)[OF l2_props]
show ?case
proof (cases "x1 < x2")
case True note x1_less_x2 = this

from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
show ?thesis
apply (metis linorder_not_le)
done
next
case False note x2_le_x1 = this

show ?thesis
proof (cases "x1 = x2")
case True note x1_eq_x2 = this

from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
show ?thesis
apply (simp add: subset_iff x1_eq_x2 Ball_def)
apply metis
done
next
case False note x1_neq_x2 = this
with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

from ind_hyp_l2 x2_le_x1 x1_neq_x2 x2_le x2_nin_l2 x1_le
show ?thesis
apply (simp add: subset_iff x2_less_x1 Ball_def)
apply (metis linorder_not_le x2_less_x1)
done
qed
qed
qed
qed

lemma set_eq_sorted_correct :
assumes l1_OK: "distinct l1 ∧ sorted l1"
assumes l2_OK: "distinct l2 ∧ sorted l2"
shows "l1 = l2 ⟷ set l1 = set l2"
using assms
proof -
have l12_eq: "l1 = l2 ⟷ subset_sorted l1 l2 ∧ subset_sorted l2 l1"
proof (induct l1 arbitrary: l2)
case Nil thus ?case by (cases l2) auto
next
case (Cons x1 l1')
note ind_hyp = Cons(1)

show ?case
proof (cases l2)
case Nil thus ?thesis by simp
next
case (Cons x2 l2')
thus ?thesis by (simp add: ind_hyp)
qed
qed
also have "… ⟷ ((set l1 ⊆ set l2) ∧ (set l2 ⊆ set l1))"
using subset_sorted_correct[OF l1_OK l2_OK] subset_sorted_correct[OF l2_OK l1_OK]
by simp
also have "… ⟷ set l1 = set l2" by auto
finally show ?thesis .
qed

fun memb_sorted where
"memb_sorted [] x = False"
| "memb_sorted (y # xs) x =
(if (y < x) then memb_sorted xs x else (x = y))"

lemma memb_sorted_correct :
"sorted xs ⟹ memb_sorted xs x ⟷ x ∈ set xs"
by (induct xs) (auto simp add: Ball_def)

fun insertion_sort where
"insertion_sort x [] = [x]"
| "insertion_sort x (y # xs) =
(if (y < x) then y # insertion_sort x xs else
(if (x = y) then y # xs else x # y # xs))"

lemma insertion_sort_correct :
"sorted xs ⟹ distinct xs ⟹
distinct (insertion_sort x xs) ∧
sorted (insertion_sort x xs) ∧
set (insertion_sort x xs) = set (x # xs)"
by (induct xs) (auto simp add: Ball_def)

fun delete_sorted where
"delete_sorted x [] = []"
| "delete_sorted x (y # xs) =
(if (y < x) then y # delete_sorted x xs else
(if (x = y) then xs else y # xs))"

lemma delete_sorted_correct :
"sorted xs ⟹ distinct xs ⟹
distinct (delete_sorted x xs) ∧
sorted (delete_sorted x xs) ∧
set (delete_sorted x xs) = set xs - {x}"
apply (induct xs)
apply simp
apply (metis order_less_le)
done

end


# Theory HashCode

(*  Title:       Isabelle Collections Library
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Philipp Meyer <meyerphi@in.tum.de>
*)
theory HashCode
imports
Native_Word.Uint32
begin

text_raw ‹\label{thy:HashCode}›

text ‹
In this theory a typeclass of hashable types is established.
For hashable types, there is a function ‹hashcode›, that
maps any entity of this type to an unsigned 32 bit word value.

This theory defines the hashable typeclass and provides instantiations
for a couple of standard types.
›

type_synonym
hashcode = "uint32"

definition "nat_of_hashcode ≡ nat_of_uint32"
definition "int_of_hashcode ≡ int_of_uint32"
definition "integer_of_hashcode ≡ integer_of_uint32"

class hashable =
fixes hashcode :: "'a ⇒ hashcode"
and def_hashmap_size :: "'a itself ⇒ nat"
assumes def_hashmap_size: "1 < def_hashmap_size TYPE('a)"
begin
definition bounded_hashcode :: "uint32 ⇒ 'a ⇒ uint32" where
"bounded_hashcode n x = (hashcode x) mod n"

lemma bounded_hashcode_bounds: "1 < n ⟹ bounded_hashcode n a < n"
unfolding bounded_hashcode_def
by (transfer, simp add: word_less_def uint_mod)

definition bounded_hashcode_nat :: "nat ⇒ 'a ⇒ nat" where
"bounded_hashcode_nat n x = nat_of_hashcode (hashcode x) mod n"

lemma bounded_hashcode_nat_bounds: "1 < n ⟹ bounded_hashcode_nat n a < n"
unfolding bounded_hashcode_nat_def
by transfer simp
end

instantiation unit :: hashable
begin
definition [simp]: "hashcode (u :: unit) = 0"
definition "def_hashmap_size = (λ_ :: unit itself. 2)"
instance
end

instantiation bool :: hashable
begin
definition [simp]: "hashcode (b :: bool) = (if b then 1 else 0)"
definition "def_hashmap_size = (λ_ :: bool itself. 2)"
end

instantiation "int" :: hashable
begin
definition [simp]: "hashcode (i :: int) = uint32_of_int i"
definition "def_hashmap_size = (λ_ :: int itself. 16)"
end

instantiation "integer" :: hashable
begin
definition [simp]: "hashcode (i :: integer) = Uint32 i"
definition "def_hashmap_size = (λ_ :: integer itself. 16)"
end

instantiation "nat" :: hashable
begin
definition [simp]: "hashcode (n :: nat) = uint32_of_int (int n)"
definition "def_hashmap_size = (λ_ :: nat itself. 16)"
end

instantiation char :: hashable
begin
definition [simp]: "hashcode (c :: char) == uint32_of_int (of_char c)"
definition "def_hashmap_size = (λ_ :: char itself. 32)"
end

instantiation prod :: (hashable, hashable) hashable
begin
definition "hashcode x == (hashcode (fst x) * 33 + hashcode (snd x))"
definition "def_hashmap_size = (λ_ :: ('a × 'b) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"
instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
end

instantiation sum :: (hashable, hashable) hashable
begin
definition "hashcode x == (case x of Inl a ⇒ 2 * hashcode a | Inr b ⇒ 2 * hashcode b + 1)"
definition "def_hashmap_size = (λ_ :: ('a + 'b) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"
instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
by(intro_classes)(simp_all add: bounded_hashcode_bounds def_hashmap_size_sum_def split: sum.split)
end

instantiation list :: (hashable) hashable
begin
definition "hashcode = foldl (λh x. h * 33 + hashcode x) 5381"
definition "def_hashmap_size = (λ_ :: 'a list itself. 2 * def_hashmap_size TYPE('a))"
instance
proof
from def_hashmap_size[where ?'a = "'a"]
show "1 < def_hashmap_size TYPE('a list)"
qed
end

instantiation option :: (hashable) hashable
begin
definition "hashcode opt = (case opt of None ⇒ 0 | Some a ⇒ hashcode a + 1)"
definition "def_hashmap_size = (λ_ :: 'a option itself. def_hashmap_size TYPE('a) + 1)"
instance using def_hashmap_size[where ?'a = "'a"]
end

lemma hashcode_option_simps [simp]:
"hashcode None = 0"
"hashcode (Some a) = 1 + hashcode a"

lemma bounded_hashcode_option_simps [simp]:
"bounded_hashcode n None = 0"
"bounded_hashcode n (Some a) = (hashcode a + 1) mod n"

(*
lemma bounded_hashcode_option_simps [simp]:
"bounded_hashcode n None = 0"
"bounded_hashcode n (Some a) = (bounded_hashcode n a + 1) mod n"
*)

instantiation String.literal :: hashable
begin

definition hashcode_literal :: "String.literal ⇒ uint32"
where "hashcode_literal s = hashcode (String.explode s)"

definition def_hashmap_size_literal  :: "String.literal itself ⇒ nat"
where "def_hashmap_size_literal _ = 10"

instance
by standard (simp_all only: def_hashmap_size_literal_def)

end

hide_type (open) word

end


# Theory Code_Target_ICF

section ‹Default Code Generator Setup for the Isabelle Collection Framework›
theory Code_Target_ICF
imports
"HOL-Library.Code_Target_Numeral"
Native_Word.Code_Target_Bits_Int
begin

end


# Theory SetIterator

(*  Title:       Iterators over Finite Sets
Author:      Thomas Tuerk <tuerk@in.tum.de>
Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
theory SetIterator
imports
Automatic_Refinement.Misc
Automatic_Refinement.Foldi
begin

text ‹When reasoning about finite sets, it is often handy to be able to iterate over the elements
of the set. If the finite set is represented by a list, the @{term fold} operation can be used.
For general finite sets, the order of elements is not fixed though. Therefore, nondeterministic
iterators are introduced in this theory.›

subsection ‹General Iterators›

type_synonym ('x,'σ) set_iterator = "('σ⇒bool) ⇒ ('x⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"

locale set_iterator_genord =
fixes iti::"('x,'σ) set_iterator"
and S0::"'x set"
and R::"'x ⇒ 'x ⇒ bool"
assumes foldli_transform:
"∃l0. distinct l0 ∧ S0 = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0"
begin
text ‹Let's prove some trivial lemmata to show that the formalisation agrees with
the view of iterators described above.›
lemma set_iterator_weaken_R :
"(⋀x y. ⟦x ∈ S0; y ∈ S0; R x y⟧ ⟹ R' x y) ⟹
set_iterator_genord iti S0 R'"
by (metis set_iterator_genord.intro foldli_transform sorted_wrt_mono_rel)

lemma finite_S0 :
shows "finite S0"
by (metis finite_set foldli_transform)

lemma iti_stop_rule_cond :
assumes not_c: "¬(c σ)"
shows "iti c f σ = σ"
proof -
from foldli_transform obtain l0 where l0_props:
"iti c = foldli l0 c" by blast
with foldli_not_cond [of c σ l0 f, OF not_c]
show ?thesis by simp
qed

lemma iti_stop_rule_emp :
assumes S0_emp: "S0 = {}"
shows "iti c f σ = σ"
proof -
from foldli_transform obtain l0 where l0_props:
"S0 = set l0" "iti c = foldli l0 c" by blast
with foldli.simps(1) [of c f σ] S0_emp
show ?thesis by simp
qed

text ‹Reducing everything to folding is cumbersome. Let's
define a few high-level inference rules.›

lemma iteratei_rule_P:
assumes
"I S0 σ0"
"⋀S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0;
∀y∈S - {x}. R x y; ∀y∈S0 - S. R y x⟧
⟹ I (S - {x}) (f x σ)"
"⋀σ. I {} σ ⟹ P σ"
"⋀σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ c σ; I S σ;
∀x∈S. ∀y∈S0-S. R y x ⟧ ⟹ P σ"
shows "P (iti c f σ0)"
proof -
{ fix P I σ0 f
assume
I: "I S0 σ0" and
R: "⋀S σ x. ⟦c σ; x ∈ S; I S σ; S ⊆ S0; ∀y∈S-{x}. R x y⟧ ⟹ I (S - {x}) (f x σ)" and
C1: "I {} (iti c f σ0) ⟹ P" and
C2:"⋀S. ⟦S ⊆ S0; S ≠ {}; ¬ c (iti c f σ0); I S (iti c f σ0)⟧ ⟹ P"

from foldli_transform obtain l0 where l0_props:
"distinct l0" "S0 = set l0" "sorted_wrt R l0"  "iti c = foldli l0 c" by auto

from I R
have "I {} (iti c f σ0) ∨
(∃S. S ⊆ S0 ∧ S ≠ {} ∧
¬ (c (iti c f σ0)) ∧
I S (iti c f σ0))"
unfolding l0_props using l0_props(1,3)
proof (induct l0 arbitrary: σ0)
case Nil thus ?case by simp
next
case (Cons x l0)
note ind_hyp = Cons(1)
note I_x_l0 = Cons(2)
note step = Cons(3)
from Cons(4) have dist_l0: "distinct l0" and x_nin_l0: "x ∉ set l0" by simp_all
from Cons(5) have R_l0: "∀y∈set l0. R x y" and
sort_l0: "sorted_wrt R l0" by simp_all

show ?case
proof (cases "c σ0")
case False
with I_x_l0 show ?thesis
apply (rule_tac disjI2)
apply (rule_tac exI[where x="set (x # l0)"])
apply (simp)
done
next
case True note c_σ0 = this

from step[of σ0 x "set (x # l0)"] I_x_l0 R_l0 c_σ0 x_nin_l0
have step': "I (set l0) (f x σ0)"

from ind_hyp [OF step' step dist_l0 sort_l0]
have "I {} (foldli l0 c f (f x σ0)) ∨
(∃S. S ⊆ set l0 ∧ S ≠ {} ∧
¬ c (foldli l0 c f (f x σ0)) ∧ I S (foldli l0 c f (f x σ0)))"
by (fastforce)
thus ?thesis
by (simp add: c_σ0 subset_iff) metis
qed
qed
with C1 C2 have "P" by blast
} note aux = this

from assms
show ?thesis
apply (rule_tac aux [of "λS σ. I S σ ∧ (∀x∈S. ∀y∈S0-S. R y x)" σ0 f])
apply auto
done
qed

text ‹Instead of removing elements one by one from the invariant, adding them is sometimes more natural.›
lemma iteratei_rule_insert_P:
assumes pre :
"I {} σ0"
"⋀S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ∀y∈(S0 - S) - {x}. R x y;
∀y∈S. R y x⟧
⟹ I (insert x S) (f x σ)"
"⋀σ. I S0 σ ⟹ P σ"
"⋀σ S. ⟦ S ⊆ S0; S ≠ S0;
¬ (c σ); I S σ; ∀x∈S0-S. ∀y∈S. R y x ⟧ ⟹ P σ"
shows "P (iti c f σ0)"
proof -
let ?I' = "λS σ. I (S0 - S) σ"

have pre1:
"!!σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ (c σ); ?I' S σ;
∀x∈S. ∀y∈S0-S. R y x⟧ ⟹ P σ"
proof -
fix S σ
assume AA:
"S ⊆ S0" "S ≠ {}"
"¬ (c σ)"
"?I' S σ" "∀x∈S. ∀y∈S0-S. R y x"
with pre(4) [of "S0 - S"]
show "P σ" by auto
qed

have pre2 :"⋀x S σ. ⟦c σ; x ∈ S; S ⊆ S0; ?I' S σ; ∀y∈S - {x}. R x y; ∀y∈S0-S. R y x ⟧ ⟹ ?I' (S - {x}) (f x σ)"
proof -
fix x S σ
assume AA : "c σ" "x ∈ S" "S ⊆ S0" "?I' S σ" "∀y∈S - {x}. R x y" "∀y∈S0 - S. R y x"

from AA(2) AA(3) have "S0 - (S - {x}) = insert x (S0 - S)" "S0 - (S0 - S) = S" by auto
moreover
note pre(2) [of σ x "S0 - S"] AA
ultimately show "?I' (S - {x}) (f x σ)"
by auto
qed

show "P (iti c f σ0)"
apply (rule iteratei_rule_P [of ?I' σ0 c f P])
apply (rule pre2) apply simp_all
done
qed

text ‹Show that iti without interruption is related to fold›
lemma iti_fold:
assumes lc_f: "comp_fun_commute f"
shows "iti (λ_. True) f σ0 = Finite_Set.fold f σ0 S0"
proof (rule iteratei_rule_insert_P [where I = "λX σ'. σ' = Finite_Set.fold f σ0 X"])
fix S σ x
assume "x ∈ S0 - S" "S ⊆ S0" and σ_eq: "σ = Finite_Set.fold f σ0 S"
from finite_S0 ‹S ⊆ S0› have fin_S: "finite S" by (metis finite_subset)
from ‹x ∈ S0 - S› have x_nin_S: "x ∉ S" by simp
note fold_eq = comp_fun_commute.fold_insert [OF lc_f fin_S x_nin_S]

show "f x σ = Finite_Set.fold f σ0 (insert x S)"
qed simp_all
end

subsection ‹Iterators over Maps›

type_synonym ('k,'v,'σ) map_iterator = "('k×'v,'σ) set_iterator"

text ‹Iterator over the key-value pairs of a finite map are called iterators over maps.›
abbreviation "map_iterator_genord it m R ≡ set_iterator_genord it (map_to_set m) R"

subsection ‹Unordered Iterators›

text ‹Often one does not care about the order in which the elements are processed.
Therefore, the selection function can be set to not impose any further restrictings.
This leads to considerably simpler theorems.›

definition "set_iterator it S0 ≡ set_iterator_genord it S0 (λ_ _. True)"
abbreviation "map_iterator it m ≡ set_iterator it (map_to_set m)"

lemma set_iterator_intro :
"set_iterator_genord it S0 R ⟹ set_iterator it S0"
unfolding set_iterator_def
apply (rule set_iterator_genord.set_iterator_weaken_R [where R = R])
apply simp_all
done

lemma set_iterator_no_cond_rule_P:
"⟦ set_iterator it S0;
I S0 σ0;
!!S σ x. ⟦ x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ
⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp

lemma set_iterator_no_cond_rule_insert_P:
"⟦ set_iterator it S0;
I {} σ0;
!!S σ x. ⟦ x ∈ S0 - S; I S σ; S ⊆ S0 ⟧  ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ
⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp

lemma set_iterator_rule_P:
"⟦ set_iterator it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp

lemma set_iterator_rule_insert_P:
"⟦ set_iterator it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0 ⟧  ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp

text‹The following rules is adapted for maps. Instead of a set of key-value pairs the invariant
now only sees the keys.›
lemma map_iterator_genord_rule_P:
assumes "map_iterator_genord it m R"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
∀k' v'. k' ∈ it-{k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)⟧ ⟹
I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶
R (k, v) (k', v') ⟧ ⟹ P σ"
shows "P (it c f σ0)"
proof (rule set_iterator_genord.iteratei_rule_P [of it "map_to_set m" R "λS σ. I (fst  S) σ" σ0 c f P])
show "map_iterator_genord it m R" by fact
next
show "I (fst  map_to_set m) σ0" using I0 by (simp add: map_to_set_dom[symmetric])
next
fix σ
assume "I (fst  {}) σ"
with IF show "P σ" by simp
next
fix σ S
assume "S ⊆ map_to_set m" "S ≠ {}" "¬ c σ" "I (fst  S) σ"
and R_prop: "∀x∈S. ∀y∈map_to_set m - S. R y x"
let ?S' = "fst  S"

show "P σ"
proof (rule II [where it = ?S'])
from ‹S ⊆ map_to_set m›
show "?S' ⊆ dom m"
unfolding map_to_set_dom
by auto
next
from ‹S ≠ {}› show "?S' ≠ {}" by auto
next
show "¬ (c σ)" by fact
next
show "I (fst  S) σ" by fact
next
show "∀k v k' v'.
k ∉ fst  S ∧
m k = Some v ∧
k' ∈ fst  S ∧ m k' = Some v' ⟶
R (k, v) (k', v')"
proof (intro allI impI, elim conjE )
fix k v k' v'
assume pre_k: "k ∉ fst  S" "m k = Some v"
assume pre_k': "k' ∈ fst  S" "m k' = Some v'"

from ‹S ⊆ map_to_set m› pre_k'
have kv'_in: "(k', v') ∈ S"
unfolding map_to_set_def by auto

from ‹S ⊆ map_to_set m› pre_k
have kv_in: "(k, v) ∈ map_to_set m - S"
unfolding map_to_set_def

from R_prop kv_in kv'_in
show "R (k, v) (k',v')" by simp
qed
qed
next
fix σ S kv
assume "S ⊆ map_to_set m" "kv ∈ S" "c σ" and I_S': "I (fst  S) σ" and
R_S: "∀kv'∈S - {kv}. R kv kv'" and
R_not_S: "∀kv'∈map_to_set m - S. R kv' kv"
let ?S' = "fst  S"
obtain k v where kv_eq[simp]: "kv = (k, v)" by (rule prod.exhaust)

have "I (fst  S - {k}) (f (k, v) σ)"
proof (rule IP)
show "c σ" by fact
next
from ‹kv ∈ S› show "k ∈ ?S'" by (auto simp add: image_iff Bex_def)
next
from ‹kv ∈ S› ‹S ⊆ map_to_set m›
have "kv ∈ map_to_set m" by auto
thus m_k_eq: "m k = Some v" unfolding map_to_set_def by simp
next
from ‹S ⊆ map_to_set m›
show S'_subset: "?S' ⊆ dom m"
unfolding map_to_set_dom
by auto
next
show "I (fst  S) σ" by fact
next
from ‹S ⊆ map_to_set m› ‹kv ∈ S›
have S_simp: "{(k', v'). k' ∈ (fst  S) - {k} ∧ m k' = Some v'} = S - {kv}"
unfolding map_to_set_def subset_iff
apply (auto simp add: image_iff Bex_def)
apply (metis option.inject)
done

from R_S[unfolded S_simp[symmetric]] R_not_S
show "∀k' v'. k' ∈ fst  S - {k} ∧ m k' = Some v' ⟶
R (k, v) (k', v') "
by simp
next
from ‹S ⊆ map_to_set m› R_not_S
show "∀k' v'. k' ∉ fst  S ∧ m k' = Some v' ⟶ R (k', v') (k, v)"
apply (simp add: Ball_def map_to_set_def subset_iff image_iff)
apply metis
done
qed

moreover
from ‹S ⊆ map_to_set m› ‹kv ∈ S›
have "fst  (S - {kv}) = fst  S - {k}"
apply (simp add: set_eq_iff image_iff Bex_def map_to_set_def subset_iff)
apply (metis option.inject)
done

ultimately show "I (fst  (S - {kv})) (f kv σ)" by simp
qed

lemma map_iterator_genord_rule_insert_P:
assumes "map_iterator_genord it m R"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
∀k' v'. k' ∈ (dom m - it) - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
∀k' v'. k' ∈ it ∧ m k' = Some v' ⟶
R (k', v') (k, v)⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
∀k v k' v'. k ∈ it ∧ m k = Some v ∧ k' ∉ it ∧ m k' = Some v' ⟶
R (k, v) (k', v') ⟧ ⟹ P σ"
shows "P (it c f σ0)"
proof (rule map_iterator_genord_rule_P [of it m R "λS σ. I (dom m - S) σ"])
show "map_iterator_genord it m R" by fact
next
show "I (dom m - dom m) σ0" using I0 by simp
next
fix σ
assume "I (dom m - {}) σ"
with IF show "P σ" by simp
next
fix σ it
assume assms: "it ⊆ dom m" "it ≠ {}" "¬ c σ" "I (dom m - it) σ"
"∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶
R (k, v) (k', v')"
from assms have "dom m - it ≠ dom m" by auto
with II[of "dom m - it" σ] assms
show "P σ"
apply (metis option.simps(2))
done
next
fix k v it σ
assume assms: "c σ" "k ∈ it" "m k = Some v" "it ⊆ dom m" "I (dom m - it) σ"
"∀k' v'. k' ∈ it - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v')"
"∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)"

hence "insert k (dom m - it) = (dom m - (it - {k}))" "dom m - (dom m - it) = it" by auto
with assms IP[of σ k "dom m - it" v]
show "I (dom m - (it - {k})) (f (k, v) σ)" by (simp_all add: subset_iff)
qed

lemma map_iterator_rule_P:
assumes "map_iterator it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ ⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_rule_insert_P:
assumes "map_iterator it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ ⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_P:
assumes "map_iterator it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ k ∈ it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_insert_P:
assumes "map_iterator it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp

subsection ‹Ordered Iterators›

text ‹Selecting according to a linear order is another case that is interesting.
Ordered iterators over maps, i.\,e.\ iterators over key-value pairs,
use an order on the keys.›

context linorder begin
definition "set_iterator_linord it S0
≡ set_iterator_genord it S0 (≤)"
definition "set_iterator_rev_linord it S0
≡ set_iterator_genord it S0 (≥)"
definition "set_iterator_map_linord it S0 ≡
set_iterator_genord it S0 (λ(k,_) (k',_). k≤k')"
definition "set_iterator_map_rev_linord it S0 ≡
set_iterator_genord it S0 (λ(k,_) (k',_). k≥k')"
abbreviation "map_iterator_linord it m ≡
set_iterator_map_linord it (map_to_set m)"
abbreviation "map_iterator_rev_linord it m ≡
set_iterator_map_rev_linord it (map_to_set m)"

lemma set_iterator_linord_rule_P:
"⟦ set_iterator_linord it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x' ≤ x; ⋀x'. x' ∈ S ⟹ x ≤ x'⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_linord_def
apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≤)" I σ0 c f P])
apply (metis order_refl)
done

lemma set_iterator_linord_rule_insert_P:
"⟦ set_iterator_linord it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x' ≤ x; ⋀x'. x' ∈ S0 - S ⟹ x ≤ x'⟧  ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≤)" I σ0 c f P])
apply (metis order_refl)
done

lemma set_iterator_rev_linord_rule_P:
"⟦ set_iterator_rev_linord it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x ≤ x'; ⋀x'. x' ∈ S ⟹ x' ≤ x⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≥)" I σ0 c f P])
apply (metis order_refl)
done

lemma set_iterator_rev_linord_rule_insert_P:
"⟦ set_iterator_rev_linord it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x ≤ x'; ⋀x'. x' ∈ S0 - S ⟹ x' ≤ x⟧  ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹  (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≥)" I σ0 c f P])
apply (metis order_refl)
done

lemma set_iterator_map_linord_rule_P:
"⟦ set_iterator_map_linord it S0;
I S0 σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k' ≤ k;
⋀k' v'. (k', v') ∈ S ⟹ k ≤ k'⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k ≤ k') ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_linord_def
apply (rule set_iterator_genord.iteratei_rule_P
[of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
apply simp_all
apply (metis order_refl)
apply metis
done

lemma set_iterator_map_linord_rule_insert_P:
"⟦ set_iterator_map_linord it S0;
I {} σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k;
⋀k' v'. (k',v') ∈ S0 - S ⟹ k ≤ k'⟧  ⟹ I (insert (k,v) S) (f (k,v) σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k ≤ k') ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P
[of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
apply simp_all
apply (metis order_refl)
apply metis
done

lemma set_iterator_map_rev_linord_rule_P:
"⟦ set_iterator_map_rev_linord it S0;
I S0 σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k ≤ k';
⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k' ≤ k) ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_P
[of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
apply simp_all
apply (metis order_refl)
apply metis
done

lemma set_iterator_map_rev_linord_rule_insert_P:
"⟦ set_iterator_map_rev_linord it S0;
I {} σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k ≤ k';
⋀k' v'. (k',v') ∈ S0 - S ⟹ k' ≤ k⟧  ⟹ I (insert (k,v) S) (f (k,v) σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k' ≤ k) ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P
[of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
apply simp_all
apply (metis order_refl)
apply metis
done

lemma map_iterator_linord_rule_P:
assumes "map_iterator_linord it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ it ⟹ k ≤ k';
⋀k'. k' ∈ (dom m)-it ⟹ k' ≤ k⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_linord_def
by (rule map_iterator_genord_rule_P) auto

lemma map_iterator_linord_rule_insert_P:
assumes "map_iterator_linord it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ (dom m - it) ⟹ k ≤ k';
⋀k'. k' ∈ it ⟹ k' ≤ k ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_linord_def
by (rule map_iterator_genord_rule_insert_P) auto

lemma map_iterator_rev_linord_rule_P:
assumes "map_iterator_rev_linord it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ it ⟹ k' ≤ k;
⋀k'. k' ∈ (dom m)-it ⟹ k ≤ k'⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_rev_linord_def
by (rule map_iterator_genord_rule_P) auto

lemma map_iterator_rev_linord_rule_insert_P:
assumes "map_iterator_rev_linord it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ (dom m - it) ⟹ k' ≤ k;
⋀k'. k' ∈ it ⟹ k ≤ k'⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_rev_linord_def
by (rule map_iterator_genord_rule_insert_P) auto
end

subsection ‹Conversions to foldli›

lemma set_iterator_genord_foldli_conv :
"set_iterator_genord iti S R ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
unfolding set_iterator_genord_def by simp

lemma set_iterator_genord_I [intro] :
"⟦distinct l0; S = set l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
set_iterator_genord iti S R" unfolding set_iterator_genord_foldli_conv
by blast

lemma set_iterator_foldli_conv :
"set_iterator iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ iti = foldli l0)"
unfolding set_iterator_def set_iterator_genord_def by simp

lemma set_iterator_I [intro] :
"⟦distinct l0; S = set l0; iti = foldli l0⟧ ⟹
set_iterator iti S"
unfolding set_iterator_foldli_conv
by blast

context linorder begin
lemma set_iterator_linord_foldli_conv :
"set_iterator_linord iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted l0 ∧ iti = foldli l0)"
unfolding set_iterator_linord_def set_iterator_genord_def by (simp add: sorted_sorted_wrt)

lemma set_iterator_linord_I [intro] :
"⟦distinct l0; S = set l0; sorted l0; iti = foldli l0⟧ ⟹
set_iterator_linord iti S"
unfolding set_iterator_linord_foldli_conv
by blast

lemma set_iterator_rev_linord_foldli_conv :
"set_iterator_rev_linord iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted (rev l0) ∧ iti = foldli l0)"
unfolding set_iterator_rev_linord_def set_iterator_genord_def by simp

lemma set_iterator_rev_linord_I [intro] :
"⟦distinct l0; S = set l0; sorted (rev l0); iti = foldli l0⟧ ⟹
set_iterator_rev_linord iti S"
unfolding set_iterator_rev_linord_foldli_conv
by blast
end

lemma map_iterator_genord_foldli_conv :
"map_iterator_genord iti m R ⟷
(∃(l0::('k × 'v) list). distinct (map fst l0) ∧ m = map_of l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
proof -
{ fix l0 :: "('k × 'v) list"
assume dist: "distinct l0"
have "(map_to_set m = set l0) ⟷
(distinct (map fst l0) ∧
m = map_of l0)"
proof (cases "distinct (map fst l0)")
case True thus ?thesis by (metis map_of_map_to_set)
next
case False note not_dist_fst = this

with dist have "~(inj_on fst (set l0))" by (simp add: distinct_map)
hence "set l0 ≠ map_to_set m"
by (rule_tac notI) (simp add: map_to_set_def inj_on_def)
with not_dist_fst show ?thesis by simp
qed
}
thus ?thesis
unfolding set_iterator_genord_def distinct_map
by metis
qed

lemma map_iterator_genord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
map_iterator_genord iti m R"
unfolding map_iterator_genord_foldli_conv
by blast

lemma map_iterator_foldli_conv :
"map_iterator iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ iti = foldli l0)"
unfolding set_iterator_def map_iterator_genord_foldli_conv
by simp

lemma map_iterator_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; iti = foldli l0⟧ ⟹
map_iterator iti m"
unfolding map_iterator_foldli_conv
by blast

context linorder begin

lemma sorted_wrt_keys_map_fst:
"sorted_wrt (λ(k,_) (k',_). R k k') l = sorted_wrt R (map fst l)"
by (induct l) auto

lemma map_iterator_linord_foldli_conv :
"map_iterator_linord iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (map fst l0) ∧ iti = foldli l0)"
unfolding set_iterator_map_linord_def map_iterator_genord_foldli_conv

lemma map_iterator_linord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted (map fst l0); iti = foldli l0⟧ ⟹
map_iterator_linord iti m"
unfolding map_iterator_linord_foldli_conv
by blast

lemma map_iterator_rev_linord_foldli_conv :
"map_iterator_rev_linord iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (rev (map fst l0)) ∧ iti = foldli l0)"
unfolding set_iterator_map_rev_linord_def map_iterator_genord_foldli_conv

lemma map_iterator_rev_linord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted (rev (map fst l0)); iti = foldli l0⟧ ⟹
map_iterator_rev_linord iti m"
unfolding map_iterator_rev_linord_foldli_conv
by blast

end

end


# 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



# Theory Proper_Iterator

section ‹Proper Iterators›
theory Proper_Iterator
imports
SetIteratorOperations
Automatic_Refinement.Refine_Lib
begin
text ‹
Proper iterators provide a way to obtain polymorphic iterators even
inside locale contexts.

For this purpose, an iterator that converts the set to a list is fixed
inside the locale, and polymorphic iterators are described by folding
over the generated list.

In order to ensure efficiency, it is shown that folding over the generated
list is equivalent to directly iterating over the set, and this equivalence
is set up as a code preprocessing rule.
›

subsection ‹Proper Iterators›

text ‹A proper iterator can be expressed as a fold over a list, where
the list does only depend on the set. In particular, it does not depend
on the type of the state. We express this by the following definition,
using two iterators with different types:›

definition proper_it
:: "('x,'σ1) set_iterator ⇒ ('x,'σ2) set_iterator ⇒ bool"
where "proper_it it it' ≡ (∃l. it=foldli l ∧ it'=foldli l)"

lemma proper_itI[intro?]:
fixes it :: "('x,'σ1) set_iterator"
and it' :: "('x,'σ2) set_iterator"
assumes "it=foldli l ∧ it'=foldli l"
shows "proper_it it it'"
using assms unfolding proper_it_def by auto

lemma proper_itE:
fixes it :: "('x,'σ1) set_iterator"
and it' :: "('x,'σ2) set_iterator"
assumes "proper_it it it'"
obtains l where "it=foldli l" and "it'=foldli l"
using assms unfolding proper_it_def by auto

lemma proper_it_parE:
fixes it :: "'a ⇒ ('x,'σ1) set_iterator"
and it' :: "'a ⇒ ('x,'σ2) set_iterator"
assumes "∀x. proper_it (it x) (it' x)"
obtains f where "it = (λx. foldli (f x))" and "it' = (λx. foldli (f x))"
using assms unfolding proper_it_def
by metis

definition
proper_it'
where "proper_it' it it' ≡ ∀s. proper_it (it s) (it' s)"

lemma proper_it'I:
"⟦⋀s. proper_it (it s) (it' s)⟧ ⟹ proper_it' it it'"
unfolding proper_it'_def by blast

lemma proper_it'D:
"proper_it' it it' ⟹ proper_it (it s) (it' s)"
unfolding proper_it'_def by blast

subsubsection ‹Properness Preservation›
ML ‹
structure Icf_Proper_Iterator = struct

structure icf_proper_iteratorI = Named_Thms
( val name = @{binding icf_proper_iteratorI_raw}
val description = "ICF (internal): Rules to show properness of iterators" )

val get = icf_proper_iteratorI.get

fun del_thm thm = icf_proper_iteratorI.del_thm thm

val del = Thm.declaration_attribute del_thm

val setup = I
#> icf_proper_iteratorI.setup
#> Attrib.setup @{binding icf_proper_iteratorI}
("ICF: Rules to show properness of iterators")
get o Context.proof_of
)

end
›
setup ‹Icf_Proper_Iterator.setup›

lemma proper_iterator_trigger:
"proper_it it it' ⟹ proper_it it it'"
"proper_it' itf itf' ⟹ proper_it' itf itf'" .

declaration ‹
Tagged_Solver.declare_solver @{thms proper_iterator_trigger}
@{binding proper_iterator} "Proper iterator solver"
(fn ctxt => REPEAT_ALL_NEW (resolve_tac ctxt (Icf_Proper_Iterator.get ctxt)))
›

lemma pi_foldli[icf_proper_iteratorI]:
"proper_it (foldli l :: ('a,'σ) set_iterator) (foldli l)"
unfolding proper_it_def
by auto

lemma pi_foldri[icf_proper_iteratorI]:
"proper_it (foldri l :: ('a,'σ) set_iterator) (foldri l)"
unfolding proper_it_def foldri_def by auto

lemma pi'_foldli[icf_proper_iteratorI]:
"proper_it' (foldli o tsl) (foldli o tsl)"
apply (tagged_solver)
done

lemma pi'_foldri[icf_proper_iteratorI]:
"proper_it' (foldri o tsl) (foldri o tsl)"
apply (tagged_solver)
done

text ‹Iterator combinators preserve properness›
lemma pi_emp[icf_proper_iteratorI]:
"proper_it set_iterator_emp set_iterator_emp"
unfolding proper_it_def set_iterator_emp_def[abs_def]
by (auto intro!: ext exI[where x="[]"])

lemma pi_sng[icf_proper_iteratorI]:
"proper_it (set_iterator_sng x) (set_iterator_sng x)"
unfolding proper_it_def set_iterator_sng_def[abs_def]
by (auto intro!: ext exI[where x="[x]"])

lemma pi_union[icf_proper_iteratorI]:
assumes PA: "proper_it it_a it_a'"
assumes PB: "proper_it it_b it_b'"
shows "proper_it (set_iterator_union it_a it_b)
(set_iterator_union it_a' it_b')"
unfolding set_iterator_union_def
apply (rule proper_itE[OF PA])
apply (rule proper_itE[OF PB])
apply (rule_tac l="l@la" in proper_itI)
apply simp
apply (intro conjI ext)
done

lemma pi_product[icf_proper_iteratorI]:
fixes it_a :: "('a,'σa) set_iterator"
fixes it_b :: "'a ⇒ ('b,'σa) set_iterator"
assumes PA: "proper_it it_a it_a'"
and PB: "⋀x. proper_it (it_b x) (it_b' x)"
shows "proper_it (set_iterator_product it_a it_b)
(set_iterator_product it_a' it_b')"
proof -
from PB have PB': "∀x. proper_it (it_b x) (it_b' x)" ..
show ?thesis
unfolding proper_it_def
apply (rule proper_itE[OF PA])
apply (rule proper_it_parE[OF PB'])
done
qed

lemma pi_image_filter[icf_proper_iteratorI]:
fixes it :: "('x,'σ1) set_iterator"
and it' :: "('x,'σ2) set_iterator"
and g :: "'x ⇒ 'y option"
assumes P: "proper_it it it'"
shows "proper_it (set_iterator_image_filter g it)
(set_iterator_image_filter g it')"
unfolding proper_it_def
apply (rule proper_itE[OF P])
apply (auto simp: set_iterator_image_filter_foldli_conv)
done

lemma pi_filter[icf_proper_iteratorI]:
assumes P: "proper_it it it'"
shows "proper_it (set_iterator_filter P it)
(set_iterator_filter P it')"
unfolding proper_it_def
apply (rule proper_itE[OF P])
by (auto simp: set_iterator_filter_foldli_conv)

lemma pi_image[icf_proper_iteratorI]:
assumes P: "proper_it it it'"
shows "proper_it (set_iterator_image g it)
(set_iterator_image g it')"
unfolding proper_it_def
apply (rule proper_itE[OF P])
by (auto simp: set_iterator_image_foldli_conv)

lemma pi_dom[icf_proper_iteratorI]:
assumes P: "proper_it it it'"
shows "proper_it (map_iterator_dom it)
(map_iterator_dom it')"
unfolding proper_it_def
apply (rule proper_itE[OF P])
by (auto simp: map_iterator_dom_foldli_conv)

lemma set_iterator_product_eq2:
assumes "∀a∈set la. itb a = itb' a"
shows "set_iterator_product (foldli la) itb
= set_iterator_product (foldli la) itb'"
proof (intro ext)
fix c f σ
show "set_iterator_product (foldli la) itb c f σ
= set_iterator_product (foldli la) itb' c f σ"
using assms
unfolding set_iterator_product_def
apply (induct la arbitrary: σ)
apply (auto)
done
qed

subsubsection ‹Optimizing Folds›
text ‹
Using an iterator to create a list. The optimizations will
match the pattern ‹foldli (it_to_list it s)›
›
definition "it_to_list it s ≡ (it s) (λ_. True) (λx l. l@[x]) []"

lemma map_it_to_list_genord_correct:
assumes A: "map_iterator_genord (it s) m (λ(k,_) (k',_). R k k')"
shows "map_of (it_to_list it s) = m
∧ distinct (map fst (it_to_list it s))
∧ sorted_wrt R ((map fst (it_to_list it s)))"
unfolding it_to_list_def
apply (rule map_iterator_genord_rule_insert_P[OF A, where I="
λit l. map_of l = m | it
∧ distinct (map fst l)
∧ sorted_wrt R ((map fst l))
"])
apply auto
apply (auto simp: restrict_map_def) []
apply (metis Some_eq_map_of_iff restrict_map_eq(2))
by (metis (lifting) restrict_map_eq(2) weak_map_of_SomeI)

lemma (in linorder) map_it_to_list_linord_correct:
assumes A: "map_iterator_linord (it s) m"
shows "map_of (it_to_list it s) = m
∧ distinct (map fst (it_to_list it s))
∧ sorted ((map fst (it_to_list it s)))"
using map_it_to_list_genord_correct[where it=it,
OF A[unfolded set_iterator_map_linord_def]]

lemma (in linorder) map_it_to_list_rev_linord_correct:
assumes A: "map_iterator_rev_linord (it s) m"
shows "map_of (it_to_list it s) = m
∧ distinct (map fst (it_to_list it s))
∧ sorted (rev (map fst (it_to_list it s)))"
using map_it_to_list_genord_correct[where it=it,
OF A[unfolded set_iterator_map_rev_linord_def]]
by simp

end


# Theory It_to_It

theory It_to_It
imports
Proper_Iterator
begin

lemma proper_it_fold:
"proper_it it it' ⟹ foldli (it (λ_. True) (λx l. l@[x]) []) = it'"
unfolding proper_it_def by auto
lemma proper_it_unfold:
"proper_it it it' ⟹ it' = foldli (it (λ_. True) (λx l. l@[x]) [])"
unfolding proper_it_def by auto

text ‹The following constant converts an iterator over list-state
to an iterator over arbitrary state›
definition it_to_it :: "('x,'x list) set_iterator ⇒ ('x,'σ) set_iterator"
where [code del]: "it_to_it it
≡ (foldli (it (λ_. True) (λx l. l@[x]) []))"

lemma pi_it_to_it[icf_proper_iteratorI]: "proper_it (it_to_it I) (it_to_it I)"
unfolding it_to_it_def by (rule pi_foldli)
text ‹In case of a proper iterator, it is equivalent to direct iteration›
lemma it_to_it_fold: "proper_it it (it'::('x,'σ) set_iterator)
⟹ it_to_it it = it'"
unfolding it_to_it_def

lemma it_to_it_map_fold:
assumes P: "proper_it it it'"
shows "it_to_it (λc f. it c (f ∘ f')) = (λc f. it' c (f o f'))"
apply (rule proper_itE[OF P])
unfolding it_to_it_def
apply (intro ext)
apply (simp add: foldli_foldl map_by_foldl foldli_map)
done

lemma it_to_it_fold': "proper_it' it (it'::'s ⇒ ('x,'σ) set_iterator)
⟹ it_to_it (it s) = (it' s)"
by (drule proper_it'D) (rule it_to_it_fold)

lemma it_to_it_map_fold':
assumes P: "proper_it' it it'"
shows "it_to_it (λc f. it s c (f ∘ f')) = (λc f. it' s c (f o f'))"
using P[THEN proper_it'D] by (rule it_to_it_map_fold)

text ‹This locale wraps up the setup of a proper iterator for use
with ‹it_to_it›.›
locale proper_it_loc =
fixes it :: "'s ⇒ ('x,'x list) set_iterator"
and it' :: "'s ⇒ ('x,'σ) set_iterator"
assumes proper': "proper_it' it it'"
begin
lemma proper: "proper_it (it s) (it' s)"
using proper' by (rule proper_it'D)

lemmas it_to_it_code_unfold[code_unfold] = it_to_it_fold[OF proper]
end

subsubsection ‹Correctness›
text ‹The polymorphic iterator is a valid iterator again.›
lemma it_to_it_genord_correct:
assumes "set_iterator_genord (it::('x,'x list) set_iterator) S R"
shows "set_iterator_genord ((it_to_it it)::('x,'σ) set_iterator) S R"
proof -
interpret set_iterator_genord it S R by fact

show ?thesis
apply (unfold_locales)
unfolding it_to_it_def
using foldli_transform
by auto
qed

lemma it_to_it_linord_correct:
assumes "set_iterator_linord (it::('x::linorder,'x list) set_iterator) S"
shows "set_iterator_linord ((it_to_it it)::('x,'σ) set_iterator) S"
using assms
unfolding set_iterator_linord_def
by (rule it_to_it_genord_correct)

lemma it_to_it_rev_linord_correct:
assumes "set_iterator_rev_linord (it::('x::linorder,'x list) set_iterator) S"
shows "set_iterator_rev_linord ((it_to_it it)::('x,'σ) set_iterator) S"
using assms
unfolding set_iterator_rev_linord_def
by (rule it_to_it_genord_correct)

lemma it_to_it_correct:
assumes "set_iterator (it::('x,'x list) set_iterator) S"
shows "set_iterator ((it_to_it it)::('x,'σ) set_iterator) S"
using assms
unfolding set_iterator_def
by (rule it_to_it_genord_correct)

lemma it_to_it_map_genord_correct:
assumes "map_iterator_genord (it::('u,'v,('u×'v) list) map_iterator) S R"
shows "map_iterator_genord ((it_to_it it)::('u,'v,'σ) map_iterator) S R"
using assms by (rule it_to_it_genord_correct)

lemma it_to_it_map_linord_correct:
assumes "map_iterator_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S"
shows "map_iterator_linord ((it_to_it it)::('u,'v,'σ) map_iterator) S"
using assms unfolding set_iterator_map_linord_def by (rule it_to_it_genord_correct)

lemma it_to_it_map_rev_linord_correct:
assumes
"map_iterator_rev_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S"
shows "map_iterator_rev_linord ((it_to_it it)::('u,'v,'σ) map_iterator) S"
using assms unfolding set_iterator_map_rev_linord_def
by (rule it_to_it_genord_correct)

lemma it_to_it_map_correct:
assumes "map_iterator (it::('u,'v,('u×'v) list) map_iterator) S"
shows "map_iterator ((it_to_it it)::('u,'v,'σ) map_iterator) S"
using assms by (rule it_to_it_correct)

end


# Theory SetIteratorGA

(*  Title:       General Algorithms for Iterators
Author:      Thomas Tuerk <tuerk@in.tum.de>
Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹General Algorithms for Iterators over Finite Sets›
theory SetIteratorGA
imports Main SetIteratorOperations
begin

subsection ‹Quantification›

definition iterate_ball where
"iterate_ball (it::('x,bool) set_iterator) P = it id (λx σ. P x) True"

lemma iterate_ball_correct :
assumes it: "set_iterator it S0"
shows "iterate_ball it P = (∀x∈S0. P x)"
unfolding iterate_ball_def
apply (rule set_iterator_rule_P [OF it,
where I = "λS σ. σ = (∀x∈S0-S. P x)"])
apply auto
done

definition iterate_bex where
"iterate_bex (it::('x,bool) set_iterator) P = it (λσ. ¬σ) (λx σ. P x) False"

lemma iterate_bex_correct :
assumes it: "set_iterator it S0"
shows "iterate_bex it P = (∃x∈S0. P x)"
unfolding iterate_bex_def
apply (rule set_iterator_rule_P [OF it, where I = "λS σ. σ = (∃x∈S0-S. P x)"])
apply auto
done

subsection ‹Iterator to List›

definition iterate_to_list where
"iterate_to_list (it::('x,'x list) set_iterator) = it (λ_. True) (λx σ. x # σ) []"

lemma iterate_to_list_foldli [simp] :
"iterate_to_list (foldli xs) = rev xs"
unfolding iterate_to_list_def
by (induct xs rule: rev_induct, simp_all add: foldli_snoc)

lemma iterate_to_list_genord_correct :
assumes it: "set_iterator_genord it S0 R"
shows "set (iterate_to_list it) = S0 ∧ distinct (iterate_to_list it) ∧
sorted_wrt R (rev (iterate_to_list it))"
using it unfolding set_iterator_genord_foldli_conv by auto

lemma iterate_to_list_correct :
assumes it: "set_iterator it S0"
shows "set (iterate_to_list it) = S0 ∧ distinct (iterate_to_list it)"
using iterate_to_list_genord_correct [OF it[unfolded set_iterator_def]]
by simp

lemma (in linorder) iterate_to_list_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_linord it S0"
shows "set (iterate_to_list it) = S0 ∧ distinct (iterate_to_list it) ∧
sorted (rev (iterate_to_list it))"
using it_OK unfolding set_iterator_linord_foldli_conv by auto

lemma (in linorder) iterate_to_list_rev_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_rev_linord it S0"
shows "set (iterate_to_list it) = S0 ∧ distinct (iterate_to_list it) ∧
sorted (iterate_to_list it)"
using it_OK unfolding set_iterator_rev_linord_foldli_conv by auto

lemma (in linorder) iterate_to_list_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "map_of (iterate_to_list it) = m ∧ distinct (map fst (iterate_to_list it)) ∧
sorted (map fst (rev (iterate_to_list it)))"
using it_OK unfolding map_iterator_linord_foldli_conv

lemma (in linorder) iterate_to_list_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "map_of (iterate_to_list it) = m ∧ distinct (map fst (iterate_to_list it)) ∧
sorted (map fst (iterate_to_list it))"
using it_OK unfolding map_iterator_rev_linord_foldli_conv

subsection ‹Size›

lemma set_iterator_finite :
assumes it: "set_iterator it S0"
shows "finite S0"
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]] .

lemma map_iterator_finite :
assumes it: "map_iterator it m"
shows "finite (dom m)"
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]

definition iterate_size where
"iterate_size (it::('x,nat) set_iterator) = it (λ_. True) (λx σ. Suc σ) 0"

lemma iterate_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_size it = card S0 ∧ finite S0"
unfolding iterate_size_def
apply (rule_tac set_iterator_rule_insert_P [OF it,
where I = "λS σ. σ = card S ∧ finite S"])
apply auto
done

definition iterate_size_abort where
"iterate_size_abort (it::('x,nat) set_iterator) n = it (λσ. σ < n) (λx σ. Suc σ) 0"

lemma iterate_size_abort_correct :
assumes it: "set_iterator it S0"
shows "iterate_size_abort it n = (min n (card S0)) ∧ finite S0"
unfolding iterate_size_abort_def
proof (rule set_iterator_rule_insert_P [OF it,
where I = "λS σ. σ = (min n (card S)) ∧ finite S"], goal_cases)
case (4 σ S)
assume "S ⊆ S0" "S ≠ S0" "¬ σ < n" "σ = min n (card S) ∧ finite S"

from ‹σ = min n (card S) ∧ finite S› ‹¬ σ < n›
have "σ = n" "n ≤ card S"

note fin_S0 = set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
from card_mono [OF fin_S0 ‹S ⊆ S0›] have "card S ≤ card S0" .

with ‹σ = n› ‹n ≤ card S› fin_S0
show "σ = min n (card S0) ∧ finite S0" by simp
qed simp_all

subsection ‹Emptyness Check›

definition iterate_is_empty_by_size where
"iterate_is_empty_by_size it = (iterate_size_abort it 1 = 0)"

lemma iterate_is_empty_by_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty_by_size it = (S0 = {})"
using iterate_size_abort_correct[OF it, of 1]
unfolding iterate_is_empty_by_size_def
by (cases "card S0") auto

definition iterate_is_empty where
"iterate_is_empty (it::('x,bool) set_iterator) = (it (λb. b) (λ_ _. False) True)"

lemma iterate_is_empty_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty it = (S0 = {})"
unfolding iterate_is_empty_def
apply (rule set_iterator_rule_insert_P [OF it,
where I = "λS σ. σ ⟷ S = {}"])
apply auto
done

subsection ‹Check for singleton Sets›

definition iterate_is_sng where
"iterate_is_sng it = (iterate_size_abort it 2 = 1)"

lemma iterate_is_sng_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_sng it = (card S0 = 1)"
using iterate_size_abort_correct[OF it, of 2]
unfolding iterate_is_sng_def
apply (cases "card S0", simp, rename_tac n')
apply (case_tac n')
apply auto
done

subsection ‹Selection›

definition iterate_sel where
"iterate_sel (it::('x,'y option) set_iterator) f = it (λσ. σ = None) (λx σ. f x) None"

lemma iterate_sel_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel it f = None ⟷ (∀x∈S0. (f x = None))"
"iterate_sel it f = Some y ⟹ (∃x ∈ S0. f x = Some y ∧ (∀x' ∈ S0-{x}. ∀y. f x' = Some y' ⟶ R x x'))"
proof -
show "iterate_sel it f = None ⟷ (∀x∈S0. (f x = None))"
unfolding iterate_sel_def
apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK,
where I = "λS σ. (σ = None) ⟷ (∀x∈S. (f x = None))"])
apply auto
done
next
have "iterate_sel it f = Some y ⟶ (∃x ∈ S0. f x = Some y ∧ (∀x' ∈ S0-{x}. ∀y'. f x' = Some y' ⟶ R x x'))"
unfolding iterate_sel_def
apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK,
where I = "λS σ. (∀y. σ = Some y ⟶ (∃x ∈ S. f x = Some y ∧ (∀x' ∈ S-{x}.∀y'. f x' = Some y' ⟶ R x x'))) ∧
((σ = None) ⟷ (∀x∈S. f x = None))"])
apply simp
apply (auto simp add: Bex_def subset_iff Ball_def)
apply metis
done
moreover assume "iterate_sel it f = Some y"
finally show "(∃x ∈ S0. f x = Some y ∧ (∀x' ∈ S0-{x}. ∀y. f x' = Some y' ⟶ R x x'))" by blast
qed

definition iterate_sel_no_map where
"iterate_sel_no_map it P = iterate_sel it (λx. if P x then Some x else None)"
lemmas iterate_sel_no_map_alt_def = iterate_sel_no_map_def[unfolded iterate_sel_def, code]

lemma iterate_sel_no_map_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ (x ∈ S0 ∧ P x ∧ (∀x' ∈ S0-{x}. P x' ⟶ R x x'))"
unfolding iterate_sel_no_map_def
using iterate_sel_genord_correct[OF it_OK, of "λx. if P x then Some x else None"]
apply (metis option.inject option.simps(2))
done

lemma iterate_sel_no_map_correct :
assumes it_OK: "set_iterator it S0"
shows "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ x ∈ S0 ∧ P x"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ x ∈ S0 ∧ P x"
by simp_all
qed

lemma (in linorder) iterate_sel_no_map_linord_correct :
assumes it_OK: "set_iterator_linord it S0"
shows "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ (x ∈ S0 ∧ P x ∧ (∀x'∈S0. P x' ⟶ x ≤ x'))"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_linord_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ (x ∈ S0 ∧ P x ∧ (∀x'∈S0. P x' ⟶ x ≤ x'))"
by auto
qed

lemma (in linorder) iterate_sel_no_map_rev_linord_correct :
assumes it_OK: "set_iterator_rev_linord it S0"
shows "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ (x ∈ S0 ∧ P x ∧ (∀x'∈S0. P x' ⟶ x' ≤ x))"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_rev_linord_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀x∈S0. ¬(P x))"
"iterate_sel_no_map it P = Some x ⟹ (x ∈ S0 ∧ P x ∧ (∀x'∈S0. P x' ⟶ x' ≤ x))"
by auto
qed

lemma iterate_sel_no_map_map_correct :
assumes it_OK: "map_iterator it m"
shows "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v))"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v))"
qed

lemma (in linorder) iterate_sel_no_map_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v) ∧ (∀k' v' . m k' = Some v' ∧
P (k', v') ⟶ k ≤ k'))"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_linord_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v) ∧ (∀k' v' . m k' = Some v' ∧
P (k', v') ⟶ k ≤ k'))"
apply (auto simp add: map_to_set_def Ball_def)
done
qed

lemma (in linorder) iterate_sel_no_map_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v) ∧ (∀k' v' . m k' = Some v' ∧
P (k', v') ⟶ k' ≤ k))"
proof -
note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_rev_linord_def], of P]
thus "iterate_sel_no_map it P = None ⟷ (∀k v. m k = Some v ⟶ ¬(P (k, v)))"
"iterate_sel_no_map it P = Some (k, v) ⟹ (m k = Some v ∧ P (k, v) ∧ (∀k' v' . m k' = Some v' ∧
P (k', v') ⟶ k' ≤ k))"
apply (auto simp add: map_to_set_def Ball_def)
done
qed

subsection ‹Creating ordered iterators›

text ‹One can transform an iterator into an ordered one by converting it to list,
sorting this list and then converting back to an iterator. In general, this brute-force
method is inefficient, though.›

definition iterator_to_ordered_iterator where
"iterator_to_ordered_iterator sort_fun it =
foldli (sort_fun (iterate_to_list it))"

lemma iterator_to_ordered_iterator_correct :
assumes sort_fun_OK: "⋀l. sorted_wrt R (sort_fun l) ∧ mset (sort_fun l) = mset l"
and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R"
proof -
define l where "l = iterate_to_list it"
have l_props: "set l = S0" "distinct l"
using iterate_to_list_correct [OF it_OK, folded l_def] by simp_all

with sort_fun_OK[of l] have sort_l_props:
"sorted_wrt R (sort_fun l)"
"set (sort_fun l) = S0" "distinct (sort_fun l)"
apply (simp_all)
apply (metis set_mset_mset)
apply (metis distinct_count_atmost_1 set_mset_mset)
done

show ?thesis
apply (rule set_iterator_genord_I[of "sort_fun l"])
apply (simp_all add: sort_l_props iterator_to_ordered_iterator_def l_def[symmetric])
done
qed

definition iterator_to_ordered_iterator_quicksort where
"iterator_to_ordered_iterator_quicksort R it =
iterator_to_ordered_iterator (quicksort_by_rel R []) it"

lemmas iterator_to_ordered_iterator_quicksort_code[code] =
iterator_to_ordered_iterator_quicksort_def[unfolded iterator_to_ordered_iterator_def]

lemma iterator_to_ordered_iterator_quicksort_correct :
assumes lin : "⋀x y. (R x y) ∨ (R y x)"
and trans_R: "⋀x y z. R x y ⟹ R y z ⟹ R x z"
and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_quicksort R it) S0 R"
unfolding iterator_to_ordered_iterator_quicksort_def
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
apply (simp_all add: sorted_wrt_quicksort_by_rel[OF lin trans_R])
done

definition iterator_to_ordered_iterator_mergesort where
"iterator_to_ordered_iterator_mergesort R it =
iterator_to_ordered_iterator (mergesort_by_rel R) it"

lemmas iterator_to_ordered_iterator_mergesort_code[code] =
iterator_to_ordered_iterator_mergesort_def[unfolded iterator_to_ordered_iterator_def]

lemma iterator_to_ordered_iterator_mergesort_correct :
assumes lin : "⋀x y. (R x y) ∨ (R y x)"
and trans_R: "⋀x y z. R x y ⟹ R y z ⟹ R x z"
and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_mergesort R it) S0 R"
unfolding iterator_to_ordered_iterator_mergesort_def
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
apply (simp_all add: sorted_wrt_mergesort_by_rel[OF lin trans_R])
done

end



# Theory Gen_Iterator

section ‹\isaheader{Iterators}›
theory Gen_Iterator
begin
text ‹
Iterators are realized by to-list functions followed by folding.
A post-optimization step then replaces these constructions by
real iterators.›

lemma param_it_to_list[param]: "(it_to_list,it_to_list) ∈
(Rs → (Ra → bool_rel) →
(Rb → ⟨Rb⟩list_rel → ⟨Rb⟩list_rel) → ⟨Rc⟩list_rel → Rd) → Rs → Rd"
unfolding it_to_list_def[abs_def]
by parametricity

definition key_rel :: "('k ⇒ 'k ⇒ bool) ⇒ ('k×'v) ⇒ ('k×'v) ⇒ bool"
where "key_rel R a b ≡ R (fst a) (fst b)"

lemma key_rel_UNIV[simp]: "key_rel (λ_ _. True) = (λ_ _. True)"
unfolding key_rel_def[abs_def] by auto

subsection ‹Setup for Autoref›
text ‹Default pattern rules for ‹it_to_sorted_list››
definition "set_to_sorted_list R S ≡ it_to_sorted_list R S"
lemma set_to_sorted_list_itype[autoref_itype]:
"set_to_sorted_list R ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨⟨I⟩⇩ii_list⟩⇩ii_nres"
by simp

context begin interpretation autoref_syn .
lemma set_to_sorted_list_pat[autoref_op_pat]:
"it_to_sorted_list R S ≡ OP (set_to_sorted_list R) S"
unfolding set_to_sorted_list_def[abs_def] by auto
end

definition "map_to_sorted_list R M
≡ it_to_sorted_list (key_rel R) (map_to_set M)"
lemma map_to_sorted_list_itype[autoref_itype]:
"map_to_sorted_list R ::⇩i ⟨Rk,Rv⟩⇩ii_map →⇩i ⟨⟨⟨Rk,Rv⟩⇩ii_prod⟩⇩ii_list⟩⇩ii_nres"
by simp

context begin interpretation autoref_syn .
lemma map_to_sorted_list_pat[autoref_op_pat]:
"it_to_sorted_list (key_rel R) (map_to_set M)
≡ OP (map_to_sorted_list R) M"
"it_to_sorted_list (λ_ _. True) (map_to_set M)
≡ OP (map_to_sorted_list (λ_ _. True)) M"
unfolding map_to_sorted_list_def[abs_def] by auto
end

subsection ‹Set iterators›
(*definition "is_set_to_sorted_list_deprecated ordR Rk Rs tsl ≡ ∀s s'.
(s,s')∈⟨Rk⟩Rs ⟶
(RETURN (tsl s),it_to_sorted_list ordR s')∈⟨⟨Rk⟩list_rel⟩nres_rel"
*)

definition "is_set_to_sorted_list ordR Rk Rs tsl ≡ ∀s s'.
(s,s')∈⟨Rk⟩Rs
⟶ ( ∃l'. (tsl s,l')∈⟨Rk⟩list_rel
∧ RETURN l' ≤ it_to_sorted_list ordR s')"

definition "is_set_to_list ≡ is_set_to_sorted_list (λ_ _. True)"

lemma is_set_to_sorted_listE:
assumes "is_set_to_sorted_list ordR Rk Rs tsl"
assumes "(s,s')∈⟨Rk⟩Rs"
obtains l' where "(tsl s,l')∈⟨Rk⟩list_rel"
and "RETURN l' ≤ it_to_sorted_list ordR s'"
using assms unfolding is_set_to_sorted_list_def by blast

(* TODO: Move *)
lemma it_to_sorted_list_weaken:
"R≤R' ⟹ it_to_sorted_list R s ≤ it_to_sorted_list R' s"
unfolding it_to_sorted_list_def
by (auto intro!: sorted_wrt_mono_rel[where P=R])

lemma set_to_list_by_set_to_sorted_list[autoref_ga_rules]:
assumes "GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)"
shows "is_set_to_list Rk Rs tsl"
using assms
unfolding is_set_to_list_def is_set_to_sorted_list_def autoref_tag_defs
apply (safe)
apply (drule spec, drule spec, drule (1) mp)
apply (elim exE conjE)
apply (rule exI, rule conjI, assumption)
apply (rule order_trans, assumption)
apply (rule it_to_sorted_list_weaken)
by blast

definition "det_fold_set R c f σ result ≡
∀l. distinct l ∧ sorted_wrt R l ⟶ foldli l c f σ = result (set l)"

lemma det_fold_setI[intro?]:
assumes "⋀l. ⟦distinct l; sorted_wrt R l⟧
⟹ foldli l c f σ = result (set l)"
shows "det_fold_set R c f σ result"
using assms unfolding det_fold_set_def by auto

text ‹Template lemma for generic algorithm using set iterator›
lemma det_fold_sorted_set:
assumes 1: "det_fold_set ordR c' f' σ' result"
assumes 2: "is_set_to_sorted_list ordR Rk Rs tsl"
assumes SREF[param]: "(s,s')∈⟨Rk⟩Rs"
assumes [param]:  "(c,c')∈Rσ→Id"
assumes [param]: "(f,f')∈Rk → Rσ → Rσ"
assumes [param]: "(σ,σ')∈Rσ"
shows "(foldli (tsl s) c f σ, result s') ∈ Rσ"
proof -
obtain tsl' where
[param]: "(tsl s,tsl') ∈ ⟨Rk⟩list_rel"
and IT: "RETURN tsl' ≤ it_to_sorted_list ordR s'"
using 2 SREF
by (rule is_set_to_sorted_listE)

have "(foldli (tsl s) c f σ, foldli tsl' c' f' σ') ∈ Rσ"
by parametricity
also have "foldli tsl' c' f' σ' = result s'"
using 1 IT
unfolding det_fold_set_def it_to_sorted_list_def
by simp
finally show ?thesis .
qed

lemma det_fold_set:
assumes "det_fold_set (λ_ _. True) c' f' σ' result"
assumes "is_set_to_list Rk Rs tsl"
assumes "(s,s')∈⟨Rk⟩Rs"
assumes "(c,c')∈Rσ→Id"
assumes "(f,f')∈Rk → Rσ → Rσ"
assumes "(σ,σ')∈Rσ"
shows "(foldli (tsl s) c f σ, result s') ∈ Rσ"
using assms
unfolding  is_set_to_list_def
by (rule det_fold_sorted_set)

subsection ‹Map iterators›

text ‹Build relation on keys›

(*definition "is_map_to_sorted_list_deprecated ordR Rk Rv Rm tsl ≡ ∀m m'.
(m,m')∈⟨Rk,Rv⟩Rm ⟶
(RETURN (tsl m),it_to_sorted_list (key_rel ordR) (map_to_set m'))
∈⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"*)

definition "is_map_to_sorted_list ordR Rk Rv Rm tsl ≡ ∀m m'.
(m,m')∈⟨Rk,Rv⟩Rm ⟶ (
∃l'. (tsl m,l')∈⟨⟨Rk,Rv⟩prod_rel⟩list_rel
∧ RETURN l' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m'))"

definition "is_map_to_list Rk Rv Rm tsl
≡ is_map_to_sorted_list (λ_ _. True) Rk Rv Rm tsl"

lemma is_map_to_sorted_listE:
assumes "is_map_to_sorted_list ordR Rk Rv Rm tsl"
assumes "(m,m')∈⟨Rk,Rv⟩Rm"
obtains l' where "(tsl m,l')∈⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and "RETURN l' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m')"
using assms unfolding is_map_to_sorted_list_def by blast

lemma map_to_list_by_map_to_sorted_list[autoref_ga_rules]:
assumes "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)"
shows "is_map_to_list Rk Rv Rm tsl"
using assms
unfolding is_map_to_list_def is_map_to_sorted_list_def autoref_tag_defs
apply (safe)
apply (drule spec, drule spec, drule (1) mp)
apply (elim exE conjE)
apply (rule exI, rule conjI, assumption)
apply (rule order_trans, assumption)
apply (rule it_to_sorted_list_weaken)
unfolding key_rel_def[abs_def]
by blast

definition "det_fold_map R c f σ result ≡
∀l. distinct (map fst l) ∧ sorted_wrt (key_rel R) l
⟶ foldli l c f σ = result (map_of l)"

lemma det_fold_mapI[intro?]:
assumes "⋀l. ⟦distinct (map fst l); sorted_wrt (key_rel R) l⟧
⟹ foldli l c f σ = result (map_of l)"
shows "det_fold_map R c f σ result"
using assms unfolding det_fold_map_def by auto

lemma det_fold_map_aux:
assumes 1: "⟦distinct (map fst l); sorted_wrt (key_rel R) l ⟧
⟹ foldli l c f σ = result (map_of l)"
assumes 2: "RETURN l ≤ it_to_sorted_list (key_rel R) (map_to_set m)"
shows "foldli l c f σ = result m"
proof -
from 2 have "distinct l" and "set l = map_to_set m"
and SORTED: "sorted_wrt (key_rel R) l"
unfolding it_to_sorted_list_def by simp_all
hence "∀(k,v)∈set l. ∀(k',v')∈set l. k=k' ⟶ v=v'"
apply simp
unfolding map_to_set_def
apply auto
done
with ‹distinct l› have DF: "distinct (map fst l)"
apply (induct l)
apply simp
apply force
done
with ‹set l = map_to_set m› have [simp]: "m = map_of l"
by (metis map_of_map_to_set)

from 1[OF DF SORTED] show ?thesis by simp
qed

text ‹Template lemma for generic algorithm using map iterator›
lemma det_fold_sorted_map:
assumes 1: "det_fold_map ordR c' f' σ' result"
assumes 2: "is_map_to_sorted_list ordR Rk Rv Rm tsl"
assumes MREF[param]: "(m,m')∈⟨Rk,Rv⟩Rm"
assumes [param]:  "(c,c')∈Rσ→Id"
assumes [param]: "(f,f')∈⟨Rk,Rv⟩prod_rel → Rσ → Rσ"
assumes [param]: "(σ,σ')∈Rσ"
shows "(foldli (tsl m) c f σ, result m') ∈ Rσ"
proof -
obtain tsl' where
[param]: "(tsl m,tsl') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and IT: "RETURN tsl' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m')"
using 2 MREF by (rule is_map_to_sorted_listE)

have "(foldli (tsl m) c f σ, foldli tsl' c' f' σ') ∈ Rσ"
by parametricity
also have "foldli tsl' c' f' σ' = result m'"
using det_fold_map_aux[of tsl' ordR c' f' σ' result] 1 IT
unfolding det_fold_map_def
by clarsimp
finally show ?thesis .
qed

lemma det_fold_map:
assumes "det_fold_map (λ_ _. True) c' f' σ' result"
assumes "is_map_to_list Rk Rv Rm tsl"
assumes "(m,m')∈⟨Rk,Rv⟩Rm"
assumes "(c,c')∈Rσ→Id"
assumes "(f,f')∈⟨Rk,Rv⟩prod_rel → Rσ → Rσ"
assumes "(σ,σ')∈Rσ"
shows "(foldli (tsl m) c f σ, result m') ∈ Rσ"
using assms
unfolding is_map_to_list_def
by (rule det_fold_sorted_map)

lemma set_to_sorted_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 11)"
assumes TSL: "SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)"
shows "(λs. RETURN (tsl s), set_to_sorted_list R)
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
proof (intro fun_relI nres_relI)
fix s s'
assume "(s,s')∈⟨Rk⟩Rs"
with TSL obtain l' where
R1: "(tsl s, l') ∈ ⟨Rk⟩list_rel"
and R2: "RETURN l' ≤ set_to_sorted_list R s'"
unfolding is_set_to_sorted_list_def set_to_sorted_list_def autoref_tag_defs
by blast

have "RETURN (tsl s) ≤ ⇓(⟨Rk⟩list_rel) (RETURN l')"
by (rule RETURN_refine) fact
also note R2
finally show "RETURN (tsl s) ≤ ⇓ (⟨Rk⟩list_rel) (set_to_sorted_list R s')" .
qed

lemma set_to_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 10)"
assumes TSL: "SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)"
shows "(λs. RETURN (tsl s), set_to_sorted_list (λ_ _. True))
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
using assms(2-) unfolding is_set_to_list_def
by (rule set_to_sorted_list_by_tsl[OF PRIO_TAGI])

lemma map_to_sorted_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 11)"
assumes TSL: "SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)"
shows "(λs. RETURN (tsl s), map_to_sorted_list R)
∈ ⟨Rk,Rv⟩Rs → ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"
proof (intro fun_relI nres_relI)
fix s s'
assume "(s,s')∈⟨Rk,Rv⟩Rs"
with TSL obtain l' where
R1: "(tsl s, l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and R2: "RETURN l' ≤ map_to_sorted_list R s'"
unfolding is_map_to_sorted_list_def map_to_sorted_list_def autoref_tag_defs
by blast

have "RETURN (tsl s) ≤ ⇓(⟨⟨Rk,Rv⟩prod_rel⟩list_rel) (RETURN l')"
apply (rule RETURN_refine)
by fact
also note R2
finally show
"RETURN (tsl s) ≤ ⇓ (⟨⟨Rk,Rv⟩prod_rel⟩list_rel) (map_to_sorted_list R s')" .
qed

lemma map_to_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 10)"
assumes TSL: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)"
shows "(λs. RETURN (tsl s), map_to_sorted_list (λ_ _. True))
∈ ⟨Rk,Rv⟩Rs → ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"
using assms(2-) unfolding is_map_to_list_def
by (rule map_to_sorted_list_by_tsl[OF PRIO_TAGI])

(*lemma dres_it_FOREACH_it_simp[iterator_simps]:
"dres_it_FOREACH (λs. dRETURN (i s)) s c f σ
= foldli (i s) (case_dres False False c) (λx s. s ⤜ f x) (dRETURN σ)"
unfolding dres_it_FOREACH_def
by simp
*)

text ‹
TODO/FIXME:
* Integrate mono-prover properly into solver-infrastructure,
i.e. tag a mono-goal.
* Tag iterators, such that, for the mono-prover, we can just convert
a proper iterator back to its foldli-equivalent!
›
lemma proper_it_mono_dres_pair:
assumes PR: "proper_it' it it'"
assumes A: "⋀k v x. f k v x ≤ f' k v x"
shows "
it' s (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ
≤ it' s (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ" (is "?a ≤ ?b")
proof -
from proper_itE[OF PR[THEN proper_it'D]] obtain l where
A_FMT:
"?a = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ"
(is "_ = ?a'")
and B_FMT:
"?b = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ"
(is "_ = ?b'")
by metis

from A have A': "⋀kv x. case_prod f kv x ≤ case_prod f' kv x"
by auto

note A_FMT
also have
"?a' = foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f kv) σ"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note foldli_mono_dres[OF A']
also have
"foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f' kv) σ = ?b'"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note B_FMT[symmetric]
finally show ?thesis .
qed

lemma proper_it_mono_dres_pair_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀k v x. flat_ge (f k v x) (f' k v x)"
shows "
flat_ge (it' s (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ)
(it' s (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ)"
(is "flat_ge ?a ?b")
proof -
from proper_itE[OF PR[THEN proper_it'D]] obtain l where
A_FMT:
"?a = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ"
(is "_ = ?a'")
and B_FMT:
"?b = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ"
(is "_ = ?b'")
by metis

from A have A': "⋀kv x. flat_ge (case_prod f kv x) (case_prod f' kv x)"
by auto

note A_FMT
also have
"?a' = foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f kv) σ"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note foldli_mono_dres_flat[OF A']
also have
"foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f' kv) σ = ?b'"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note B_FMT[symmetric]
finally show ?thesis .
qed

lemma proper_it_mono_dres:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. f kv x ≤ f' kv x"
shows "
it' s (case_dres False False c) (λkv s. s ⤜ f kv) σ
≤ it' s (case_dres False False c) (λkv s. s ⤜ f' kv) σ"
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
apply (erule_tac t="it' s" in ssubst)
apply (rule foldli_mono_dres[OF A])
done

lemma proper_it_mono_dres_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. flat_ge (f kv x) (f' kv x)"
shows "
flat_ge (it' s (case_dres False False c) (λkv s. s ⤜ f kv) σ)
(it' s (case_dres False False c) (λkv s. s ⤜ f' kv) σ)"
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
apply (erule_tac t="it' s" in ssubst)
apply (rule foldli_mono_dres_flat[OF A])
done

lemma pi'_dom[icf_proper_iteratorI]: "proper_it' it it'
⟹ proper_it' (map_iterator_dom o it) (map_iterator_dom o it')"
apply (rule proper_it'I)
apply (rule icf_proper_iteratorI)
apply (erule proper_it'D)
done

lemma proper_it_mono_dres_dom:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. f kv x ≤ f' kv x"
shows "
(map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f kv) σ
≤
(map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f' kv) σ"

apply (rule proper_it_mono_dres)
apply (rule icf_proper_iteratorI)
by fact+

lemma proper_it_mono_dres_dom_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. flat_ge (f kv x) (f' kv x)"
shows "flat_ge
((map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f kv) σ)
((map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f' kv) σ)"
apply (rule proper_it_mono_dres_flat)
apply (rule icf_proper_iteratorI)
by fact+

(* TODO/FIXME: Hack! Mono-prover should be able to find proper-iterators itself
*)
lemmas proper_it_monos =
proper_it_mono_dres_pair proper_it_mono_dres_pair_flat
proper_it_mono_dres proper_it_mono_dres_flat
proper_it_mono_dres_dom proper_it_mono_dres_dom_flat

(* TODO: Conceptually, this leads to some kind of bundles:
Each bundle has a list of processors, that are invoked for every registered
theorem. *)

attribute_setup "proper_it" = ‹
Scan.succeed (Thm.declaration_attribute (fn thm => fn context =>
let
val mono_thms = map_filter (try (curry (RS) thm)) @{thms proper_it_monos}
(*val mono_thms = map (fn mt => thm RS mt) @{thms proper_it_monos}*)
val context = context
in
context
end
))
›
"Proper iterator declaration"

end


# Theory Idx_Iterator

section ‹\isaheader{Iterator by get and size }›
theory Idx_Iterator
imports
SetIterator
Automatic_Refinement.Automatic_Refinement
begin

fun idx_iteratei_aux
:: "('s ⇒ nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 's ⇒ ('σ⇒bool) ⇒ ('a ⇒'σ ⇒ 'σ) ⇒ 'σ ⇒ 'σ"
where
"idx_iteratei_aux get sz i l c f σ = (
if i=0 ∨ ¬ c σ then σ
else idx_iteratei_aux get sz (i - 1) l c f (f (get l (sz-i)) σ)
)"

declare idx_iteratei_aux.simps[simp del]

lemma idx_iteratei_aux_simps[simp]:
"i=0 ⟹ idx_iteratei_aux get sz i l c f σ = σ"
"¬c σ ⟹ idx_iteratei_aux get sz i l c f σ = σ"
"⟦i≠0; c σ⟧ ⟹ idx_iteratei_aux get sz i l c f σ = idx_iteratei_aux get sz (i - 1) l c f (f (get l (sz-i)) σ)"
apply -
apply (subst idx_iteratei_aux.simps, simp)+
done

definition "idx_iteratei get sz l c f σ == idx_iteratei_aux get (sz l) (sz l) l c f σ"

lemma idx_iteratei_eq_foldli:
assumes sz: "(sz, length) ∈ arel → nat_rel"
assumes get: "(get, (!)) ∈ arel → nat_rel → Id"
assumes "(s,s') ∈ arel"
shows "(idx_iteratei get sz s, foldli s') ∈ Id"
proof-
have size_correct: "⋀s s'. (s,s') ∈ arel ⟹ sz s = length s'"
using sz[param_fo] by simp
have get_correct: "⋀s s' n. (s,s') ∈ arel ⟹ get s n = s' ! n"
using get[param_fo] by simp
{
fix n l
assume A: "Suc n ≤ length l"
hence B: "length l - Suc n < length l" by simp
from A have [simp]: "Suc (length l - Suc n) = length l - n" by simp
from Cons_nth_drop_Suc[OF B, simplified] have
"drop (length l - Suc n) l = l!(length l - Suc n)#drop (length l - n) l"
by simp
} note drop_aux=this

{
fix s s' c f σ i
assume "(s,s') ∈ arel" "i≤sz s"
hence "idx_iteratei_aux get (sz s) i s c f σ = foldli (drop (sz s - i) s') c f σ"
proof (induct i arbitrary: σ)
case 0 with size_correct[of s] show ?case by simp
next
case (Suc n)
note S = Suc.prems(1)
show ?case proof (cases "c σ")
case False thus ?thesis by simp
next
case [simp, intro!]: True
show ?thesis using Suc
by (simp add: size_correct[OF S] get_correct[OF S] drop_aux)
qed
qed
} note aux=this

show ?thesis
unfolding idx_iteratei_def[abs_def]
by (simp, intro ext, simp add: aux[OF ‹(s,s') ∈ arel›])
qed

text ‹Misc.›

lemma idx_iteratei_aux_nth_conv_foldli_drop:
fixes xs :: "'b list"
assumes "i ≤ length xs"
shows "idx_iteratei_aux (!) (length xs) i xs c f σ = foldli (drop (length xs - i) xs) c f σ"
using assms
proof(induct get≡"(!) :: 'b list ⇒ nat ⇒ 'b" sz≡"length xs" i xs c f σ rule: idx_iteratei_aux.induct)
case (1 i l c f σ)
show ?case
proof(cases "i = 0 ∨ ¬ c σ")
case True thus ?thesis
by(subst idx_iteratei_aux.simps)(auto)
next
case False
hence i: "i > 0" and c: "c σ" by auto
hence "idx_iteratei_aux (!) (length l) i l c f σ = idx_iteratei_aux (!) (length l) (i - 1) l c f (f (l ! (length l - i)) σ)"
by(subst idx_iteratei_aux.simps) simp
also have "… = foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ)"
using ‹i ≤ length l› i c by -(rule 1, auto)
also from ‹i ≤ length l› i
have "drop (length l - i) l = (l ! (length l - i)) # drop (length l - (i - 1)) l"
apply (subst Cons_nth_drop_Suc[symmetric])
apply simp_all
done
hence "foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ) = foldli (drop (length l - i) l) c f σ"
using c by simp
finally show ?thesis .
qed
qed

lemma idx_iteratei_nth_length_conv_foldli: "idx_iteratei nth length = foldli"
end


# Theory Iterator

theory Iterator
imports
It_to_It
SetIteratorOperations
SetIteratorGA
Proper_Iterator
Gen_Iterator
Idx_Iterator
begin

text ‹Folding over a list created by a proper iterator can be replaced
by a single iteration›
lemma proper_it_to_list_opt[refine_transfer_post_subst]:
assumes PR: "proper_it' it it'"
shows "foldli o it_to_list it ≡ it'"
proof (rule eq_reflection, intro ext)
fix s c f σ

obtain l where "it s = foldli l" and "it' s = foldli l"
by (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
thus "(foldli o it_to_list it) s c f σ = it' s c f σ"
qed

lemma iterator_cnv_to_comp[refine_transfer_post_simp]:
"foldli (it_to_list it x) = (foldli o it_to_list it) x"
by auto

declare idx_iteratei_eq_foldli[autoref_rules]

end


(*  Title:       Isabelle Collections Library
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
imports
"HOL-Library.RBT_Impl"
"../Iterator/Iterator"
begin

lemma tlt_trans: "⟦l |« u; u≤v⟧ ⟹ l |« v"
by (induct l) auto

lemma trt_trans: "⟦ u≤v; v«|r ⟧ ⟹ u«|r"
by (induct r) auto

lemmas tlt_trans' = tlt_trans[OF _ less_imp_le]
lemmas trt_trans' = trt_trans[OF less_imp_le]

primrec rm_iterateoi
:: "('k,'v) RBT_Impl.rbt ⇒ ('k × 'v, 'σ) set_iterator"
where
"rm_iterateoi RBT_Impl.Empty c f σ = σ" |
"rm_iterateoi (RBT_Impl.Branch col l k v r) c f σ = (
if (c σ) then
let σ' = rm_iterateoi l c f σ in
if (c σ') then
rm_iterateoi r c f (f (k, v) σ')
else σ'
else
σ
)"

lemma rm_iterateoi_abort :
"¬(c σ) ⟹ rm_iterateoi t c f σ = σ"
by (cases t) auto

lemma rm_iterateoi_alt_def :
"rm_iterateoi RBT_Impl.Empty = set_iterator_emp"
"rm_iterateoi (RBT_Impl.Branch col l k v r) =
set_iterator_union (rm_iterateoi l)
(set_iterator_union (set_iterator_sng (k, v)) (rm_iterateoi r))"
by (simp_all add: fun_eq_iff set_iterator_emp_def rm_iterateoi_abort
set_iterator_union_def set_iterator_sng_def Let_def)
declare rm_iterateoi.simps[simp del]

primrec rm_reverse_iterateoi
:: "('k,'v) RBT_Impl.rbt ⇒ ('k × 'v, 'σ) set_iterator"
where
"rm_reverse_iterateoi RBT_Impl.Empty c f σ = σ" |
"rm_reverse_iterateoi (Branch col l k v r) c f σ = (
if (c σ) then
let σ' = rm_reverse_iterateoi r c f σ in
if (c σ') then
rm_reverse_iterateoi l c f (f (k, v) σ')
else σ'
else
σ
)"

lemma rm_reverse_iterateoi_abort :
"¬(c σ) ⟹ rm_reverse_iterateoi t c f σ = σ"
by (cases t) auto

lemma rm_reverse_iterateoi_alt_def :
"rm_reverse_iterateoi RBT_Impl.Empty = set_iterator_emp"
"rm_reverse_iterateoi (RBT_Impl.Branch col l k v r) =
set_iterator_union (rm_reverse_iterateoi r)
(set_iterator_union (set_iterator_sng (k, v)) (rm_reverse_iterateoi l))"
by (simp_all add: fun_eq_iff set_iterator_emp_def rm_reverse_iterateoi_abort
set_iterator_union_def set_iterator_sng_def Let_def)
declare rm_reverse_iterateoi.simps[simp del]

(*
lemma finite_dom_lookup [simp, intro!]: "finite (dom (RBT.lookup t))"

instantiation rbt :: ("{equal, linorder}", equal) equal begin

definition "equal_class.equal (r :: ('a, 'b) rbt) r' == RBT.impl_of r = RBT.impl_of r'"

instance
proof

end
*)

lemma (in linorder) map_to_set_lookup_entries:
"rbt_sorted t ⟹ map_to_set (rbt_lookup t) = set (RBT_Impl.entries t)"
using map_of_entries[symmetric,of t]

lemma (in linorder) rm_iterateoi_correct:
fixes t::"('a, 'v) RBT_Impl.rbt"
assumes is_sort: "rbt_sorted t"
defines "it ≡
RBT_add.rm_iterateoi::(('a, 'v) RBT_Impl.rbt ⇒ ('a × 'v, 'σ) set_iterator)"
shows "map_iterator_linord (it t) (rbt_lookup t)"
using is_sort
proof (induct t)
case Empty
show ?case unfolding it_def
map_iterator_linord_emp_correct rbt_lookup_Empty)
next
case (Branch c l k v r)
note is_sort_t = Branch(3)

from Branch(1) is_sort_t have
l_it: "map_iterator_linord (it l) (rbt_lookup l)" by simp
from Branch(2) is_sort_t have
r_it: "map_iterator_linord (it r) (rbt_lookup r)" by simp
note kv_it = map_iterator_linord_sng_correct[of k v]

have kv_r_it : "set_iterator_map_linord
(set_iterator_union (set_iterator_sng (k, v)) (it r))
(map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup r))"
proof (rule map_iterator_linord_union_correct [OF kv_it r_it])
fix kv kv'
assume pre: "kv ∈ map_to_set [k ↦ v]" "kv' ∈ map_to_set (rbt_lookup r)"
obtain k' v' where kv'_eq[simp]: "kv' = (k', v')" by (rule prod.exhaust)

from pre is_sort_t show "fst kv < fst kv'"
apply (simp add: map_to_set_lookup_entries split: prod.splits)
apply (metis entry_in_tree_keys rbt_greater_prop)
done
qed

have l_kv_r_it : "set_iterator_map_linord (it (Branch c l k v r))
(map_to_set (rbt_lookup l)
∪ (map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup r)))"
unfolding it_def rm_iterateoi_alt_def
unfolding it_def[symmetric]
proof (rule map_iterator_linord_union_correct [OF l_it kv_r_it])
fix kv1 kv2
assume pre: "kv1 ∈ map_to_set (rbt_lookup l)"
"kv2 ∈ map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup r)"

obtain k1 v1 where kv1_eq[simp]: "kv1 = (k1, v1)" by (rule prod.exhaust)
obtain k2 v2 where kv2_eq[simp]: "kv2 = (k2, v2)" by (rule prod.exhaust)

from pre is_sort_t show "fst kv1 < fst kv2"
apply (simp add: map_to_set_lookup_entries split: prod.splits)
by (metis (lifting) map_of_entries neqE option.simps(3)
ord.rbt_lookup_rbt_greater ord.rbt_lookup_rbt_less rbt_greater_trans
rbt_less_trans weak_map_of_SomeI)
qed

from is_sort_t
have map_eq: "map_to_set (rbt_lookup l)
∪ (map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup r)) =
map_to_set (rbt_lookup (Branch c l k v r))"

from l_kv_r_it[unfolded map_eq]
show ?case .
qed

lemma (in linorder) rm_reverse_iterateoi_correct:
fixes t::"('a, 'v) RBT_Impl.rbt"
assumes is_sort: "rbt_sorted t"
::(('a, 'v) RBT_Impl.rbt ⇒ ('a × 'v, 'σ) set_iterator)"
shows "map_iterator_rev_linord (it t) (rbt_lookup t)"
using is_sort
proof (induct t)
case Empty
show ?case unfolding it_def
map_iterator_rev_linord_emp_correct rbt_lookup_Empty)
next
case (Branch c l k v r)
note is_sort_t = Branch(3)

from Branch(1) is_sort_t have
l_it: "map_iterator_rev_linord (it l) (rbt_lookup l)" by simp
from Branch(2) is_sort_t have
r_it: "map_iterator_rev_linord (it r) (rbt_lookup r)" by simp
note kv_it = map_iterator_rev_linord_sng_correct[of k v]

have kv_l_it : "set_iterator_map_rev_linord
(set_iterator_union (set_iterator_sng (k, v)) (it l))
(map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup l))"
proof (rule map_iterator_rev_linord_union_correct [OF kv_it l_it])
fix kv kv'
assume pre: "kv ∈ map_to_set [k ↦ v]" "kv' ∈ map_to_set (rbt_lookup l)"
obtain k' v' where kv'_eq[simp]: "kv' = (k', v')" by (rule prod.exhaust)

from pre is_sort_t show "fst kv > fst kv'"
apply (simp add: map_to_set_lookup_entries split: prod.splits)
apply (metis entry_in_tree_keys rbt_less_prop)
done
qed

have r_kv_l_it : "set_iterator_map_rev_linord (it (Branch c l k v r))
(map_to_set (rbt_lookup r)
∪ (map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup l)))"
unfolding it_def rm_reverse_iterateoi_alt_def
unfolding it_def[symmetric]
proof (rule map_iterator_rev_linord_union_correct [OF r_it kv_l_it])
fix kv1 kv2
assume pre: "kv1 ∈ map_to_set (rbt_lookup r)"
"kv2 ∈ map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup l)"

obtain k1 v1 where kv1_eq[simp]: "kv1 = (k1, v1)" by (rule prod.exhaust)
obtain k2 v2 where kv2_eq[simp]: "kv2 = (k2, v2)" by (rule prod.exhaust)

from pre is_sort_t show "fst kv1 > fst kv2"
apply (simp add: map_to_set_lookup_entries split: prod.splits)
by (metis (mono_tags) entry_in_tree_keys neq_iff option.simps(3)
ord.rbt_greater_prop ord.rbt_lookup_rbt_less rbt_less_trans
rbt_lookup_in_tree)
qed

from is_sort_t
have map_eq: "map_to_set (rbt_lookup r)
∪ (map_to_set [k ↦ v] ∪ map_to_set (rbt_lookup l)) =
map_to_set (rbt_lookup (Branch c l k v r))"
by (auto simp add: set_eq_iff map_to_set_lookup_entries)

from r_kv_l_it[unfolded map_eq]
show ?case .
qed

lemma pi_rm[icf_proper_iteratorI]:
by (induct t) (simp_all add: rm_iterateoi_alt_def icf_proper_iteratorI)

lemma pi_rm_rev[icf_proper_iteratorI]:
by (induct t) (simp_all add: rm_reverse_iterateoi_alt_def
icf_proper_iteratorI)

primrec bheight_aux :: "('a,'b) RBT_Impl.rbt ⇒ nat ⇒ nat"
where
"⋀acc. bheight_aux RBT_Impl.Empty acc = acc"
| "⋀acc. bheight_aux (RBT_Impl.Branch c lt k v rt) acc =
bheight_aux lt (case c of RBT_Impl.B ⇒ Suc acc | RBT_Impl.R ⇒ acc)"

lemma bheight_aux_eq: "bheight_aux t a = bheight t + a"
by (induct t arbitrary: a) (auto split: RBT_Impl.color.split)

definition [code_unfold]: "rbt_bheight t ≡ bheight_aux t 0"
lemma "rbt_bheight t = bheight t"
unfolding rbt_bheight_def by (simp add: bheight_aux_eq)

(*definition "black_height t ≡ rbt_bheight (RBT.impl_of t)"*)

end


section ‹\isaheader{Additions to Distinct Lists}›
imports
"HOL-Library.Dlist"
Automatic_Refinement.Misc
"../Iterator/SetIteratorOperations"
begin

primrec dlist_remove1' :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list"
where
"dlist_remove1' x z [] = z"
| "dlist_remove1' x z (y # ys)
= (if x = y then z @ ys else dlist_remove1' x (y # z) ys)"

definition dlist_remove' :: "'a ⇒ 'a dlist ⇒ 'a dlist"
where "dlist_remove' a xs = Dlist (dlist_remove1' a [] (list_of_dlist xs))"

lemma distinct_remove1': "distinct (xs @ ys) ⟹
distinct (dlist_remove1' x xs ys)"
by(induct ys arbitrary: xs) simp_all

lemma set_dlist_remove1': "distinct ys ⟹
set (dlist_remove1' x xs ys) = set xs ∪ (set ys - {x})"
by(induct ys arbitrary: xs) auto

lemma list_of_dlist_remove' [simp, code abstract]:
"list_of_dlist (dlist_remove' a xs) = dlist_remove1' a [] (list_of_dlist xs)"

lemma dlist_remove'_correct:
"y ∈ set (list_of_dlist (dlist_remove' x xs))
⟷ (if x = y then False else y ∈ set (list_of_dlist xs))"
set_