# Theory Gen_Map

```section ‹\isaheader{Generic Map Algorithms}›
theory Gen_Map
imports "../Intf/Intf_Map" "../../Iterator/Iterator"
begin
lemma map_to_set_distinct_conv:
assumes "distinct tsl'" and "map_to_set m' = set tsl'"
shows "distinct (map fst tsl')"
apply (rule ccontr)
apply (drule not_distinct_decomp)
using assms
apply (clarsimp elim!: map_eq_appendE)
by (metis (opaque_lifting, no_types) insert_iff map_to_set_inj)

(* TODO: Make foldli explicit, such that it is seen by
iterator-optimizations! cf Gen_Set for how to do this! *)
(λ_. True) (λ(k,v) m. op_map_update k v m) m ((++) m)"
proof (rule, goal_cases)
case (1 l) thus ?case
apply (induct l arbitrary: m)
apply (auto simp: map_of_distinct_upd[symmetric])
done
qed

:: "('s2 ⇒ _) ⇒ ('k ⇒ 'v ⇒ 's1 ⇒ 's1) ⇒ 's1 ⇒ 's2 ⇒ 's1"
where
"gen_add it upd A B ≡ it B (λ_. True) (λ(k,v) m. upd k v m) A"

assumes PRIO_TAG_GEN_ALGO
assumes UPD: "GEN_OP ins op_map_update (Rk→Rv→⟨Rk,Rv⟩Rs1→⟨Rk,Rv⟩Rs1)"
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs2 tsl)"
shows "(gen_add (foldli o tsl) ins,(++))
∈ (⟨Rk,Rv⟩Rs1) → (⟨Rk,Rv⟩Rs2) → (⟨Rk,Rv⟩Rs1)"
apply (intro fun_relI)
apply (rule det_fold_map[OF foldli_add IT[unfolded autoref_tag_defs]])
done

lemma foldli_restrict: "det_fold_map X (λ_. True)
(λ(k,v) m. if P (k,v) then op_map_update k v m else m) Map.empty
(op_map_restrict P )" (is "det_fold_map _ _ ?f _ _")
proof -
{
fix l m
have "distinct (map fst l) ⟹
foldli l (λ_. True) ?f m = m ++ op_map_restrict P (map_of l)"
proof (induction l arbitrary: m)
case Nil thus ?case by simp
next
case (Cons kv l)
obtain k v where [simp]: "kv = (k,v)" by fastforce
from Cons.prems have
DL: "distinct (map fst l)" and KNI: "k ∉ set (map fst l)"
by auto

show ?case proof (cases "P (k,v)")
case [simp]: True
have "foldli (kv#l) (λ_. True) ?f m = foldli l (λ_. True) ?f (m(k↦v))"
by simp
also from Cons.IH[OF DL] have
"… = m(k↦v) ++ op_map_restrict P (map_of l)" .
also have "… = m ++ op_map_restrict P (map_of (kv#l))"
using KNI
by (auto
split: option.splits
intro!: ext
simp: map_of_eq_None_iff[symmetric])
finally show ?thesis .
next
case [simp]: False
have "foldli (kv#l) (λ_. True) ?f m = foldli l (λ_. True) ?f m"
by simp
also from Cons.IH[OF DL] have
"… = m ++ op_map_restrict P (map_of l)" .
also have "… = m ++ op_map_restrict P (map_of (kv#l))"
using KNI
by (auto
intro!: ext
simp: map_of_eq_None_iff[symmetric]
)
finally show ?thesis .
qed
qed
}
from this[of _ Map.empty] show ?thesis
by (auto intro!: det_fold_mapI)
qed

definition gen_restrict :: "('s1 ⇒ _) ⇒ _"
where "gen_restrict it upd emp P m
≡ it m (λ_. True) (λ(k,v) m. if P (k,v) then upd k v m else m) emp"

lemma gen_restrict[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs1 tsl)"
assumes INS:
"GEN_OP upd op_map_update (Rk→Rv→⟨Rk,Rv⟩Rs2→⟨Rk,Rv⟩Rs2)"
assumes EMPTY:
"GEN_OP emp Map.empty (⟨Rk,Rv⟩Rs2)"
shows "(gen_restrict (foldli o tsl) upd emp,op_map_restrict)
∈ (⟨Rk,Rv⟩prod_rel → Id) → (⟨Rk,Rv⟩Rs1) → (⟨Rk,Rv⟩Rs2)"
apply (intro fun_relI)
unfolding gen_restrict_def comp_def
apply (rule det_fold_map[OF foldli_restrict IT[unfolded autoref_tag_defs]])
using INS EMPTY unfolding autoref_tag_defs
apply (parametricity)+
done

lemma fold_map_of:
"fold (λ(k,v) s. op_map_update k v s) (rev l) Map.empty = map_of l"
proof -
{
fix m
have "fold (λ(k,v) s. s(k↦v)) (rev l) m = m ++ map_of l"
apply (induct l arbitrary: m)
apply auto
done
} thus ?thesis by simp
qed

definition gen_map_of :: "'m ⇒ ('k⇒'v⇒'m⇒'m) ⇒ _" where
"gen_map_of emp upd l ≡ fold (λ(k,v) s. upd k v s) (rev l) emp"

lemma gen_map_of[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes UPD: "GEN_OP upd op_map_update (Rk→Rv→⟨Rk,Rv⟩Rm→⟨Rk,Rv⟩Rm)"
assumes EMPTY: "GEN_OP emp Map.empty (⟨Rk,Rv⟩Rm)"
shows "(gen_map_of emp upd,map_of) ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨Rk,Rv⟩Rm"
using assms
apply (intro fun_relI)
unfolding gen_map_of_def[abs_def]
unfolding autoref_tag_defs
apply (subst fold_map_of[symmetric])
apply parametricity
done

lemma foldli_ball_aux:
"distinct (map fst l) ⟹ foldli l (λx. x) (λx _. P x) b
⟷ b ∧ op_map_ball (map_of l) P"
apply (induct l arbitrary: b)
apply simp
apply (force simp: map_to_set_map_of image_def)
done

lemma foldli_ball:
"det_fold_map X (λx. x) (λx _. P x) True (λm. op_map_ball m P)"
apply rule
using foldli_ball_aux[where b=True] by auto

definition gen_ball :: "('m ⇒ _) ⇒ _" where
"gen_ball it m P ≡ it m (λx. x) (λx _. P x) True"

lemma gen_ball[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
shows "(gen_ball (foldli o tsl),op_map_ball)
∈ ⟨Rk,Rv⟩Rm → (⟨Rk,Rv⟩prod_rel → Id) → Id"
apply (intro fun_relI)
unfolding gen_ball_def comp_def
apply (rule det_fold_map[OF foldli_ball IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done

lemma foldli_bex_aux:
"distinct (map fst l) ⟹ foldli l (λx. ¬x) (λx _. P x) b
⟷ b ∨ op_map_bex (map_of l) P"
apply (induct l arbitrary: b)
apply simp
apply (force simp: map_to_set_map_of image_def)
done

lemma foldli_bex:
"det_fold_map X (λx. ¬x) (λx _. P x) False (λm. op_map_bex m P)"
apply rule
using foldli_bex_aux[where b=False] by auto

definition gen_bex :: "('m ⇒ _) ⇒ _" where
"gen_bex it m P ≡ it m (λx. ¬x) (λx _. P x) False"

lemma gen_bex[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
shows "(gen_bex (foldli o tsl),op_map_bex)
∈ ⟨Rk,Rv⟩Rm → (⟨Rk,Rv⟩prod_rel → Id) → Id"
apply (intro fun_relI)
unfolding gen_bex_def comp_def
apply (rule det_fold_map[OF foldli_bex IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done

lemma ball_isEmpty: "op_map_isEmpty m = op_map_ball m (λ_. False)"
apply (auto intro!: ext)
by (metis map_to_set_simps(7) option.exhaust)

definition "gen_isEmpty ball m ≡ ball m (λ_. False)"

lemma gen_isEmpty[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes BALL:
"GEN_OP ball op_map_ball (⟨Rk,Rv⟩Rm→(⟨Rk,Rv⟩prod_rel→Id) → Id)"
shows "(gen_isEmpty ball,op_map_isEmpty)
∈ ⟨Rk,Rv⟩Rm → Id"
apply (intro fun_relI)
unfolding gen_isEmpty_def using assms
unfolding autoref_tag_defs
apply -
apply (subst ball_isEmpty)
apply parametricity+
done

lemma foldli_size_aux: "distinct (map fst l)
⟹ foldli l (λ_. True) (λ_ n. Suc n) n = n + op_map_size (map_of l)"
apply (induct l arbitrary: n)
apply (auto simp: dom_map_of_conv_image_fst)
done

lemma foldli_size: "det_fold_map X (λ_. True) (λ_ n. Suc n) 0 op_map_size"
apply rule
using foldli_size_aux[where n=0] by simp

definition gen_size :: "('m ⇒ _) ⇒ _"
where "gen_size it m ≡ it m (λ_. True) (λ_ n. Suc n) 0"

lemma gen_size[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
shows "(gen_size (foldli o tsl),op_map_size) ∈ ⟨Rk,Rv⟩Rm → Id"
apply (intro fun_relI)
unfolding gen_size_def comp_def
apply (rule det_fold_map[OF foldli_size IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done

lemma foldli_size_abort_aux:
"⟦n0≤m; distinct (map fst l)⟧ ⟹
foldli l (λn. n<m) (λ_ n. Suc n) n0 = min m (n0 + card (dom (map_of l)))"
apply (induct l arbitrary: n0)
apply (auto simp: dom_map_of_conv_image_fst)
done

lemma foldli_size_abort:
"det_fold_map X (λn. n<m) (λ_ n. Suc n) 0 (op_map_size_abort m)"
apply rule
using foldli_size_abort_aux[where ?n0.0=0]
by simp

definition gen_size_abort :: "('s ⇒ _) ⇒ _" where
"gen_size_abort it m s ≡ it s (λn. n<m) (λ_ n. Suc n) 0"

lemma gen_size_abort[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
shows "(gen_size_abort (foldli o tsl),op_map_size_abort)
∈ Id → ⟨Rk,Rv⟩Rm → Id"
apply (intro fun_relI)
unfolding gen_size_abort_def comp_def
apply (rule det_fold_map[OF foldli_size_abort
IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done

lemma size_abort_isSng: "op_map_isSng s ⟷ op_map_size_abort 2 s = 1"
by (auto simp: dom_eq_singleton_conv min_def dest!: card_eq_SucD)

definition gen_isSng :: "(nat ⇒ 's ⇒ nat) ⇒ _" where
"gen_isSng sizea s ≡ sizea 2 s = 1"

lemma gen_isSng[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "GEN_OP sizea op_map_size_abort (Id → (⟨Rk,Rv⟩Rm) → Id)"
shows "(gen_isSng sizea,op_map_isSng)
∈ ⟨Rk,Rv⟩Rm → Id"
apply (intro fun_relI)
unfolding gen_isSng_def using assms
unfolding autoref_tag_defs
apply -
apply (subst size_abort_isSng)
apply parametricity
done

(* TODO: Also do sel! *)

lemma foldli_pick:
assumes "l≠[]"
obtains k v where "(k,v)∈set l"
and "(foldli l (case_option True (λ_. False)) (λx _. Some x) None)
= Some (k,v)"
using assms by (cases l) auto

definition gen_pick where
"gen_pick it s ≡
(the (it s (case_option True (λ_. False)) (λx _. Some x) None))"

context begin interpretation autoref_syn .

lemma gen_pick[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm it)"
assumes NE: "SIDE_PRECOND (m'≠Map.empty)"
assumes SREF: "(m,m')∈⟨Rk,Rv⟩Rm"
shows "(RETURN (gen_pick (λx. foldli (it x)) m),
(OP op_map_pick ::: ⟨Rk,Rv⟩Rm→⟨Rk×⇩rRv⟩nres_rel)\$m')∈⟨Rk×⇩rRv⟩nres_rel"
proof -
thm is_map_to_list_def is_map_to_sorted_listE

obtain tsl' where
[param]: "(it m,tsl') ∈ ⟨Rk×⇩rRv⟩list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) (map_to_set m')"
using IT[unfolded autoref_tag_defs is_map_to_list_def] SREF
by (auto intro: is_map_to_sorted_listE)

from IT' NE have "tsl'≠[]" and [simp]: "m'=map_of tsl'"
and DIS': "distinct (map fst tsl')"
unfolding it_to_sorted_list_def
apply simp_all
apply (metis empty_set map_to_set_empty_iff(1))
apply (metis map_of_map_to_set map_to_set_distinct_conv)
apply (metis map_to_set_distinct_conv)
done

then obtain k v where "m' k = Some v" and
"(foldli tsl' (case_option True (λ_. False)) (λx _. Some x) None)
= Some (k,v)"
(is "?fld = _")
by (cases rule: foldli_pick) auto
moreover
have "(RETURN (gen_pick (λx. foldli (it x)) m), RETURN (the ?fld))
∈ ⟨Rk×⇩rRv⟩nres_rel"
unfolding gen_pick_def
using ‹?fld = Some (k,v)›
by simp
ultimately show ?thesis
unfolding autoref_tag_defs
apply -
apply (drule nres_relD)
apply (rule nres_relI)
apply (erule ref_two_step)
by simp
qed
end

definition "gen_map_pick_remove pick del m ≡ do {
(k,v)←pick m;
let m = del k m;
RETURN ((k,v),m)
}"

context begin interpretation autoref_syn .
lemma gen_map_pick_remove
[unfolded gen_map_pick_remove_def, autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes PICK: "SIDE_GEN_OP (
(pick m,
(OP op_map_pick ::: ⟨Rk,Rv⟩Rm → ⟨Rk×⇩rRv⟩nres_rel)\$m') ∈
⟨Rk×⇩rRv⟩nres_rel)"
assumes DEL: "GEN_OP del op_map_delete (Rk → ⟨Rk,Rv⟩Rm → ⟨Rk,Rv⟩Rm)"
assumes [param]: "(m,m')∈⟨Rk,Rv⟩Rm"
shows "(gen_map_pick_remove pick del m,
(OP op_map_pick_remove
::: ⟨Rk,Rv⟩Rm → ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel)\$m')
∈ ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel"
proof -
note [param] =
PICK[unfolded autoref_tag_defs]
DEL[unfolded autoref_tag_defs]

have "(gen_map_pick_remove pick del m,
do {
(k,v)←op_map_pick m';
let m' = op_map_delete k m';
RETURN ((k,v),m')
}) ∈ ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel" (is "(_,?h):_")
unfolding gen_map_pick_remove_def[abs_def]
apply parametricity
done
also have "?h = op_map_pick_remove m'"
by (auto simp add: pw_eq_iff refine_pw_simps)
finally show ?thesis by simp
qed
end

end
```