# HG changeset patch
# User krauss
# Date 1248727801 -7200
# Node ID 0203e1006f1bc35344f92fdb020c9e1bd4660b92
# Parent  8f9b8d14fc9f06f21e31e2c0fca3a5f7046719c3
some lemmas about maps (contributed by Peter Lammich)

diff -r 8f9b8d14fc9f -r 0203e1006f1b src/HOL/Map.thy
--- 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