src/HOL/Map.thy
changeset 33635 dcaada178c6f
parent 32236 0203e1006f1b
child 34941 156925dd67af
     1.1 --- a/src/HOL/Map.thy	Wed Nov 11 21:53:58 2009 +0100
     1.2 +++ b/src/HOL/Map.thy	Thu Nov 12 15:10:24 2009 +0100
     1.3 @@ -218,6 +218,10 @@
     1.4    ultimately show ?case by simp
     1.5  qed
     1.6  
     1.7 +lemma map_of_zip_map:
     1.8 +  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
     1.9 +  by (induct xs) (simp_all add: expand_fun_eq)
    1.10 +
    1.11  lemma finite_range_map_of: "finite (range (map_of xys))"
    1.12  apply (induct xys)
    1.13   apply (simp_all add: image_constant)