Added more lemmas
authornipkow
Sun Nov 21 18:39:25 2004 +0100 (2004-11-21)
changeset 153043514ca74ac54
parent 15303 eedbb8d22ca2
child 15305 0bd9eedaa301
Added more lemmas
src/HOL/List.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/List.thy	Sun Nov 21 15:44:20 2004 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Nov 21 18:39:25 2004 +0100
     1.3 @@ -1479,6 +1479,13 @@
     1.4  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
     1.5  by (induct xs) auto
     1.6  
     1.7 +lemma distinct_map_filterI:
     1.8 + "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))"
     1.9 +apply(induct xs)
    1.10 + apply simp
    1.11 +apply force
    1.12 +done
    1.13 +
    1.14  text {*
    1.15  It is best to avoid this indexed version of distinct, but sometimes
    1.16  it is useful. *}
     2.1 --- a/src/HOL/Map.thy	Sun Nov 21 15:44:20 2004 +0100
     2.2 +++ b/src/HOL/Map.thy	Sun Nov 21 18:39:25 2004 +0100
     2.3 @@ -178,6 +178,35 @@
     2.4  
     2.5  subsection {* @{term map_of} *}
     2.6  
     2.7 +lemma map_of_eq_None_iff:
     2.8 + "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
     2.9 +by (induct xys) simp_all
    2.10 +
    2.11 +lemma map_of_is_SomeD:
    2.12 + "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
    2.13 +apply(induct xys)
    2.14 + apply simp
    2.15 +apply(clarsimp split:if_splits)
    2.16 +done
    2.17 +
    2.18 +lemma map_of_eq_Some_iff[simp]:
    2.19 + "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
    2.20 +apply(induct xys)
    2.21 + apply(simp)
    2.22 +apply(auto simp:map_of_eq_None_iff[symmetric])
    2.23 +done
    2.24 +
    2.25 +lemma Some_eq_map_of_iff[simp]:
    2.26 + "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
    2.27 +by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
    2.28 +
    2.29 +lemma [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
    2.30 +  \<Longrightarrow> map_of xys x = Some y"
    2.31 +apply (induct xys)
    2.32 + apply simp
    2.33 +apply force
    2.34 +done
    2.35 +
    2.36  lemma map_of_zip_is_None[simp]:
    2.37    "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
    2.38  by (induct rule:list_induct2, simp_all)
    2.39 @@ -287,6 +316,10 @@
    2.40  done
    2.41  declare fun_upd_apply [simp]
    2.42  
    2.43 +lemma inj_on_map_add_dom[iff]:
    2.44 + "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
    2.45 +by(fastsimp simp add:map_add_def dom_def inj_on_def split:option.splits)
    2.46 +
    2.47  subsection {* @{term restrict_map} *}
    2.48  
    2.49  lemma restrict_map_to_empty[simp]: "m\<lfloor>{} = empty"
    2.50 @@ -442,6 +475,10 @@
    2.51  apply(auto simp del:fun_upd_apply)
    2.52  done
    2.53  
    2.54 +lemma dom_map_of_conv_image_fst:
    2.55 +  "dom(map_of xys) = fst ` (set xys)"
    2.56 +by(force simp: dom_map_of)
    2.57 +
    2.58  lemma dom_map_of_zip[simp]: "[| length xs = length ys; distinct xs |] ==>
    2.59    dom(map_of(zip xs ys)) = set xs"
    2.60  by(induct rule: list_induct2, simp_all)
    2.61 @@ -526,6 +563,9 @@
    2.62  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
    2.63    by (fastsimp simp add: map_le_def)
    2.64  
    2.65 +lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
    2.66 +by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
    2.67 +
    2.68  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
    2.69  by (fastsimp simp add: map_le_def map_add_def dom_def)
    2.70