# HG changeset patch
# User webertj
# Date 1053095736 -7200
# Node ID bc723de8ec958250422b7c2969ab8d2443cabeb0
# Parent  a6239314e38057aa68ffad83cdb143c4fb707a17
Added a few lemmas about map_le

diff -r a6239314e380 -r bc723de8ec95 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu May 15 11:22:54 2003 +0200
+++ b/src/HOL/Map.thy	Fri May 16 16:35:36 2003 +0200
@@ -370,4 +370,29 @@
  apply auto
 done
 
+lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
+  by (fastsimp simp add: map_le_def dom_def)
+
+lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
+  by (simp add: map_le_def)
+
+lemma map_le_trans: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m h"
+  apply (clarsimp simp add: map_le_def)
+  apply (drule_tac x="a" in bspec, fastsimp)+
+  apply assumption
+done
+
+lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
+  apply (unfold map_le_def)
+  apply (rule ext)
+  apply (case_tac "x \<in> dom f")
+    apply simp
+  apply (case_tac "x \<in> dom g")
+    apply simp
+  apply fastsimp
+done
+
+lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
+  by (fastsimp simp add: map_le_def)
+
 end