src/HOL/Map.thy
 changeset 26443 cae9fa186541 parent 25965 05df64f786a4 child 28562 4e74209f113e
```     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)