# 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[\]ys)) = (m1++m2)(xs[\]ys)" by (simp add: map_upds_def) +lemma map_add_upd_left: "m\dom e2 \ e1(m \ u1) ++ e2 = (e1 ++ e2)(m \ 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 \ dom m2 = {} \ m1++m2 = m2++m1" by (rule ext) (force simp: map_add_def dom_def split: option.split) +lemma map_add_dom_app_simps: + "\ m\dom l2 \ \ (l1++l2) m = l2 m" + "\ m\dom l1 \ \ (l1++l2) m = l2 m" + "\ m\dom l2 \ \ (l1++l2) m = l1 m" +by (auto simp add: map_add_def split: option.split_asm) + lemma dom_const [simp]: "dom (\x. Some y) = UNIV" by auto