# Theory Impl_List_Map

```section ‹\isaheader{List Based Maps}›
theory Impl_List_Map
imports
"../../Iterator/Iterator"
"../Gen/Gen_Map"
"../Intf/Intf_Comp"
"../Intf/Intf_Map"
begin

type_synonym ('k,'v) list_map = "('k×'v) list"

definition "list_map_invar = distinct o map fst"

definition list_map_rel_internal_def:
"list_map_rel Rk Rv ≡ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel O br map_of list_map_invar"

lemma list_map_rel_def:
"⟨Rk,Rv⟩list_map_rel = ⟨⟨Rk,Rv⟩prod_rel⟩list_rel O br map_of list_map_invar"
unfolding list_map_rel_internal_def[abs_def] by (simp add: relAPP_def)

lemma list_rel_Range:
"∀x'∈set l'. x' ∈ Range R ⟹ l' ∈ Range (⟨R⟩list_rel)"
proof (induction l')
case Nil thus ?case by force
next
case (Cons x' xs')
then obtain xs where "(xs,xs') ∈ ⟨R⟩ list_rel" by force
moreover from Cons.prems obtain x where "(x,x') ∈ R" by force
ultimately have "(x#xs, x'#xs') ∈ ⟨R⟩ list_rel" by simp
thus ?case ..
qed

text ‹All finite maps can be represented›
lemma list_map_rel_range:
"Range (⟨Rk,Rv⟩list_map_rel) =
{m. finite (dom m) ∧ dom m ⊆ Range Rk ∧ ran m ⊆ Range Rv}"
(is "?A = ?B")
proof (intro equalityI subsetI)
fix m' assume "m' ∈ ?A"
then obtain l l' where A: "(l,l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel" and
B: "m' = map_of l'" and C: "list_map_invar l'"
unfolding list_map_rel_def br_def by blast
{
fix x' y' assume "m' x' = Some y'"
with B have "(x',y') ∈ set l'" by (fast dest: map_of_SomeD)
hence "x' ∈ Range Rk" and "y' ∈ Range Rv"
by (induction rule: list_rel_induct[OF A], auto)
}
with B show "m' ∈ ?B" by (force dest: map_of_SomeD simp: ran_def)

next
fix m' assume "m' ∈ ?B"
hence A: "finite (dom m')" and B: "dom m' ⊆ Range Rk" and
C: "ran m' ⊆ Range Rv" by simp_all
from A have "finite (map_to_set m')" by (simp add: finite_map_to_set)
from finite_distinct_list[OF this]
obtain l' where l'_props: "distinct l'" "set l' = map_to_set m'" by blast
hence *: "distinct (map fst l')"
by (force simp: distinct_map inj_on_def map_to_set_def)
from map_of_map_to_set[OF this] and l'_props
have  "map_of l' = m'" by simp
with * have "(l',m') ∈ br map_of list_map_invar"
unfolding br_def list_map_invar_def o_def by simp

moreover from B and C and l'_props
have "∀x ∈ set l'. x ∈ Range (⟨Rk,Rv⟩prod_rel)"
unfolding map_to_set_def ran_def prod_rel_def by force
from list_rel_Range[OF this] obtain l where
"(l,l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel" by force

ultimately show "m' ∈ ?A" unfolding list_map_rel_def by blast
qed

lemmas [autoref_rel_intf] = REL_INTFI[of list_map_rel i_map]

lemma list_map_rel_finite[autoref_ga_rules]:
"finite_map_rel (⟨Rk,Rv⟩list_map_rel)"
unfolding finite_map_rel_def list_map_rel_def
by (auto simp: br_def)

lemma list_map_rel_sv[relator_props]:
"single_valued Rk ⟹ single_valued Rv ⟹
single_valued (⟨Rk,Rv⟩list_map_rel)"
unfolding list_map_rel_def
by tagged_solver

(* TODO: Move to Misc *)

subsection ‹Implementation›

primrec list_map_lookup ::
"('k ⇒ 'k ⇒ bool) ⇒ 'k ⇒ ('k,'v) list_map ⇒ 'v option" where
"list_map_lookup eq _ [] = None" |
"list_map_lookup eq k (y#ys) =
(if eq (fst y) k then Some (snd y) else list_map_lookup eq k ys)"

primrec list_map_update_aux :: "('k ⇒ 'k ⇒ bool) ⇒ 'k ⇒ 'v ⇒
('k,'v) list_map ⇒ ('k,'v) list_map ⇒ ('k,'v) list_map"where
"list_map_update_aux eq k v [] accu = (k,v) # accu" |
"list_map_update_aux eq k v (x#xs) accu =
(if eq (fst x) k
then (k,v) # xs @ accu
else list_map_update_aux eq k v xs (x#accu))"

definition "list_map_update eq k v m ≡
list_map_update_aux eq k v m []"

primrec list_map_delete_aux :: "('k ⇒ 'k ⇒ bool) ⇒ 'k ⇒
('k, 'v) list_map ⇒ ('k, 'v) list_map ⇒ ('k, 'v) list_map" where
"list_map_delete_aux eq k [] accu = accu" |
"list_map_delete_aux eq k (x#xs) accu =
(if eq (fst x) k
then xs @ accu
else list_map_delete_aux eq k xs (x#accu))"

definition "list_map_delete eq k m ≡ list_map_delete_aux eq k m []"

definition list_map_isEmpty :: "('k,'v) list_map ⇒ bool"
where "list_map_isEmpty ≡ List.null"

definition list_map_isSng :: "('k,'v) list_map ⇒ bool"
where "list_map_isSng m = (case m of [x] ⇒ True | _ ⇒ False)"

definition list_map_size :: "('k,'v) list_map ⇒ nat"
where "list_map_size ≡ length"

definition list_map_iteratei :: "('k,'v) list_map ⇒ ('b ⇒ bool) ⇒
(('k×'v) ⇒ 'b ⇒ 'b) ⇒ 'b ⇒ 'b"
where "list_map_iteratei ≡ foldli"

definition list_map_to_list :: "('k,'v) list_map ⇒ ('k×'v) list"
where "list_map_to_list = id"

subsection ‹Parametricity›

lemma list_map_autoref_empty[autoref_rules]:
"([], op_map_empty)∈⟨Rk,Rv⟩list_map_rel"
by (auto simp: list_map_rel_def br_def list_map_invar_def)

lemma param_list_map_lookup[param]:
"(list_map_lookup,list_map_lookup) ∈ (Rk → Rk → bool_rel) →
Rk → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨Rv⟩option_rel"
unfolding list_map_lookup_def[abs_def] by parametricity

lemma list_map_autoref_lookup_aux:
assumes eq: "GEN_OP eq (=) (Rk→Rk→Id)"
assumes K: "(k, k') ∈ Rk"
assumes M: "(m, m') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
shows "(list_map_lookup eq k m, op_map_lookup k' (map_of m'))
∈ ⟨Rv⟩option_rel"
unfolding op_map_lookup_def
proof (induction rule: list_rel_induct[OF M, case_names Nil Cons])
case Nil
show ?case by simp
next
case (Cons x x' xs xs')
from eq have eq': "(eq,(=)) ∈ Rk → Rk → Id" by simp
with eq'[param_fo] and K  and Cons
show ?case by (force simp: prod_rel_def)
qed

lemma list_map_autoref_lookup[autoref_rules]:
assumes "GEN_OP eq (=) (Rk→Rk→Id)"
shows "(list_map_lookup eq, op_map_lookup) ∈
Rk → ⟨Rk,Rv⟩list_map_rel → ⟨Rv⟩option_rel"
by (force simp: list_map_rel_def br_def
dest: list_map_autoref_lookup_aux[OF assms])

lemma param_list_map_update_aux[param]:
"(list_map_update_aux,list_map_update_aux) ∈ (Rk → Rk → bool_rel) →
Rk → Rv → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel
→ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
unfolding list_map_update_aux_def[abs_def] by parametricity

lemma param_list_map_update[param]:
"(list_map_update,list_map_update) ∈ (Rk → Rk → bool_rel) →
Rk → Rv → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
unfolding list_map_update_def[abs_def] by parametricity

lemma list_map_autoref_update_aux1:
assumes eq: "(eq,(=)) ∈ Rk → Rk → Id"
assumes K: "(k, k') ∈ Rk"
assumes V: "(v, v') ∈ Rv"
assumes A: "(accu, accu') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
assumes M: "(m, m') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
shows "(list_map_update_aux eq k v m accu,
list_map_update_aux (=) k' v' m' accu')
∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
proof (insert A, induction arbitrary: accu accu'
rule: list_rel_induct[OF M, case_names Nil Cons])
case Nil
thus ?case by (simp add: K V)
next
case (Cons x x' xs xs')
from eq have eq': "(eq,(=)) ∈ Rk → Rk → Id" by simp
from eq'[param_fo] Cons(1) K
have [simp]: "(eq (fst x) k) ⟷ ((fst x') = k')"
by (force simp: prod_rel_def)
show ?case
proof (cases "eq (fst x) k")
case False
from Cons.prems and Cons.hyps have "(x # accu, x' # accu') ∈
⟨⟨Rk, Rv⟩prod_rel⟩list_rel" by parametricity
from Cons.IH[OF this] and False show ?thesis by simp
next
case True
from Cons.prems and Cons.hyps have "(xs @ accu, xs' @ accu') ∈
⟨⟨Rk, Rv⟩prod_rel⟩list_rel" by parametricity
with K and V and True show ?thesis by simp
qed
qed

lemma list_map_autoref_update1[param]:
assumes eq: "(eq,(=)) ∈ Rk → Rk → Id"
shows "(list_map_update eq, list_map_update (=)) ∈ Rk → Rv →
⟨⟨Rk, Rv⟩prod_rel⟩list_rel → ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
unfolding list_map_update_def[abs_def]
by (intro fun_relI, erule (1) list_map_autoref_update_aux1[OF eq],
simp_all)

(* TODO: Move - Perhaps. *)
lemma map_add_sng_right: "m ++ [k↦v] = m(k ↦ v)"
"m ++ (λa. if a = k then Some v else None) = m(k ↦ v)"

lemma list_map_autoref_update_aux2:
assumes K: "(k, k') ∈ Id"
assumes V: "(v, v') ∈ Id"
assumes A: "(accu, accu') ∈ br map_of list_map_invar"
assumes A1: "distinct (map fst (m @ accu))"
assumes A2: "k ∉ set (map fst accu)"
assumes M: "(m, m') ∈ br map_of list_map_invar"
shows "(list_map_update_aux (=) k v m accu,
accu' ++ op_map_update k' v' m')
∈ br map_of list_map_invar" (is "(?f m accu, _) ∈ _")
using M A A1 A2
proof (induction m arbitrary: accu accu' m')
case Nil
with K V show ?case by (auto simp: br_def list_map_invar_def
next
case (Cons x xs accu accu' m')
from Cons.prems have A: "m' = map_of (x#xs)" "accu' = map_of accu"
unfolding br_def by simp_all
show ?case
proof (cases "(fst x) =  k")
case True
hence "((k, v) # xs @ accu, accu' ++ op_map_update k' v' m')
∈ br map_of list_map_invar"
using K V Cons.prems(3,4) unfolding br_def
by (force simp add: A list_map_invar_def)
also from True have "(k,v) # xs @ accu = ?f (x # xs) accu" by simp
finally show ?thesis .
next
case False
from Cons.prems(1) have B: "(xs, map_of xs) ∈ br map_of
from Cons.prems(2,3) have C: "(x#accu, map_of (x#accu)) ∈ br map_of
list_map_invar" by (simp add: br_def list_map_invar_def)
from Cons.prems(3) have D: "distinct (map fst (xs @ x # accu))"
by simp
from Cons.prems(4) and False have E: "k ∉ set (map fst (x # accu))"
by simp
note Cons.IH[OF B C D E]
also from False have "?f xs (x#accu) = ?f (x#xs) accu" by simp
also from distinct_map_fstD[OF D]
have F: "⋀z. (fst x, z) ∈ set xs ⟹ z = snd x" by force
have "map_of (x # accu) ++ op_map_update k' v' (map_of xs) =
accu' ++ op_map_update k' v' m'"
by (intro ext, auto simp: A F map_add_def
dest: map_of_SomeD split: option.split)
finally show ?thesis .
qed
qed

lemma list_map_autoref_update2[param]:
shows "(list_map_update (=), op_map_update) ∈ Id → Id →
br map_of list_map_invar → br map_of list_map_invar"
unfolding list_map_update_def[abs_def]
apply (intro fun_relI)
apply (drule list_map_autoref_update_aux2
[where accu="[]" and accu'="Map.empty"])
apply (auto simp: br_def list_map_invar_def)
done

lemma list_map_autoref_update[autoref_rules]:
assumes eq: "GEN_OP eq (=) (Rk→Rk→Id)"
shows "(list_map_update eq, op_map_update) ∈
Rk → Rv → ⟨Rk,Rv⟩list_map_rel → ⟨Rk,Rv⟩list_map_rel"
unfolding list_map_rel_def
apply (intro fun_relI, elim relcompE, intro relcompI, clarsimp)
apply (erule (2) list_map_autoref_update1[param_fo, OF eq[simplified]])
apply (rule list_map_autoref_update2[param_fo], simp_all)
done

context begin interpretation autoref_syn .
lemma list_map_autoref_update_dj[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes new: "SIDE_PRECOND_OPT (k' ∉ dom m')"
assumes K: "(k,k')∈Rk" and V: "(v,v')∈Rv"
assumes M: "(l,m')∈⟨Rk, Rv⟩list_map_rel"
defines "R_annot ≡ Rk → Rv → ⟨Rk,Rv⟩list_map_rel → ⟨Rk,Rv⟩list_map_rel"
shows "
((k, v)#l,
(OP op_map_update:::R_annot)\$k'\$v'\$m')
∈ ⟨Rk,Rv⟩list_map_rel"
proof -
from M obtain l' where A: "(l,l') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel" and
B: "(l',m') ∈ br map_of list_map_invar"
unfolding list_map_rel_def by blast
hence "((k,v)#l, (k',v')#l')∈⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
and "((k',v')#l', m'(k' ↦ v')) ∈ br map_of list_map_invar"
using assms unfolding br_def list_map_invar_def
thus ?thesis
unfolding autoref_tag_defs
by (force simp: list_map_rel_def)
qed
end

lemma param_list_map_delete_aux[param]:
"(list_map_delete_aux,list_map_delete_aux) ∈ (Rk → Rk → bool_rel) →
Rk → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel
→ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
unfolding list_map_delete_aux_def[abs_def] by parametricity

lemma param_list_map_delete[param]:
"(list_map_delete,list_map_delete) ∈ (Rk → Rk → bool_rel) →
Rk → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
unfolding list_map_delete_def[abs_def] by parametricity

lemma list_map_autoref_delete_aux1:
assumes eq: "(eq,(=)) ∈ Rk → Rk → Id"
assumes K: "(k, k') ∈ Rk"
assumes A: "(accu, accu') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
assumes M: "(m, m') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
shows "(list_map_delete_aux eq k m accu,
list_map_delete_aux (=) k' m' accu')
∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
proof (insert A, induction arbitrary: accu accu'
rule: list_rel_induct[OF M, case_names Nil Cons])
case Nil
thus ?case by (simp add: K)
next
case (Cons x x' xs xs')
from eq have eq': "(eq,(=)) ∈ Rk → Rk → Id" by simp
from eq'[param_fo] Cons(1) K
have [simp]: "(eq (fst x) k) ⟷ ((fst x') = k')"
by (force simp: prod_rel_def)
show ?case
proof (cases "eq (fst x) k")
case False
from Cons.prems and Cons.hyps have "(x # accu, x' # accu') ∈
⟨⟨Rk, Rv⟩prod_rel⟩list_rel" by parametricity
from Cons.IH[OF this] and False show ?thesis by simp
next
case True
from Cons.prems and Cons.hyps have "(xs @ accu, xs' @ accu') ∈
⟨⟨Rk, Rv⟩prod_rel⟩list_rel" by parametricity
with K and True show ?thesis by simp
qed
qed

lemma list_map_autoref_delete1[param]:
assumes eq: "(eq,(=)) ∈ Rk → Rk → Id"
shows "(list_map_delete eq, list_map_delete (=)) ∈ Rk →
⟨⟨Rk, Rv⟩prod_rel⟩list_rel → ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
unfolding list_map_delete_def[abs_def]
by (intro fun_relI, erule list_map_autoref_delete_aux1[OF eq],
simp_all)

lemma list_map_autoref_delete_aux2:
assumes K: "(k, k') ∈ Id"
assumes A: "(accu, accu') ∈ br map_of list_map_invar"
assumes A1: "distinct (map fst (m @ accu))"
assumes A2: "k ∉ set (map fst accu)"
assumes M: "(m, m') ∈ br map_of list_map_invar"
shows "(list_map_delete_aux (=) k m accu,
accu' ++ op_map_delete k' m')
∈ br map_of list_map_invar" (is "(?f m accu, _) ∈ _")
using M A A1 A2
proof (induction m arbitrary: accu accu' m')
case Nil
with K show ?case by (auto simp: br_def list_map_invar_def
next
case (Cons x xs accu accu' m')
from Cons.prems have A: "m' = map_of (x#xs)" "accu' = map_of accu"
unfolding br_def by simp_all
show ?case
proof (cases "(fst x) =  k")
case True
with Cons.prems(3) have "map_of xs (fst x) = None"
by (induction xs, simp_all)
with fun_upd_triv[of "map_of xs" "fst x"]
have "map_of xs |` (- {fst x}) = map_of xs"
with True have"(xs @ accu, accu' ++ op_map_delete k' m')
∈ br map_of list_map_invar"
using K Cons.prems unfolding br_def
by (auto simp add: A list_map_invar_def)
thus ?thesis using True by simp
next
case False
from False and K have [simp]: "fst x ≠ k'" by simp
from Cons.prems(1) have B: "(xs, map_of xs) ∈ br map_of
from Cons.prems(2,3) have C: "(x#accu, map_of (x#accu)) ∈ br map_of
list_map_invar" by (simp add: br_def list_map_invar_def)
from Cons.prems(3) have D: "distinct (map fst (xs @ x # accu))"
by simp
from Cons.prems(4) and False have E: "k ∉ set (map fst (x # accu))"
by simp
note Cons.IH[OF B C D E]
also from False have "?f xs (x#accu) = ?f (x#xs) accu" by simp
also from distinct_map_fstD[OF D]
have F: "⋀z. (fst x, z) ∈ set xs ⟹ z = snd x" by force

from Cons.prems(3) have "map_of xs (fst x) = None"
by (induction xs, simp_all)
hence "map_of (x # accu) ++ op_map_delete k' (map_of xs) =
accu' ++ op_map_delete k' m'"
split: option.split)
apply (intro conjI impI allI)
apply (auto simp: restrict_map_def)
done
finally show ?thesis .
qed
qed

lemma list_map_autoref_delete2[param]:
shows "(list_map_delete (=), op_map_delete) ∈ Id →
br map_of list_map_invar → br map_of list_map_invar"
unfolding list_map_delete_def[abs_def]
apply (intro fun_relI)
apply (drule list_map_autoref_delete_aux2
[where accu="[]" and accu'="Map.empty"])
apply (auto simp: br_def list_map_invar_def)
done

lemma list_map_autoref_delete[autoref_rules]:
assumes eq: "GEN_OP eq (=) (Rk→Rk→Id)"
shows "(list_map_delete eq, op_map_delete) ∈
Rk → ⟨Rk,Rv⟩list_map_rel → ⟨Rk,Rv⟩list_map_rel"
unfolding list_map_rel_def
apply (intro fun_relI, elim relcompE, intro relcompI, clarsimp)
apply (erule (1) list_map_autoref_delete1[param_fo, OF eq[simplified]])
apply (rule list_map_autoref_delete2[param_fo], simp_all)
done

lemma list_map_autoref_isEmpty[autoref_rules]:
shows "(list_map_isEmpty, op_map_isEmpty) ∈
⟨Rk,Rv⟩list_map_rel → bool_rel"
unfolding list_map_isEmpty_def op_map_isEmpty_def[abs_def]
list_map_rel_def br_def List.null_def[abs_def] by force

lemma param_list_map_isSng[param]:
assumes "(l,l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
shows "(list_map_isSng l, list_map_isSng l') ∈ bool_rel"
unfolding list_map_isSng_def using assms by parametricity

(* TODO: clean up this mess *)
lemma list_map_autoref_isSng_aux:
assumes "(l',m') ∈ br map_of list_map_invar"
shows "(list_map_isSng l', op_map_isSng m') ∈ bool_rel"
using assms
unfolding list_map_isSng_def op_map_isSng_def br_def list_map_invar_def
apply (clarsimp split: list.split)
apply (intro conjI impI allI)
apply (metis map_upd_nonempty)
apply blast
apply (simp, metis fun_upd_apply option.distinct(1))
done

lemma list_map_autoref_isSng[autoref_rules]:
"(list_map_isSng, op_map_isSng) ∈ ⟨Rk,Rv⟩list_map_rel → bool_rel"
unfolding list_map_rel_def
by (blast dest!: param_list_map_isSng list_map_autoref_isSng_aux)

lemma list_map_autoref_size_aux:
assumes "distinct (map fst x)"
shows "card (dom (map_of x)) = length x"
proof-
have "card (dom (map_of x)) = card (map_to_set (map_of x))"
also from assms have "... = card (set x)"
also from assms have "... = length x"
by (force simp: distinct_card dest!: distinct_mapI)
finally show ?thesis .
qed

lemma param_list_map_size[param]:
"(list_map_size, list_map_size) ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → nat_rel"
unfolding list_map_size_def[abs_def] by parametricity

lemma list_map_autoref_size[autoref_rules]:
shows "(list_map_size, op_map_size) ∈
⟨Rk,Rv⟩list_map_rel → nat_rel"
unfolding list_map_size_def[abs_def] op_map_size_def[abs_def]
list_map_rel_def br_def list_map_invar_def
by (force simp: list_map_autoref_size_aux list_rel_imp_same_length)

lemma autoref_list_map_is_iterator[autoref_ga_rules]:
shows "is_map_to_list Rk Rv list_map_rel list_map_to_list"
unfolding is_map_to_list_def is_map_to_sorted_list_def
proof (clarify)
fix l m'
assume "(l,m') ∈ ⟨Rk,Rv⟩list_map_rel"
then obtain l' where *: "(l,l')∈⟨⟨Rk,Rv⟩prod_rel⟩list_rel" "(l',m')∈br map_of list_map_invar"
unfolding list_map_rel_def by blast
then have "RETURN l' ≤ it_to_sorted_list (key_rel (λ_ _. True)) (map_to_set m')"
unfolding it_to_sorted_list_def
apply (intro refine_vcg)
unfolding br_def list_map_invar_def key_rel_def[abs_def]
apply (auto intro: distinct_mapI simp: map_to_set_map_of)
done
with * show
"∃l'. (list_map_to_list l, l') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel ∧
RETURN l' ≤ it_to_sorted_list (key_rel (λ_ _. True))
(map_to_set m')"
unfolding list_map_to_list_def by force
qed

lemma pi_list_map[icf_proper_iteratorI]:
"proper_it (list_map_iteratei m) (list_map_iteratei m)"
unfolding proper_it_def list_map_iteratei_def by blast

lemma pi'_list_map[icf_proper_iteratorI]:
"proper_it' list_map_iteratei list_map_iteratei"
by (rule proper_it'I, rule pi_list_map)

primrec list_map_pick_remove where
"list_map_pick_remove [] = undefined"
| "list_map_pick_remove (kv#l) = (kv,l)"

context begin interpretation autoref_syn .
lemma list_map_autoref_pick_remove[autoref_rules]:
assumes NE: "SIDE_PRECOND (m≠Map.empty)"
assumes R: "(l,m)∈⟨Rk,Rv⟩list_map_rel"
defines "Rres ≡ ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩list_map_rel⟩nres_rel"
shows "(
RETURN (list_map_pick_remove l),
(OP op_map_pick_remove ::: ⟨Rk,Rv⟩list_map_rel → Rres)\$m
) ∈ Rres"
proof -
from NE R obtain k v lr where
[simp]: "l=(k,v)#lr"
by (cases l) (auto simp: list_map_rel_def br_def)

thm list_map_rel_def
from R obtain l' where
LL': "(l,l')∈⟨Rk×⇩rRv⟩list_rel" and
L'M: "(l',m)∈br map_of list_map_invar"
unfolding list_map_rel_def by auto
from LL' obtain k' v' lr' where
[simp]: "l' = (k',v')#lr'" and
KVR: "(k,k')∈Rk" "(v,v')∈Rv" and
LRR: "(lr,lr')∈⟨Rk×⇩rRv⟩list_rel"
by (fastforce elim!: list_relE)

from L'M have
MKV': "m k' = Some v'" and
LRR': "(lr',m|`(-{k'}))∈br map_of list_map_invar"
by (auto
simp: restrict_map_def map_of_eq_None_iff br_def list_map_invar_def
intro!: ext
intro: sym)

from LRR LRR' have LM: "(lr,m|`(-{k'}))∈⟨Rk,Rv⟩list_map_rel"
unfolding list_map_rel_def by auto

show ?thesis