--- a/NEWS Mon Feb 13 19:40:38 2023 +0100
+++ b/NEWS Tue Feb 14 09:36:35 2023 +0100
@@ -43,6 +43,8 @@
*** HOL ***
+* Map.map_of and lemmas moved to List.
+
* Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings";
"euclidean division" typically denotes a particular division on
integers. Minor INCOMPATIBILITY.
--- a/src/Doc/Main/Main_Doc.thy Mon Feb 13 19:40:38 2023 +0100
+++ b/src/Doc/Main/Main_Doc.thy Tue Feb 14 09:36:35 2023 +0100
@@ -543,6 +543,7 @@
\<^const>\<open>List.list_all2\<close> & \<^typeof>\<open>List.list_all2\<close>\\
\<^const>\<open>List.list_update\<close> & \<^typeof>\<open>List.list_update\<close>\\
\<^const>\<open>List.map\<close> & \<^typeof>\<open>List.map\<close>\\
+\<^const>\<open>List.map_of\<close> & \<^typeof>\<open>List.map_of\<close>\\
\<^const>\<open>List.measures\<close> & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
\<^const>\<open>List.nth\<close> & \<^typeof>\<open>List.nth\<close>\\
\<^const>\<open>List.nths\<close> & \<^typeof>\<open>List.nths\<close>\\
@@ -585,32 +586,31 @@
qualifier \<open>q\<^sub>i\<close> is either a generator \mbox{\<open>pat \<leftarrow> e\<close>} or a
guard, i.e.\ boolean expression.
-\section*{Map}
-
-Maps model partial functions and are often used as finite tables. However,
-the domain of a map may be infinite.
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\<^const>\<open>Map.empty\<close> & \<^typeof>\<open>Map.empty\<close>\\
-\<^const>\<open>Map.map_add\<close> & \<^typeof>\<open>Map.map_add\<close>\\
-\<^const>\<open>Map.map_comp\<close> & \<^typeof>\<open>Map.map_comp\<close>\\
-\<^const>\<open>Map.restrict_map\<close> & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\
-\<^const>\<open>Map.dom\<close> & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
-\<^const>\<open>Map.ran\<close> & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\
-\<^const>\<open>Map.map_le\<close> & \<^typeof>\<open>Map.map_le\<close>\\
-\<^const>\<open>Map.map_of\<close> & \<^typeof>\<open>Map.map_of\<close>\\
-\<^const>\<open>Map.map_upds\<close> & \<^typeof>\<open>Map.map_upds\<close>\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\<^term>\<open>Map.empty\<close> & @{term[source] "\<lambda>_. None"}\\
-\<^term>\<open>m(x:=Some y)\<close> & @{term[source]"m(x:=Some y)"}\\
-\<open>m(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)\<close> & @{text[source]"m(x\<^sub>1\<mapsto>y\<^sub>1)\<dots>(x\<^sub>n\<mapsto>y\<^sub>n)"}\\
-\<open>[x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n]\<close> & @{text[source]"Map.empty(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"}\\
-\<^term>\<open>map_upds m xs ys\<close> & @{term[source]"map_upds m xs ys"}\\
-\end{tabular}
+%\section*{Map}
+%
+%Maps model partial functions and are often used as finite tables. However,
+%the domain of a map may be infinite.
+%
+%\begin{tabular}{@ {} l @ {~::~} l @ {}}
+%\<const>\<open>Map.empty\<close> & \<typeof>\<open>Map.empty\<close>\\
+%\<const>\<open>Map.map_add\<close> & \<typeof>\<open>Map.map_add\<close>\\
+%\<const>\<open>Map.map_comp\<close> & \<typeof>\<open>Map.map_comp\<close>\\
+%\<const>\<open>Map.restrict_map\<close> & @ {term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\
+%\<const>\<open>Map.dom\<close> & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
+%\<const>\<open>Map.ran\<close> & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\
+%\<const>\<open>Map.map_le\<close> & \<typeof>\<open>Map.map_le\<close>\\
+%\<const>\<open>Map.map_upds\<close> & \<typeof>\<open>Map.map_upds\<close>\\
+%\end{tabular}
+%
+%\subsubsection*{Syntax}
+%
+%\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+%\<term>\<open>Map.empty\<close> & @ {term[source] "\<lambda>_. None"}\\
+%\<term>\<open>m(x:=Some y)\<close> & @ {term[source]"m(x:=Some y)"}\\
+%m(x1\<mapsto>y1,\<dots>,xn\<mapsto>yn) & @ {text[source]"m(x1\<mapsto>y1)\<dots>(xn\<mapsto>yn)"}\\
+%[x1\<mapsto>y1,\<dots>,xn\<mapsto>yn] & @ {text[source]"Map.empty(x1\<mapsto>y1,\<dots>,xn\<mapsto>yn)"}\\
+%\<term>\<open>map_upds m xs ys\<close> & @ {term[source]"map_upds m xs ys"}\\
+%\end{tabular}
\section*{Infix operators in Main} % \<^theory>\<open>Main\<close>
--- a/src/HOL/Data_Structures/Trie_Map.thy Mon Feb 13 19:40:38 2023 +0100
+++ b/src/HOL/Data_Structures/Trie_Map.thy Tue Feb 14 09:36:35 2023 +0100
@@ -6,14 +6,31 @@
Trie_Fun
begin
-text \<open>An implementation of tries based on maps implemented by red-black trees.
-Works for any kind of search tree.\<close>
+text \<open>An implementation of tries for an arbitrary alphabet \<open>'a\<close> where
+the mapping from an element of type \<open>'a\<close> to the sub-trie is implemented by a binary search tree.
+Although this implementation uses maps implemented by red-black trees it works for any
+implementation of maps.
+
+This is an implementation of the ``ternary search trees'' by Bentley and Sedgewick
+[SODA 1997, Dr. Dobbs 1998]. The name derives from the fact that a node in the BST can now
+be drawn to have 3 children, where the middle child is the sub-trie that the node maps
+its key to. Hence the name \<open>trie3\<close>.
+
+Example from @{url "https://en.wikipedia.org/wiki/Ternary_search_tree#Description"}:
-text \<open>Implementation of map:\<close>
+ c
+ / | \
+ a u h
+ | | | \
+ t. t e. u
+ / / | / |
+ s. p. e. i. s.
-type_synonym 'a mapi = "'a rbt"
+Characters with a dot are final.
+Thus the tree represents the set of strings "cute","cup","at","as","he","us" and "i".
+\<close>
-datatype 'a trie_map = Nd bool "('a * 'a trie_map) mapi"
+datatype 'a trie3 = Nd3 bool "('a * 'a trie3) rbt"
text \<open>In principle one should be able to given an implementation of tries
once and for all for any map implementation and not just for a specific one (RBT) as done here.
@@ -21,89 +38,90 @@
However, the development below works verbatim for any map implementation, eg \<open>Tree_Map\<close>,
and not just \<open>RBT_Map\<close>, except for the termination lemma \<open>lookup_size\<close>.\<close>
+
term size_tree
lemma lookup_size[termination_simp]:
- fixes t :: "('a::linorder * 'a trie_map) rbt"
+ fixes t :: "('a::linorder * 'a trie3) rbt"
shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc(Suc (size (snd(fst ab))))) t)"
apply(induction t a rule: lookup.induct)
apply(auto split: if_splits)
done
-definition empty :: "'a trie_map" where
-[simp]: "empty = Nd False Leaf"
+definition empty3 :: "'a trie3" where
+[simp]: "empty3 = Nd3 False Leaf"
-fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where
-"isin (Nd b m) [] = b" |
-"isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
+fun isin3 :: "('a::linorder) trie3 \<Rightarrow> 'a list \<Rightarrow> bool" where
+"isin3 (Nd3 b m) [] = b" |
+"isin3 (Nd3 b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin3 t xs)"
-fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
-"insert [] (Nd b m) = Nd True m" |
-"insert (x#xs) (Nd b m) =
- Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> empty | Some t \<Rightarrow> t)) m)"
+fun insert3 :: "('a::linorder) list \<Rightarrow> 'a trie3 \<Rightarrow> 'a trie3" where
+"insert3 [] (Nd3 b m) = Nd3 True m" |
+"insert3 (x#xs) (Nd3 b m) =
+ Nd3 b (update x (insert3 xs (case lookup m x of None \<Rightarrow> empty3 | Some t \<Rightarrow> t)) m)"
-fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
-"delete [] (Nd b m) = Nd False m" |
-"delete (x#xs) (Nd b m) = Nd b
+fun delete3 :: "('a::linorder) list \<Rightarrow> 'a trie3 \<Rightarrow> 'a trie3" where
+"delete3 [] (Nd3 b m) = Nd3 False m" |
+"delete3 (x#xs) (Nd3 b m) = Nd3 b
(case lookup m x of
None \<Rightarrow> m |
- Some t \<Rightarrow> update x (delete xs t) m)"
+ Some t \<Rightarrow> update x (delete3 xs t) m)"
subsection "Correctness"
-text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close>
+text \<open>Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\<close>
-fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where
-"abs (Nd b t) = Trie_Fun.Nd b (\<lambda>a. map_option abs (lookup t a))"
+fun abs3 :: "'a::linorder trie3 \<Rightarrow> 'a trie" where
+"abs3 (Nd3 b t) = Nd b (\<lambda>a. map_option abs3 (lookup t a))"
-fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where
-"invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))"
+fun invar3 :: "('a::linorder)trie3 \<Rightarrow> bool" where
+"invar3 (Nd3 b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar3 t))"
-lemma isin_abs: "isin t xs = Trie_Fun.isin (abs t) xs"
-apply(induction t xs rule: isin.induct)
+lemma isin_abs3: "isin3 t xs = isin (abs3 t) xs"
+apply(induction t xs rule: isin3.induct)
apply(auto split: option.split)
done
-lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun.insert xs (abs t)"
-apply(induction xs t rule: insert.induct)
+lemma abs3_insert3: "invar3 t \<Longrightarrow> abs3(insert3 xs t) = insert xs (abs3 t)"
+apply(induction xs t rule: insert3.induct)
apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split)
done
-lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun.delete xs (abs t)"
-apply(induction xs t rule: delete.induct)
+lemma abs3_delete3: "invar3 t \<Longrightarrow> abs3(delete3 xs t) = delete xs (abs3 t)"
+apply(induction xs t rule: delete3.induct)
apply(auto simp: M.map_specs split: option.split)
done
-lemma invar_insert: "invar t \<Longrightarrow> invar (insert xs t)"
-apply(induction xs t rule: insert.induct)
+lemma invar3_insert3: "invar3 t \<Longrightarrow> invar3 (insert3 xs t)"
+apply(induction xs t rule: insert3.induct)
apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split)
done
-lemma invar_delete: "invar t \<Longrightarrow> invar (delete xs t)"
-apply(induction xs t rule: delete.induct)
+lemma invar3_delete3: "invar3 t \<Longrightarrow> invar3 (delete3 xs t)"
+apply(induction xs t rule: delete3.induct)
apply(auto simp: M.map_specs split: option.split)
done
text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>
interpretation S2: Set
-where empty = empty and isin = isin and insert = insert and delete = delete
-and set = "set o abs" and invar = invar
+where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3
+and set = "set o abs3" and invar = invar3
proof (standard, goal_cases)
case 1 show ?case by (simp add: isin_case split: list.split)
next
- case 2 thus ?case by (simp add: isin_abs)
+ case 2 thus ?case by (simp add: isin_abs3)
next
- case 3 thus ?case by (simp add: set_insert abs_insert del: set_def)
+ case 3 thus ?case by (simp add: set_insert abs3_insert3 del: set_def)
next
- case 4 thus ?case by (simp add: set_delete abs_delete del: set_def)
+ case 4 thus ?case by (simp add: set_delete abs3_delete3 del: set_def)
next
case 5 thus ?case by (simp add: M.map_specs RBT_Set.empty_def[symmetric])
next
- case 6 thus ?case by (simp add: invar_insert)
+ case 6 thus ?case by (simp add: invar3_insert3)
next
- case 7 thus ?case by (simp add: invar_delete)
+ case 7 thus ?case by (simp add: invar3_delete3)
qed
--- a/src/HOL/List.thy Mon Feb 13 19:40:38 2023 +0100
+++ b/src/HOL/List.thy Tue Feb 14 09:36:35 2023 +0100
@@ -243,6 +243,11 @@
abbreviation length :: "'a list \<Rightarrow> nat" where
"length \<equiv> size"
+primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option"
+where
+ "map_of [] = (\<lambda>x. None)"
+| "map_of (p # ps) = (map_of ps)(fst p := Some(snd p))"
+
definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"
@@ -4681,6 +4686,126 @@
by (subst foldr_fold [symmetric]) simp_all
+subsubsection \<open>\<^const>\<open>map_of\<close>\<close>
+
+lemma map_of_eq_None_iff:
+ "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
+by (induct xys) simp_all
+
+lemma map_of_eq_Some_iff [simp]:
+ "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
+proof (induct xys)
+ case (Cons xy xys)
+ then show ?case
+ by (cases xy) (auto simp flip: map_of_eq_None_iff)
+qed auto
+
+lemma Some_eq_map_of_iff [simp]:
+ "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
+by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
+
+lemma map_of_is_SomeI [simp]:
+ "\<lbrakk>distinct(map fst xys); (x,y) \<in> set xys\<rbrakk> \<Longrightarrow> map_of xys x = Some y"
+ by simp
+
+lemma map_of_zip_is_None [simp]:
+ "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
+by (induct rule: list_induct2) simp_all
+
+lemma map_of_zip_is_Some:
+ assumes "length xs = length ys"
+ shows "x \<in> set xs \<longleftrightarrow> (\<exists>y. map_of (zip xs ys) x = Some y)"
+using assms by (induct rule: list_induct2) simp_all
+
+lemma map_of_zip_upd:
+ fixes x :: 'a and xs :: "'a list" and ys zs :: "'b list"
+ assumes "length ys = length xs"
+ and "length zs = length xs"
+ and "x \<notin> set xs"
+ and "(map_of (zip xs ys))(x := Some y) = (map_of (zip xs zs))(x := Some z)"
+ shows "map_of (zip xs ys) = map_of (zip xs zs)"
+proof
+ fix x' :: 'a
+ show "map_of (zip xs ys) x' = map_of (zip xs zs) x'"
+ proof (cases "x = x'")
+ case True
+ from assms True map_of_zip_is_None [of xs ys x']
+ have "map_of (zip xs ys) x' = None" by simp
+ moreover from assms True map_of_zip_is_None [of xs zs x']
+ have "map_of (zip xs zs) x' = None" by simp
+ ultimately show ?thesis by simp
+ next
+ case False from assms
+ have "((map_of (zip xs ys))(x := Some y)) x' = ((map_of (zip xs zs))(x := Some z)) x'" by auto
+ with False show ?thesis by simp
+ qed
+qed
+
+lemma map_of_zip_inject:
+ assumes "length ys = length xs"
+ and "length zs = length xs"
+ and dist: "distinct xs"
+ and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
+ shows "ys = zs"
+ using assms(1) assms(2)[symmetric]
+ using dist map_of
+proof (induct ys xs zs rule: list_induct3)
+ case Nil show ?case by simp
+next
+ case (Cons y ys x xs z zs)
+ from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
+ have map_of: "(map_of (zip xs ys))(x := Some y) = (map_of (zip xs zs))(x := Some z)" by simp
+ from Cons have "length ys = length xs" and "length zs = length xs"
+ and "x \<notin> set xs" by simp_all
+ then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
+ with Cons.hyps \<open>distinct (x # xs)\<close> have "ys = zs" by simp
+ moreover have "y = z" using fun_upd_eqD[OF map_of] by simp
+ ultimately show ?case by simp
+qed
+
+lemma map_of_zip_nth:
+ assumes "length xs = length ys"
+ assumes "distinct xs"
+ assumes "i < length ys"
+ shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
+using assms proof (induct arbitrary: i rule: list_induct2)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons x xs y ys)
+ then show ?case
+ using less_Suc_eq_0_disj by auto
+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: fun_eq_iff)
+
+lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
+ by (induct xs) (auto split: if_splits)
+
+lemma map_of_mapk_SomeI:
+ "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
+ map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
+by (induct t) (auto simp: inj_eq)
+
+lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
+by (induct l) auto
+
+lemma map_of_filter_in:
+ "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
+by (induct xs) auto
+
+lemma map_of_map:
+ "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
+ by (induct xs) (auto simp: fun_eq_iff)
+
+lemma map_of_Cons_code [code]:
+ "map_of [] k = None"
+ "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
+ by simp_all
+
+
subsubsection \<open>\<^const>\<open>enumerate\<close>\<close>
lemma enumerate_simps [simp, code]:
--- a/src/HOL/Map.thy Mon Feb 13 19:40:38 2023 +0100
+++ b/src/HOL/Map.thy Tue Feb 14 09:36:35 2023 +0100
@@ -70,21 +70,11 @@
"_Map (_Maplets ms1 ms2)" \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
"_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
-primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b"
-where
- "map_of [] = empty"
-| "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
-
definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b"
where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
translations
"_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
-lemma map_of_Cons_code [code]:
- "map_of [] k = None"
- "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
- by simp_all
-
subsection \<open>@{term [source] empty}\<close>
@@ -142,99 +132,6 @@
"empty = map_of xys \<longleftrightarrow> xys = []"
by(subst eq_commute) simp
-lemma map_of_eq_None_iff:
- "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
-by (induct xys) simp_all
-
-lemma map_of_eq_Some_iff [simp]:
- "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
-proof (induct xys)
- case (Cons xy xys)
- then show ?case
- by (cases xy) (auto simp flip: map_of_eq_None_iff)
-qed auto
-
-lemma Some_eq_map_of_iff [simp]:
- "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
-by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
-
-lemma map_of_is_SomeI [simp]:
- "\<lbrakk>distinct(map fst xys); (x,y) \<in> set xys\<rbrakk> \<Longrightarrow> map_of xys x = Some y"
- by simp
-
-lemma map_of_zip_is_None [simp]:
- "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
-by (induct rule: list_induct2) simp_all
-
-lemma map_of_zip_is_Some:
- assumes "length xs = length ys"
- shows "x \<in> set xs \<longleftrightarrow> (\<exists>y. map_of (zip xs ys) x = Some y)"
-using assms by (induct rule: list_induct2) simp_all
-
-lemma map_of_zip_upd:
- fixes x :: 'a and xs :: "'a list" and ys zs :: "'b list"
- assumes "length ys = length xs"
- and "length zs = length xs"
- and "x \<notin> set xs"
- and "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)"
- shows "map_of (zip xs ys) = map_of (zip xs zs)"
-proof
- fix x' :: 'a
- show "map_of (zip xs ys) x' = map_of (zip xs zs) x'"
- proof (cases "x = x'")
- case True
- from assms True map_of_zip_is_None [of xs ys x']
- have "map_of (zip xs ys) x' = None" by simp
- moreover from assms True map_of_zip_is_None [of xs zs x']
- have "map_of (zip xs zs) x' = None" by simp
- ultimately show ?thesis by simp
- next
- case False from assms
- have "(map_of (zip xs ys)(x \<mapsto> y)) x' = (map_of (zip xs zs)(x \<mapsto> z)) x'" by auto
- with False show ?thesis by simp
- qed
-qed
-
-lemma map_of_zip_inject:
- assumes "length ys = length xs"
- and "length zs = length xs"
- and dist: "distinct xs"
- and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
- shows "ys = zs"
- using assms(1) assms(2)[symmetric]
- using dist map_of
-proof (induct ys xs zs rule: list_induct3)
- case Nil show ?case by simp
-next
- case (Cons y ys x xs z zs)
- from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
- have map_of: "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)" by simp
- from Cons have "length ys = length xs" and "length zs = length xs"
- and "x \<notin> set xs" by simp_all
- then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
- with Cons.hyps \<open>distinct (x # xs)\<close> have "ys = zs" by simp
- moreover from map_of have "y = z" by (rule map_upd_eqD1)
- ultimately show ?case by simp
-qed
-
-lemma map_of_zip_nth:
- assumes "length xs = length ys"
- assumes "distinct xs"
- assumes "i < length ys"
- shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
-using assms proof (induct arbitrary: i rule: list_induct2)
- case Nil
- then show ?case by simp
-next
- case (Cons x xs y ys)
- then show ?case
- using less_Suc_eq_0_disj by auto
-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: fun_eq_iff)
-
lemma finite_range_map_of: "finite (range (map_of xys))"
proof (induct xys)
case (Cons a xys)
@@ -242,25 +139,6 @@
using finite_range_updI by fastforce
qed auto
-lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
- by (induct xs) (auto split: if_splits)
-
-lemma map_of_mapk_SomeI:
- "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
- map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
-by (induct t) (auto simp: inj_eq)
-
-lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
-by (induct l) auto
-
-lemma map_of_filter_in:
- "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
-by (induct xs) auto
-
-lemma map_of_map:
- "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
- by (induct xs) (auto simp: fun_eq_iff)
-
lemma dom_map_option:
"dom (\<lambda>k. map_option (f k) (m k)) = dom m"
by (simp add: dom_def)