merged

--- a/src/HOL/Library/Mapping.thy	Sat Feb 07 09:25:59 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Sat Feb 07 09:58:24 2009 +0100
@@ -39,6 +39,9 @@
 definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
   "tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
 
+definition bulkload :: "'a list \<Rightarrow> (nat, 'a) map" where
+  "bulkload xs = Map (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
+
 
 subsection {* Properties *}
 
@@ -63,6 +66,10 @@
   "lookup (tabulate ks f) = (Some o f) |` set ks"
   by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
 
+lemma lookup_bulkload:
+  "lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
+  unfolding bulkload_def by simp
+
 lemma update_update:
   "update k v (update k w m) = update k v m"
   "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
@@ -120,4 +127,16 @@
   "size (tabulate ks f) = length (remdups ks)"
   by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
 
+lemma bulkload_tabulate: (*FIXME Isar proof*)
+  "bulkload xs = tabulate [0..<length xs] (nth xs)"
+  unfolding bulkload_def tabulate_def apply simp
+  apply (rule sym)
+  apply (rule ext) apply auto
+  apply (subst map_of_eq_Some_iff)
+  apply (simp add: map_compose [symmetric] comp_def)
+  apply (simp add: image_def)
+  apply (subst map_of_eq_None_iff)
+  apply (simp add: image_def)
+  done
+
 end
\ No newline at end of file

--- a/src/HOL/List.thy	Sat Feb 07 09:25:59 2009 +0100
+++ b/src/HOL/List.thy	Sat Feb 07 09:58:24 2009 +0100
@@ -1215,10 +1215,10 @@
 
 subsubsection {* @{text nth} *}
 
-lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
+lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
 by auto
 
-lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
+lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
 by auto
 
 declare nth.simps [simp del]
@@ -1375,6 +1375,12 @@
 apply auto
 done
 
+lemma list_update_code [code]:
+  "[][i := y] = []"
+  "(x # xs)[0 := y] = y # xs"
+  "(x # xs)[Suc i := y] = x # xs[i := y]"
+  by simp_all
+
 
 subsubsection {* @{text last} and @{text butlast} *}
 
@@ -1846,6 +1852,15 @@
   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
 by(blast dest: set_zip_leftD set_zip_rightD)
 
+lemma zip_map_fst_snd:
+  "zip (map fst zs) (map snd zs) = zs"
+  by (induct zs) simp_all
+
+lemma zip_eq_conv:
+  "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
+  by (auto simp add: zip_map_fst_snd)
+
+
 subsubsection {* @{text list_all2} *}
 
 lemma list_all2_lengthD [intro?]: