Added a few lemmas about map_le
authorwebertj
Fri May 16 16:35:36 2003 +0200 (2003-05-16)
changeset 14033bc723de8ec95
parent 14032 a6239314e380
child 14034 55ba81e3502b
Added a few lemmas about map_le
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Thu May 15 11:22:54 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri May 16 16:35:36 2003 +0200
     1.3 @@ -370,4 +370,29 @@
     1.4   apply auto
     1.5  done
     1.6  
     1.7 +lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
     1.8 +  by (fastsimp simp add: map_le_def dom_def)
     1.9 +
    1.10 +lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
    1.11 +  by (simp add: map_le_def)
    1.12 +
    1.13 +lemma map_le_trans: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m h"
    1.14 +  apply (clarsimp simp add: map_le_def)
    1.15 +  apply (drule_tac x="a" in bspec, fastsimp)+
    1.16 +  apply assumption
    1.17 +done
    1.18 +
    1.19 +lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
    1.20 +  apply (unfold map_le_def)
    1.21 +  apply (rule ext)
    1.22 +  apply (case_tac "x \<in> dom f")
    1.23 +    apply simp
    1.24 +  apply (case_tac "x \<in> dom g")
    1.25 +    apply simp
    1.26 +  apply fastsimp
    1.27 +done
    1.28 +
    1.29 +lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
    1.30 +  by (fastsimp simp add: map_le_def)
    1.31 +
    1.32  end