moved lemma map_of_zip_map to Map.thy
authorhaftmann
Thu Nov 12 15:10:24 2009 +0100 (2009-11-12)
changeset 33635dcaada178c6f
parent 33617 bfee47887ca3
child 33636 a9bb3f063773
moved lemma map_of_zip_map to Map.thy
src/HOL/Library/Enum.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Library/Enum.thy	Wed Nov 11 21:53:58 2009 +0100
     1.2 +++ b/src/HOL/Library/Enum.thy	Thu Nov 12 15:10:24 2009 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  class enum =
     1.6    fixes enum :: "'a list"
     1.7 -  assumes UNIV_enum [code]: "UNIV = set enum"
     1.8 +  assumes UNIV_enum: "UNIV = set enum"
     1.9      and enum_distinct: "distinct enum"
    1.10  begin
    1.11  
    1.12 @@ -114,10 +114,6 @@
    1.13      by (simp add: length_n_lists)
    1.14  qed
    1.15  
    1.16 -lemma map_of_zip_map: (*FIXME move to Map.thy*)
    1.17 -  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
    1.18 -  by (induct xs) (simp_all add: expand_fun_eq)
    1.19 -
    1.20  lemma map_of_zip_enum_is_Some:
    1.21    assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
    1.22    shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
     2.1 --- a/src/HOL/Map.thy	Wed Nov 11 21:53:58 2009 +0100
     2.2 +++ b/src/HOL/Map.thy	Thu Nov 12 15:10:24 2009 +0100
     2.3 @@ -218,6 +218,10 @@
     2.4    ultimately show ?case by simp
     2.5  qed
     2.6  
     2.7 +lemma map_of_zip_map:
     2.8 +  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
     2.9 +  by (induct xs) (simp_all add: expand_fun_eq)
    2.10 +
    2.11  lemma finite_range_map_of: "finite (range (map_of xys))"
    2.12  apply (induct xys)
    2.13   apply (simp_all add: image_constant)