lemmas about map_of (zip _ _)
authorhaftmann
Thu Mar 27 19:04:37 2008 +0100 (2008-03-27)
changeset 26443cae9fa186541
parent 26442 57fb6a8b099e
child 26444 6a5faa5bcf19
lemmas about map_of (zip _ _)
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Thu Mar 27 19:04:36 2008 +0100
     1.2 +++ b/src/HOL/Map.thy	Thu Mar 27 19:04:37 2008 +0100
     1.3 @@ -170,6 +170,55 @@
     1.4    "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
     1.5  by (induct rule: list_induct2) simp_all
     1.6  
     1.7 +lemma map_of_zip_is_Some:
     1.8 +  assumes "length xs = length ys"
     1.9 +  shows "x \<in> set xs \<longleftrightarrow> (\<exists>y. map_of (zip xs ys) x = Some y)"
    1.10 +using assms by (induct rule: list_induct2) simp_all
    1.11 +
    1.12 +lemma map_of_zip_upd:
    1.13 +  fixes x :: 'a and xs :: "'a list" and ys zs :: "'b list"
    1.14 +  assumes "length ys = length xs"
    1.15 +    and "length zs = length xs"
    1.16 +    and "x \<notin> set xs"
    1.17 +    and "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)"
    1.18 +  shows "map_of (zip xs ys) = map_of (zip xs zs)"
    1.19 +proof
    1.20 +  fix x' :: 'a
    1.21 +  show "map_of (zip xs ys) x' = map_of (zip xs zs) x'"
    1.22 +  proof (cases "x = x'")
    1.23 +    case True
    1.24 +    from assms True map_of_zip_is_None [of xs ys x']
    1.25 +      have "map_of (zip xs ys) x' = None" by simp
    1.26 +    moreover from assms True map_of_zip_is_None [of xs zs x']
    1.27 +      have "map_of (zip xs zs) x' = None" by simp
    1.28 +    ultimately show ?thesis by simp
    1.29 +  next
    1.30 +    case False from assms
    1.31 +      have "(map_of (zip xs ys)(x \<mapsto> y)) x' = (map_of (zip xs zs)(x \<mapsto> z)) x'" by auto
    1.32 +    with False show ?thesis by simp
    1.33 +  qed
    1.34 +qed
    1.35 +
    1.36 +lemma map_of_zip_inject:
    1.37 +  assumes "length ys = length xs"
    1.38 +    and "length zs = length xs"
    1.39 +    and dist: "distinct xs"
    1.40 +    and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
    1.41 +  shows "ys = zs"
    1.42 +using assms(1) assms(2)[symmetric] using dist map_of proof (induct ys xs zs rule: list_induct3)
    1.43 +  case Nil show ?case by simp
    1.44 +next
    1.45 +  case (Cons y ys x xs z zs)
    1.46 +  from `map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))`
    1.47 +    have map_of: "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)" by simp
    1.48 +  from Cons have "length ys = length xs" and "length zs = length xs"
    1.49 +    and "x \<notin> set xs" by simp_all
    1.50 +  then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
    1.51 +  with Cons.hyps `distinct (x # xs)` have "ys = zs" by simp
    1.52 +  moreover from map_of have "y = z" by (rule map_upd_eqD1)
    1.53 +  ultimately show ?case by simp
    1.54 +qed
    1.55 +
    1.56  lemma finite_range_map_of: "finite (range (map_of xys))"
    1.57  apply (induct xys)
    1.58   apply (simp_all add: image_constant)