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  (xB. m x = (m (a := None)) x)"
      by simp
    thus ?thesis
      by blast
qed

end