Theory Mapping2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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" 
  by (simp add: lookup_tabulate)

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
      by (simp add: Cons)
qed (force simp add: keys_empty_iff_map_empty)

end