Theory Map2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Auxiliary Map Facts›

theory Map2
  imports Main
begin 

lemma map_of_tabulate:  
  "map_of (map (λx. (x, f x)) xs) x ≠ None ⟷ x ∈ set xs"
  by (induct xs) auto

lemma map_of_tabulate_simp:
  "map_of (map (λx. (x, f x)) xs) x = (if x ∈ set xs then Some (f x) else None)"
  by (metis (mono_tags, lifting) comp_eq_dest_lhs map_of_map_restrict restrict_map_def)

lemma dom_map_update:
  "dom (m (k ↦ v)) = dom m ∪ {k}"
  by simp

lemma map_equal:
  "dom m = dom m' ⟹ (⋀x. x ∈ dom m ⟹ m x = m' x) ⟹ m = m'"
  by fastforce

lemma map_reduce:
  assumes "dom m = {a} ∪ B"
  shows "∃m'. dom m' = B ∧ (∀x ∈ B. m x = m' x)"
proof (cases "a ∈ B")
  case True
    thus ?thesis
      using assms by (metis insert_absorb insert_is_Un)
next
  case False
    with assms have "dom (m (a := None)) = B ∧ (∀x∈B. m x = (m (a := None)) x)"
      by simp
    thus ?thesis
      by blast
qed

end