author | haftmann |

Thu Mar 27 19:04:37 2008 +0100 (2008-03-27) | |

changeset 26443 | cae9fa186541 |

parent 26442 | 57fb6a8b099e |

child 26444 | 6a5faa5bcf19 |

lemmas about map_of (zip _ _)

src/HOL/Map.thy | file | annotate | diff | revisions |

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)