src/HOL/Map.thy
changeset 63828 ca467e73f912
parent 63648 f9f3006a5579
child 63834 6a757f36997e
     1.1 --- a/src/HOL/Map.thy	Thu Sep 08 18:18:57 2016 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Sep 09 13:39:21 2016 +0200
     1.3 @@ -688,6 +688,12 @@
     1.4  lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f ++ g \<subseteq>\<^sub>m h"
     1.5    by (auto simp: map_le_def map_add_def dom_def split: option.splits)
     1.6  
     1.7 +lemma map_add_subsumed1: "f \<subseteq>\<^sub>m g \<Longrightarrow> f++g = g"
     1.8 +by (simp add: map_add_le_mapI map_le_antisym)
     1.9 +
    1.10 +lemma map_add_subsumed2: "f \<subseteq>\<^sub>m g \<Longrightarrow> g++f = g"
    1.11 +by (metis map_add_subsumed1 map_le_iff_map_add_commute)
    1.12 +
    1.13  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
    1.14  proof(rule iffI)
    1.15    assume "\<exists>v. f = [x \<mapsto> v]"