--- a/src/HOL/Map.thy Mon Jul 27 21:47:41 2009 +0200
+++ b/src/HOL/Map.thy Mon Jul 27 22:50:01 2009 +0200
@@ -307,6 +307,9 @@
lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
by (simp add: map_upds_def)
+lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
+by (rule ext) (auto simp: map_add_def dom_def split: option.split)
+
lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
unfolding map_add_def
apply (induct xs)
@@ -508,6 +511,12 @@
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 map_add_dom_app_simps:
+ "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+ "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+ "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
+by (auto simp add: map_add_def split: option.split_asm)
+
lemma dom_const [simp]:
"dom (\<lambda>x. Some y) = UNIV"
by auto