# HG changeset patch
# User nipkow
# Date 1676897982 -3600
# Node ID cc292dafc52735abf523713cbcf7d28b2cd27f2b
# Parent  aea11797247bac3cbb283159aaf16a6cca3400cc# Parent  fa247805669d2c819e8d3fa3bf6f7cdae3dc9a97
merged

diff -r aea11797247b -r cc292dafc527 NEWS
--- a/NEWS	Sun Feb 19 21:21:19 2023 +0000
+++ b/NEWS	Mon Feb 20 13:59:42 2023 +0100
@@ -43,8 +43,6 @@
 
 *** 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.
diff -r aea11797247b -r cc292dafc527 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun Feb 19 21:21:19 2023 +0000
+++ b/src/Doc/Main/Main_Doc.thy	Mon Feb 20 13:59:42 2023 +0100
@@ -543,7 +543,6 @@
 \<^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>\\
@@ -586,31 +585,32 @@
 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_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*{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*{Infix operators in Main} % \<^theory>\<open>Main\<close>
 
diff -r aea11797247b -r cc292dafc527 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 19 21:21:19 2023 +0000
+++ b/src/HOL/List.thy	Mon Feb 20 13:59:42 2023 +0100
@@ -243,11 +243,6 @@
 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"
 
@@ -4686,126 +4681,6 @@
 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]:
diff -r aea11797247b -r cc292dafc527 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Feb 19 21:21:19 2023 +0000
+++ b/src/HOL/Map.thy	Mon Feb 20 13:59:42 2023 +0100
@@ -70,11 +70,21 @@
   "_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>
 
@@ -132,6 +142,99 @@
   "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)
@@ -139,6 +242,25 @@
     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)