# HG changeset patch
# User nipkow
# Date 1473421161 -7200
# Node ID ca467e73f9122f28d425ae94c0976127b20f943f
# Parent  b24d0e53dd03264047f99be86fed64673c44d36d
added lemmas

diff -r b24d0e53dd03 -r ca467e73f912 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Sep 08 18:18:57 2016 +0200
+++ b/src/HOL/Map.thy	Fri Sep 09 13:39:21 2016 +0200
@@ -688,6 +688,12 @@
 lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f ++ g \<subseteq>\<^sub>m h"
   by (auto simp: map_le_def map_add_def dom_def split: option.splits)
 
+lemma map_add_subsumed1: "f \<subseteq>\<^sub>m g \<Longrightarrow> f++g = g"
+by (simp add: map_add_le_mapI map_le_antisym)
+
+lemma map_add_subsumed2: "f \<subseteq>\<^sub>m g \<Longrightarrow> g++f = g"
+by (metis map_add_subsumed1 map_le_iff_map_add_commute)
+
 lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
 proof(rule iffI)
   assume "\<exists>v. f = [x \<mapsto> v]"