lemma restrict_complement_singleton_eq

--- a/src/HOL/Map.thy	Sat Mar 06 15:31:30 2010 +0100
+++ b/src/HOL/Map.thy	Sat Mar 06 15:31:31 2010 +0100
@@ -398,6 +398,10 @@
   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
 
+lemma restrict_complement_singleton_eq:
+  "f |` (- {x}) = f(x := None)"
+  by (simp add: restrict_map_def expand_fun_eq)
+
 
 subsection {* @{term [source] map_upds} *}
 
@@ -707,4 +711,3 @@
 qed
 
 end
-