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