lemmas about dom and minus / insert

--- a/src/HOL/Map.thy	Fri Nov 14 08:50:07 2008 +0100
+++ b/src/HOL/Map.thy	Fri Nov 14 08:50:08 2008 +0100
@@ -509,6 +509,15 @@
    \<exists>x. f x = None"
 by(bestsimp dest:ex_new_if_finite)
 
+lemma dom_minus:
+  "f x = None \<Longrightarrow> dom f - insert x A = dom f - A"
+  unfolding dom_def by simp
+
+lemma insert_dom:
+  "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
+  unfolding dom_def by auto
+
+
 subsection {* @{term [source] ran} *}
 
 lemma ranI: "m a = Some b ==> b : ran m"