# Theory Gen_Map2Set

```section ‹\isaheader{Generic Map To Set Converter}›
theory Gen_Map2Set
imports
"../Intf/Intf_Map"
"../Intf/Intf_Set"
"../Intf/Intf_Comp"
"../../Iterator/Iterator"
begin

lemma map_fst_unit_distinct_eq[simp]:
fixes l :: "('k×unit) list"
shows "distinct (map fst l) ⟷ distinct l"
by (induct l) auto

definition
map2set_rel :: "
(('ki×'k) set ⇒ (unit×unit) set ⇒ ('mi×('k⇀unit))set) ⇒
('ki×'k) set ⇒
('mi×('k set)) set"
where
map2set_rel_def_internal:
"map2set_rel R Rk ≡ ⟨Rk,Id::(unit×_) set⟩R O {(m,dom m)| m. True}"

lemma map2set_rel_def: "⟨Rk⟩(map2set_rel R)
= ⟨Rk,Id::(unit×_) set⟩R O {(m,dom m)| m. True}"
unfolding map2set_rel_def_internal[abs_def] by (simp add: relAPP_def)

lemma map2set_relI:
assumes "(s,m')∈⟨Rk,Id⟩R" and "s'=dom m'"
shows "(s,s')∈⟨Rk⟩map2set_rel R"
using assms unfolding map2set_rel_def by blast

lemma map2set_relE:
assumes "(s,s')∈⟨Rk⟩map2set_rel R"
obtains m' where "(s,m')∈⟨Rk,Id⟩R" and "s'=dom m'"
using assms unfolding map2set_rel_def by blast

lemma map2set_rel_sv[relator_props]:
"single_valued (⟨Rk,Id⟩Rm) ⟹ single_valued (⟨Rk⟩map2set_rel Rm)"
unfolding map2set_rel_def
by (auto intro: single_valuedI dest: single_valuedD)

lemma map2set_empty[autoref_rules_raw]:
assumes "PRIO_TAG_GEN_ALGO"
assumes "GEN_OP e op_map_empty (⟨Rk,Id⟩R)"
shows "(e,{})∈⟨Rk⟩map2set_rel R"
using assms
unfolding map2set_rel_def
by auto

lemmas [autoref_rel_intf] =
REL_INTFI[of "map2set_rel R" i_set] for R

definition "map2set_insert i k s ≡ i k () s"
lemma map2set_insert[autoref_rules_raw]:
assumes "PRIO_TAG_GEN_ALGO"
assumes "GEN_OP i op_map_update (Rk → Id → ⟨Rk,Id⟩R → ⟨Rk,Id⟩R)"
shows
"(map2set_insert i,Set.insert)∈Rk→⟨Rk⟩map2set_rel R → ⟨Rk⟩map2set_rel R"
using assms
unfolding map2set_rel_def map2set_insert_def[abs_def]
by (force dest: fun_relD)

definition "map2set_memb l k s ≡ case l k s of None ⇒ False | Some _ ⇒ True"
lemma map2set_memb[autoref_rules_raw]:
assumes "PRIO_TAG_GEN_ALGO"
assumes "GEN_OP l op_map_lookup (Rk → ⟨Rk,Id⟩R → ⟨Id⟩option_rel)"
shows "(map2set_memb l ,(∈))
∈ Rk→⟨Rk⟩map2set_rel R→Id"
using assms
unfolding map2set_rel_def map2set_memb_def[abs_def]
by (force dest: fun_relD split: option.splits)

lemma map2set_delete[autoref_rules_raw]:
assumes "PRIO_TAG_GEN_ALGO"
assumes "GEN_OP d op_map_delete (Rk→⟨Rk,Id⟩R→⟨Rk,Id⟩R)"
shows "(d,op_set_delete)∈Rk→⟨Rk⟩map2set_rel R→⟨Rk⟩map2set_rel R"
using assms
unfolding map2set_rel_def
by (force dest: fun_relD)

lemma map2set_to_sorted_list[autoref_ga_rules]:
fixes it :: "'m ⇒ ('k×unit) list"
assumes A: "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Id R it)"
shows "is_set_to_sorted_list ordR Rk (map2set_rel R)
(it_to_list (map_iterator_dom o (foldli o it)))"
proof -
{
fix l::"('k×unit) list"
have "⋀l0. foldli l (λ_. True) (λx σ. σ @ [fst x]) l0 = l0@map fst l"
by (induct l) auto
}
hence S: "it_to_list (map_iterator_dom o (foldli o it)) = map fst o it"
unfolding it_to_list_def[abs_def] map_iterator_dom_def[abs_def]
set_iterator_image_def set_iterator_image_filter_def
by (auto)
show ?thesis
unfolding S
using assms
unfolding is_map_to_sorted_list_def is_set_to_sorted_list_def
apply clarsimp
apply (erule map2set_relE)
apply (drule spec, drule spec)
apply (drule (1) mp)
apply (elim exE conjE)
apply (rule_tac x="map fst l'" in exI)
apply (rule conjI)
apply parametricity

unfolding it_to_sorted_list_def
done
qed

lemma map2set_to_list[autoref_ga_rules]:
fixes it :: "'m ⇒ ('k×unit) list"
assumes A: "GEN_ALGO_tag (is_map_to_list Rk Id R it)"
shows "is_set_to_list Rk (map2set_rel R)
(it_to_list (map_iterator_dom o (foldli o it)))"
using assms unfolding is_set_to_list_def is_map_to_list_def
by (rule map2set_to_sorted_list)

(*lemma map2set_it_simp[iterator_simps]:
"foldli ((map fst o it) x) c f s = foldli (it x) c (λ(k,v) s. f k s) s"
by (simp add: foldli_map comp_def fn_fst_conv)
*)

text ‹Transfering also non-basic operations results in specializations
of map-algorithms to also be used for sets›
lemma map2set_union[autoref_rules_raw]:
assumes "MINOR_PRIO_TAG (- 9)"
assumes "GEN_OP u (++) (⟨Rk,Id⟩R→⟨Rk,Id⟩R→⟨Rk,Id⟩R)"
shows "(u,(∪))∈⟨Rk⟩map2set_rel R→⟨Rk⟩map2set_rel R→⟨Rk⟩map2set_rel R"
using assms
unfolding map2set_rel_def
by (force dest: fun_relD)

lemmas [autoref_ga_rules] = cmp_unit_eq_linorder
lemmas [autoref_rules_raw] = param_cmp_unit

lemma cmp_lex_zip_unit[simp]:
"cmp_lex (cmp_prod cmp cmp_unit) (map (λk. (k, ())) l)
(map (λk. (k, ())) m) =
cmp_lex cmp l m"
apply (induct cmp l m rule: cmp_lex.induct)
apply (auto split: comp_res.split)
done

lemma cmp_img_zip_unit[simp]:
"cmp_img (λm. map (λk. (k,())) (f m)) (cmp_lex (cmp_prod cmp1 cmp_unit))
= cmp_img f (cmp_lex cmp1)"
unfolding cmp_img_def[abs_def]
apply (intro ext)
apply simp
done

(* TODO: Move *)

lemma map2set_finite[relator_props]:
assumes "finite_map_rel (⟨Rk,Id⟩R)"
shows "finite_set_rel (⟨Rk⟩map2set_rel R)"
using assms
unfolding map2set_rel_def finite_set_rel_def finite_map_rel_def
by auto

lemma map2set_cmp[autoref_rules_raw]:
assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmpk)"
assumes MPAR:
"GEN_OP cmp (cmp_map cmpk cmp_unit) (⟨Rk,Id⟩R → ⟨Rk,Id⟩R → Id)"
assumes FIN: "PREFER finite_map_rel (⟨Rk, Id⟩R)"
shows "(cmp,cmp_set cmpk)∈⟨Rk⟩map2set_rel R → ⟨Rk⟩map2set_rel R → Id"
proof -
interpret linorder "comp2le cmpk" "comp2lt cmpk"
using ELO by (simp add: eq_linorder_class_conv)

show ?thesis
using MPAR
unfolding cmp_map_def cmp_set_def
apply simp
apply parametricity
apply (drule cmp_extend_paramD)
apply (insert FIN, fastforce simp add: finite_map_rel_def) []