# HG changeset patch
# User haftmann
# Date 1232736708 -3600
# Node ID 2eeb09477ed3d6a9e3c3b3a02df14e8f07723492
# Parent  82054da94a74c96c1e264b0aa303ca7cca14cb47
lemmas dom_const, dom_if

diff -r 82054da94a74 -r 2eeb09477ed3 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jan 23 10:21:48 2009 +0100
+++ b/src/HOL/Map.thy	Fri Jan 23 19:51:48 2009 +0100
@@ -503,6 +503,15 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+lemma dom_const [simp]:
+  "dom (\<lambda>x. Some y) = UNIV"
+  by auto
+
+lemma dom_if:
+  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
+  by (auto split: if_splits)
+
+
 (* Due to John Matthews - could be rephrased with dom *)
 lemma finite_map_freshness:
   "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>