# Theory Impl_Array_Map

```section ‹\isaheader{Array-Based Maps with Natural Number Keys}›
theory Impl_Array_Map
imports
Automatic_Refinement.Automatic_Refinement
"../../Lib/Diff_Array"
"../../Iterator/Iterator"
"../Gen/Gen_Map"
"../Intf/Intf_Comp"
"../Intf/Intf_Map"
begin

type_synonym 'v iam = "'v option array"

subsection ‹Definitions›

definition iam_α :: "'v iam ⇒ nat ⇀ 'v" where
"iam_α a i ≡ if i < array_length a then array_get a i else None"

lemma [code]: "iam_α a i ≡ array_get_oo None a i"
unfolding array_get_oo_def iam_α_def .

abbreviation iam_invar :: "'v iam ⇒ bool" where "iam_invar ≡ λ_. True"

definition iam_empty :: "unit ⇒ 'v iam"
where "iam_empty ≡ λ_::unit. array_of_list []"

definition iam_lookup :: "nat ⇒ 'v iam ⇀ 'v"
where [code_unfold]: "iam_lookup k a ≡ iam_α a k"

definition "iam_increment (l::nat) idx ≡
max (idx + 1 - l) (2 * l + 3)"

lemma incr_correct: "¬ idx < l ⟹ idx < l + iam_increment l idx"
unfolding iam_increment_def by auto

definition iam_update :: "nat ⇒ 'v ⇒ 'v iam ⇒ 'v iam"
where "iam_update k v a ≡ let
l = array_length a;
a = if k < l then a else array_grow a (iam_increment l k) None
in
array_set a k (Some v)"

lemma [code]: "iam_update k v a ≡ array_set_oo
(λ_. let l=array_length a in
array_set (array_grow a (iam_increment l k) None) k (Some v))
a k (Some v)"
unfolding iam_update_def array_set_oo_def
apply (rule eq_reflection)
by auto

definition iam_delete :: "nat ⇒ 'v iam ⇒ 'v iam"
where "iam_delete k a ≡
if k<array_length a then array_set a k None else a"

lemma [code]: "iam_delete k a ≡ array_set_oo (λ_. a) a k None"
unfolding iam_delete_def array_set_oo_def by auto

primrec iam_iteratei_aux
:: "nat ⇒ ('v iam) ⇒ ('σ⇒bool) ⇒ (nat × 'v⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"
where
"iam_iteratei_aux 0 a c f σ = σ"
| "iam_iteratei_aux (Suc i) a c f σ = (
if c σ then
iam_iteratei_aux i a c f (
case array_get a i of None ⇒ σ | Some x ⇒ f (i, x) σ
)
else σ)"

definition iam_iteratei :: "'v iam ⇒ (nat × 'v,'σ) set_iterator" where
"iam_iteratei a = iam_iteratei_aux (array_length a) a"

subsection ‹Parametricity›

definition iam_rel_def_internal:
"iam_rel R ≡ ⟨⟨R⟩ option_rel⟩ array_rel"
lemma iam_rel_def: "⟨R⟩ iam_rel = ⟨⟨R⟩ option_rel⟩ array_rel"

lemma iam_rel_sv[relator_props]:
"single_valued Rv ⟹ single_valued (⟨Rv⟩iam_rel)"
unfolding iam_rel_def
by tagged_solver

lemma param_iam_α[param]:
"(iam_α, iam_α) ∈ ⟨R⟩ iam_rel → nat_rel → ⟨R⟩ option_rel"
unfolding iam_α_def[abs_def] iam_rel_def by parametricity

lemma param_iam_invar[param]:
"(iam_invar, iam_invar) ∈ ⟨R⟩ iam_rel → bool_rel"
unfolding iam_rel_def by parametricity

lemma param_iam_empty[param]:
"(iam_empty, iam_empty) ∈ unit_rel → ⟨R⟩iam_rel"
unfolding iam_empty_def[abs_def] iam_rel_def by parametricity

lemma param_iam_lookup[param]:
"(iam_lookup, iam_lookup) ∈ nat_rel → ⟨R⟩iam_rel → ⟨R⟩option_rel"
unfolding iam_lookup_def[abs_def]
by parametricity

(* TODO: why does parametricity fail here? *)
lemma param_iam_increment[param]:
"(iam_increment, iam_increment) ∈ nat_rel → nat_rel → nat_rel"
unfolding iam_increment_def[abs_def]
by simp

(* TODO: The builtin "Let" rule for parametricity does some unpleasant things
here, leading to an unprovable subgoal. Investigate this. *)
lemma param_iam_update[param]:
"(iam_update, iam_update) ∈ nat_rel → R → ⟨R⟩iam_rel → ⟨R⟩iam_rel"
unfolding iam_update_def[abs_def] iam_rel_def Let_def
apply parametricity
done

lemma param_iam_delete[param]:
"(iam_delete, iam_delete) ∈ nat_rel → ⟨R⟩iam_rel → ⟨R⟩iam_rel"
unfolding iam_delete_def[abs_def] iam_rel_def by parametricity

lemma param_iam_iteratei_aux[param]:
assumes I: "i ≤ array_length a"
assumes IR: "(i,i') ∈ nat_rel"
assumes AR: "(a,a') ∈ ⟨Ra⟩iam_rel"
assumes CR: "(c,c') ∈ Rb → bool_rel"
assumes FR: "(f,f') ∈ ⟨nat_rel,Ra⟩prod_rel → Rb → Rb"
assumes σR: "(σ,σ') ∈ Rb"
shows "(iam_iteratei_aux i a c f σ, iam_iteratei_aux i' a' c' f' σ') ∈ Rb"
using assms
unfolding iam_rel_def
apply (induct i' arbitrary: i σ σ')
apply (simp_all only: pair_in_Id_conv iam_iteratei_aux.simps)
apply parametricity
apply simp_all
done

lemma param_iam_iteratei[param]:
"(iam_iteratei,iam_iteratei) ∈ ⟨Ra⟩iam_rel → (Rb → bool_rel) →
(⟨nat_rel,Ra⟩prod_rel → Rb → Rb) → Rb → Rb"
unfolding iam_iteratei_def[abs_def]

subsection ‹Correctness›

definition "iam_rel' ≡ br iam_α iam_invar"

lemma iam_empty_correct:
"(iam_empty (), Map.empty) ∈  iam_rel'"
by (simp add: iam_rel'_def br_def iam_α_def[abs_def] iam_empty_def)

lemma iam_update_correct:
"(iam_update,op_map_update) ∈ nat_rel → Id → iam_rel'  → iam_rel'"
by (auto simp: iam_rel'_def br_def Let_def array_get_array_set_other
incr_correct iam_α_def[abs_def] iam_update_def)

lemma iam_lookup_correct:
"(iam_lookup,op_map_lookup) ∈ Id → iam_rel' → ⟨Id⟩option_rel"
by (auto simp: iam_rel'_def br_def iam_lookup_def[abs_def])

lemma array_get_set_iff: "i<array_length a ⟹
array_get (array_set a i x) j = (if i=j then x else array_get a j)"
by (auto simp: array_get_array_set_other)

lemma iam_delete_correct:
"(iam_delete,op_map_delete) ∈ Id → iam_rel' → iam_rel'"
unfolding iam_α_def[abs_def] iam_delete_def[abs_def] iam_rel'_def br_def
by (auto simp: Let_def array_get_set_iff)

definition iam_map_rel_def_internal:
"iam_map_rel Rk Rv ≡
if Rk=nat_rel then ⟨Rv⟩iam_rel O iam_rel' else {}"
lemma iam_map_rel_def:
"⟨nat_rel,Rv⟩iam_map_rel ≡ ⟨Rv⟩iam_rel O iam_rel'"
unfolding iam_map_rel_def_internal relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of "iam_map_rel" i_map]

lemma iam_map_rel_sv[relator_props]:
"single_valued Rv ⟹ single_valued (⟨nat_rel,Rv⟩iam_map_rel)"
unfolding iam_map_rel_def iam_rel'_def by tagged_solver

lemma iam_empty_impl:
"(iam_empty (), op_map_empty) ∈ ⟨nat_rel,R⟩iam_map_rel"
unfolding iam_map_rel_def op_map_empty_def
apply (intro relcompI)
apply (rule param_iam_empty[THEN fun_relD], simp)
apply (rule iam_empty_correct)
done

lemma iam_lookup_impl:
"(iam_lookup, op_map_lookup)
∈ nat_rel → ⟨nat_rel,R⟩iam_map_rel → ⟨R⟩option_rel"
unfolding iam_map_rel_def
apply (intro fun_relI)
apply (elim relcompE)
apply (frule iam_lookup_correct[param_fo], assumption)
apply (frule param_iam_lookup[param_fo], assumption)
apply simp
done

lemma iam_update_impl:
"(iam_update, op_map_update) ∈
nat_rel → R → ⟨nat_rel,R⟩iam_map_rel → ⟨nat_rel,R⟩iam_map_rel"
unfolding iam_map_rel_def
apply (intro fun_relI, elim relcompEpair, intro relcompI)
apply (erule (2) param_iam_update[param_fo])
apply (rule iam_update_correct[param_fo])
apply simp_all
done

lemma iam_delete_impl:
"(iam_delete, op_map_delete) ∈
nat_rel → ⟨nat_rel,R⟩iam_map_rel → ⟨nat_rel,R⟩iam_map_rel"
unfolding iam_map_rel_def
apply (intro fun_relI, elim relcompEpair, intro relcompI)
apply (erule (1) param_iam_delete[param_fo])
apply (rule iam_delete_correct[param_fo])
by simp_all

lemmas iam_map_impl =
iam_empty_impl
iam_lookup_impl
iam_update_impl
iam_delete_impl

declare iam_map_impl[autoref_rules]

subsection ‹Iterator proofs›

abbreviation "iam_to_list a ≡ it_to_list iam_iteratei a"

lemma distinct_iam_to_list_aux:
shows "⟦distinct xs; ∀(i,_)∈set xs. i ≥ n⟧ ⟹
distinct (iam_iteratei_aux n a
(λ_.True) (λx y. y @ [x]) xs)"
(is "⟦_;_⟧ ⟹ distinct (?iam_to_list_aux n xs)")
proof (induction n arbitrary: xs)
case (0 xs) thus ?case by simp
next
case (Suc i xs)
show ?case
proof (cases "array_get a i")
case None
with Suc.IH[OF Suc.prems(1)] Suc.prems(2)
show ?thesis by force
next
case (Some x)
let ?xs' = "xs @ [(i,x)]"
from Suc.prems have "distinct ?xs'" and
"∀(i',x)∈set ?xs'. i' ≥ i" by force+
from Some and Suc.IH[OF this] show ?thesis by simp
qed
qed

lemma distinct_iam_to_list:
"distinct (iam_to_list a)"
unfolding it_to_list_def iam_iteratei_def
by (force intro: distinct_iam_to_list_aux)

lemma iam_to_list_set_correct_aux:
assumes "(a, m) ∈ iam_rel'"
shows "⟦n ≤ array_length a; map_to_set m - {(k,v). k < n} = set xs⟧
⟹ map_to_set m =
set (iam_iteratei_aux n a (λ_.True) (λx y. y @ [x]) xs)"
proof (induction n arbitrary: xs)
case (0 xs)
thus ?case by simp
next
case (Suc n xs)
with assms have [simp]: "array_get a n = m n"
unfolding iam_rel'_def br_def iam_α_def[abs_def] by simp
show ?case
proof (cases "m n")
case None
with Suc.prems(2) have "map_to_set m - {(k,v). k < n} = set xs"
unfolding map_to_set_def by (fastforce simp: less_Suc_eq)
from None and Suc.IH[OF _ this] and Suc.prems(1)
show ?thesis by simp
next
case (Some x)
let ?xs' = "xs @ [(n,x)]"
from Some and Suc.prems(2)
have "map_to_set m - {(k,v). k < n} = set ?xs'"
unfolding map_to_set_def by (fastforce simp: less_Suc_eq)
from Some and Suc.IH[OF _ this] and Suc.prems(1)
show ?thesis by simp
qed
qed

lemma iam_to_list_set_correct:
assumes "(a, m) ∈ iam_rel'"
shows "map_to_set m = set (iam_to_list a)"
proof-
from assms
have A: "map_to_set m - {(k, v). k < array_length a} = set []"
unfolding map_to_set_def iam_rel'_def br_def iam_α_def[abs_def]
by (force split: if_split_asm)
with iam_to_list_set_correct_aux[OF assms _ A] show ?thesis
unfolding it_to_list_def iam_iteratei_def by simp
qed

lemma iam_iteratei_aux_append:
"n ≤ length xs ⟹ iam_iteratei_aux n (Array (xs @ ys)) =
iam_iteratei_aux n (Array xs)"
apply (induction n)
apply force
apply (intro ext, auto split: option.split simp: nth_append)
done

lemma iam_iteratei_append:
"iam_iteratei (Array (xs @ [None])) c f σ =
iam_iteratei (Array xs) c f σ"
"iam_iteratei (Array (xs @ [Some x])) c f σ =
iam_iteratei (Array xs) c f
(if c σ then (f (length xs, x) σ) else σ)"
unfolding  iam_iteratei_def
apply (cases "length xs")
apply (force simp: nth_append iam_iteratei_aux_append) []
apply (cases "length xs")
apply (force split: option.split
simp: nth_append iam_iteratei_aux_append) []
done

lemma iam_iteratei_aux_Cons:
"n < array_length a ⟹
iam_iteratei_aux n a (λ_. True) (λx l. l @ [x]) (x#xs) =
x # iam_iteratei_aux n a (λ_. True) (λx l. l @ [x]) xs"
by (induction n arbitrary: xs, auto split: option.split)

lemma iam_to_list_append:
"iam_to_list (Array (xs @ [None])) = iam_to_list (Array xs)"
"iam_to_list (Array (xs @ [Some x])) =
(length xs, x) # iam_to_list (Array xs)"
unfolding  it_to_list_def iam_iteratei_def
done

lemma autoref_iam_is_iterator[autoref_ga_rules]:
shows "is_map_to_list nat_rel Rv iam_map_rel iam_to_list"
unfolding is_map_to_list_def is_map_to_sorted_list_def
proof (clarify)
fix a m'
assume "(a,m') ∈ ⟨nat_rel,Rv⟩iam_map_rel"
then obtain a' where [param]: "(a,a')∈⟨Rv⟩iam_rel"
and "(a',m')∈iam_rel'" unfolding iam_map_rel_def by blast

have "(iam_to_list a, iam_to_list a')
∈ ⟨⟨nat_rel, Rv⟩prod_rel⟩list_rel" by parametricity

moreover from distinct_iam_to_list and
iam_to_list_set_correct[OF ‹(a',m')∈iam_rel'›]
have "RETURN (iam_to_list a') ≤ it_to_sorted_list
(key_rel (λ_ _. True)) (map_to_set m')"
unfolding it_to_sorted_list_def key_rel_def[abs_def]
by (force intro: refine_vcg)

ultimately show "∃l'. (iam_to_list a, l') ∈
⟨⟨nat_rel, Rv⟩prod_rel⟩list_rel
∧ RETURN l' ≤ it_to_sorted_list (
key_rel (λ_ _. True)) (map_to_set m')" by blast
qed

(* We provide a ,,sorted'' iterator to simplify derivations of the
generic algorithm library *)
lemmas [autoref_ga_rules] =
autoref_iam_is_iterator[unfolded is_map_to_list_def]

lemma iam_iteratei_altdef:
"iam_iteratei a = foldli (iam_to_list a)"
(is "?f a = ?g (iam_to_list a)")
proof-
obtain l where "a = Array l" by (cases a)
have "?f (Array l) = ?g (iam_to_list (Array l))"
proof (induction "length l" arbitrary: l)
case (0 l)
thus ?case by (intro ext,
next
case (Suc n l)
hence "l ≠ []" and [simp]: "length l = Suc n" by force+
with append_butlast_last_id have [simp]:
"butlast l @ [last l] = l" by simp
with Suc have [simp]: "length (butlast l) = n" by simp
note IH = Suc(1)[OF this[symmetric]]
let ?l' = "iam_to_list (Array l)"

show ?case
proof (cases "last l")
case None
have "?f (Array l) =
?f (Array (butlast l @ [last l]))" by simp
also have "... = ?g (iam_to_list (Array (butlast l)))"
by (force simp: None iam_iteratei_append IH)
also have "iam_to_list (Array (butlast l)) =
iam_to_list (Array (butlast l @ [last l]))"
using None by (simp add: iam_to_list_append)
finally show "?f (Array l) = ?g ?l'" by simp
next
case (Some x)
have "?f (Array l) =
?f (Array (butlast l @ [last l]))" by simp
also have "... = ?g (iam_to_list
(Array (butlast l @ [last l])))"
by (force simp: IH iam_iteratei_append
iam_to_list_append Some)
finally show ?thesis by simp
qed
qed
thus ?thesis by (simp add: ‹a = Array l›)
qed

lemma pi_iam[icf_proper_iteratorI]:
"proper_it (iam_iteratei a) (iam_iteratei a)"
unfolding proper_it_def by (force simp: iam_iteratei_altdef)

lemma pi'_iam[icf_proper_iteratorI]:
"proper_it' iam_iteratei iam_iteratei"
by (rule proper_it'I, rule pi_iam)

end
```