# Theory Mapping2

theory Mapping2
imports Map2 Mapping
```(*
Author:      Salomon Sickert
*)

section ‹Auxiliary Mapping Facts›

theory Mapping2
imports Main Map2 "HOL-Library.Mapping"
begin

lemma lookup_delete:
"Mapping.lookup (Mapping.delete k m) k = None"
by (transfer; simp)

lemma lookup_tabulate:
"Mapping.lookup (Mapping.tabulate xs f) x = (if x ∈ set xs then Some (f x) else None)"
by (transfer; insert map_of_tabulate_simp)

lemma lookup_tabulate_Some:
"x ∈ set xs ⟹ the (Mapping.lookup (Mapping.tabulate xs f) x) = f x"

lemma finite_keys_tabulate:
"finite (Mapping.keys (Mapping.tabulate xs f))"
by simp

lemma keys_empty_iff_map_empty:
"Mapping.keys m = {} ⟷ m = Mapping.empty"
by (transfer; simp)

lemma mapping_equal:
"Mapping.keys m = Mapping.keys m' ⟹ (⋀x. x ∈ Mapping.keys m ⟹ Mapping.lookup m x = Mapping.lookup m' x) ⟹ m = m'"
by (transfer; blast intro: map_equal)

fun mapping_generator :: "('a ⇒ 'b list) ⇒ 'a list ⇒ ('a, 'b) mapping set"
where
"mapping_generator V [] = {Mapping.empty}"
| "mapping_generator V (k#ks) = {Mapping.update k v m | v m.  v ∈ set (V k) ∧ m ∈ mapping_generator V ks}"

fun mapping_generator_list :: "('a ⇒ 'b list) ⇒ 'a list ⇒ ('a, 'b) mapping list"
where
"mapping_generator_list V [] = [Mapping.empty]"
| "mapping_generator_list V (k#ks) = concat (map (λm. map (λv. Mapping.update k v m) (V k)) (mapping_generator_list V ks))"

lemma mapping_generator_code [code]:
"mapping_generator V K = set (mapping_generator_list V K)"
by (induction K) auto

lemma mapping_generator_set_eq:
"mapping_generator V K = {m. Mapping.keys m = set K ∧ (∀k ∈ (set K). the (Mapping.lookup m k) ∈ set (V k))}"
proof (induction K)
case (Cons k ks)
let ?l = "{m(k ↦ v) |v m. v ∈ set (V k) ∧  m ∈ {m. dom m = set ks ∧ (∀k∈set ks. the (m k) ∈ set (V k))}}"
let ?r = "{m. dom m = set (k # ks) ∧ (∀k∈set (k # ks). the (m k) ∈ set (V k))}"

have "?l ⊆ ?r"
by fastforce
moreover
{
fix m
assume "m ∈ ?r"
hence "dom m = set (k#ks)"
and "∀k ∈ set (k#ks). the (m k) ∈ set (V k)"
and "∀k' ∈ set (k#ks). m k ≠ None"
by auto
moreover
then obtain m' where "dom m' = set ks"
and "∀x ∈ set ks. m x = m' x"
using map_reduce[of m k "set ks"] by auto
ultimately
have "the (m k) ∈ set (V k)"
and "dom m' = set ks"
and "∀k ∈ (set ks). the (m' k) ∈ set (V k)"
and "m = m'(k ↦ the (m k))"
apply (simp, blast, auto)
apply (insert map_equal[of m "m'(k ↦ the (m k))"])
apply (unfold dom_map_update ‹dom m = set (k#ks)› ‹dom m' = set ks›)
by fastforce
moreover
hence "m ∈ set (map (λv. m'(k ↦ v)) (V k))"
by simp
ultimately
have "m ∈ ?l"
using ‹dom m = set (k#ks)› by blast
}
ultimately
have "{Mapping.update k v m |v m. v ∈ set (V k) ∧ m ∈ {m. Mapping.keys m = set ks ∧ (∀k∈set ks. the (Mapping.lookup m k) ∈ set (V k))}}
= {m. Mapping.keys m = set (k # ks) ∧ (∀k∈set (k # ks). the (Mapping.lookup m k) ∈ set (V k))}"
by (transfer; blast)
thus ?case