--- 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?]: