# HG changeset patch
# User haftmann
# Date 1258035024 -3600
# Node ID dcaada178c6f8012aa6a3d8e4358af195aa92a58
# Parent  bfee47887ca31e01b47e6341ae352b9d807e2314
moved lemma map_of_zip_map to Map.thy

diff -r bfee47887ca3 -r dcaada178c6f src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Wed Nov 11 21:53:58 2009 +0100
+++ b/src/HOL/Library/Enum.thy	Thu Nov 12 15:10:24 2009 +0100
@@ -10,7 +10,7 @@
 
 class enum =
   fixes enum :: "'a list"
-  assumes UNIV_enum [code]: "UNIV = set enum"
+  assumes UNIV_enum: "UNIV = set enum"
     and enum_distinct: "distinct enum"
 begin
 
@@ -114,10 +114,6 @@
     by (simp add: length_n_lists)
 qed
 
-lemma map_of_zip_map: (*FIXME move to Map.thy*)
-  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
-  by (induct xs) (simp_all add: expand_fun_eq)
-
 lemma map_of_zip_enum_is_Some:
   assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
diff -r bfee47887ca3 -r dcaada178c6f src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Nov 11 21:53:58 2009 +0100
+++ b/src/HOL/Map.thy	Thu Nov 12 15:10:24 2009 +0100
@@ -218,6 +218,10 @@
   ultimately show ?case by simp
 qed
 
+lemma map_of_zip_map:
+  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
+  by (induct xs) (simp_all add: expand_fun_eq)
+
 lemma finite_range_map_of: "finite (range (map_of xys))"
 apply (induct xys)
  apply (simp_all add: image_constant)