src/HOL/Map.thy
changeset 14033 bc723de8ec95
parent 14027 68d247b7b14b
child 14100 804be4c4b642
     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