# HG changeset patch
# User nipkow
# Date 1101058765 -3600
# Node ID 3514ca74ac541b19f64d7184884dec70ca594248
# Parent  eedbb8d22ca28b5fb7ff07ff8a02daae58550e35
Added more lemmas

diff -r eedbb8d22ca2 -r 3514ca74ac54 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 21 15:44:20 2004 +0100
+++ b/src/HOL/List.thy	Sun Nov 21 18:39:25 2004 +0100
@@ -1479,6 +1479,13 @@
 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
 by (induct xs) auto
 
+lemma distinct_map_filterI:
+ "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))"
+apply(induct xs)
+ apply simp
+apply force
+done
+
 text {*
 It is best to avoid this indexed version of distinct, but sometimes
 it is useful. *}
diff -r eedbb8d22ca2 -r 3514ca74ac54 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Nov 21 15:44:20 2004 +0100
+++ b/src/HOL/Map.thy	Sun Nov 21 18:39:25 2004 +0100
@@ -178,6 +178,35 @@
 
 subsection {* @{term map_of} *}
 
+lemma map_of_eq_None_iff:
+ "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
+by (induct xys) simp_all
+
+lemma map_of_is_SomeD:
+ "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
+apply(induct xys)
+ apply simp
+apply(clarsimp split:if_splits)
+done
+
+lemma map_of_eq_Some_iff[simp]:
+ "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
+apply(induct xys)
+ apply(simp)
+apply(auto simp:map_of_eq_None_iff[symmetric])
+done
+
+lemma Some_eq_map_of_iff[simp]:
+ "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
+by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
+
+lemma [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
+  \<Longrightarrow> map_of xys x = Some y"
+apply (induct xys)
+ apply simp
+apply force
+done
+
 lemma map_of_zip_is_None[simp]:
   "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
 by (induct rule:list_induct2, simp_all)
@@ -287,6 +316,10 @@
 done
 declare fun_upd_apply [simp]
 
+lemma inj_on_map_add_dom[iff]:
+ "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
+by(fastsimp simp add:map_add_def dom_def inj_on_def split:option.splits)
+
 subsection {* @{term restrict_map} *}
 
 lemma restrict_map_to_empty[simp]: "m\<lfloor>{} = empty"
@@ -442,6 +475,10 @@
 apply(auto simp del:fun_upd_apply)
 done
 
+lemma dom_map_of_conv_image_fst:
+  "dom(map_of xys) = fst ` (set xys)"
+by(force simp: dom_map_of)
+
 lemma dom_map_of_zip[simp]: "[| length xs = length ys; distinct xs |] ==>
   dom(map_of(zip xs ys)) = set xs"
 by(induct rule: list_induct2, simp_all)
@@ -526,6 +563,9 @@
 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   by (fastsimp simp add: map_le_def)
 
+lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
+by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
+
 lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
 by (fastsimp simp add: map_le_def map_add_def dom_def)