1.1 --- a/src/HOL/Map.thy	Mon Jul 27 21:47:41 2009 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Jul 27 22:50:01 2009 +0200
     1.3 @@ -307,6 +307,9 @@
     1.4  lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
     1.5  by (simp add: map_upds_def)
     1.6  
     1.7 +lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
     1.8 +by (rule ext) (auto simp: map_add_def dom_def split: option.split)
     1.9 +
    1.10  lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
    1.11  unfolding map_add_def
    1.12  apply (induct xs)
    1.13 @@ -508,6 +511,12 @@
    1.14  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
    1.15  by (rule ext) (force simp: map_add_def dom_def split: option.split)
    1.16  
    1.17 +lemma map_add_dom_app_simps:
    1.18 +  "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
    1.19 +  "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
    1.20 +  "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
    1.21 +by (auto simp add: map_add_def split: option.split_asm)
    1.22 +
    1.23  lemma dom_const [simp]:
    1.24    "dom (\<lambda>x. Some y) = UNIV"
    1.25    by auto