# HG changeset patch
# User nipkow
# Date 1667893308 -3600
# Node ID 3d281371b2137ddb947a1cef789693b041201f34
# Parent  49acf5dd58cede33b4b5872bb27908e50c28c239# Parent  a125c8baf643bb04a37f447e34811d3308798d36
merged

diff -r 49acf5dd58ce -r 3d281371b213 src/HOL/Library/Poly_Mapping.thy
--- a/src/HOL/Library/Poly_Mapping.thy	Mon Nov 07 21:53:36 2022 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy	Tue Nov 08 08:41:48 2022 +0100
@@ -1487,7 +1487,7 @@
   shows "items (the_value xs) = xs"
 proof -
   from assms have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
-    unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sorted_sort_id)
+    unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sort_key_id_if_sorted)
   moreover from assms have "keys (the_value xs) = fst ` set xs"
     by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
   ultimately show ?thesis
diff -r 49acf5dd58ce -r 3d281371b213 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 07 21:53:36 2022 +0100
+++ b/src/HOL/List.thy	Tue Nov 08 08:41:48 2022 +0100
@@ -5881,8 +5881,12 @@
 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto
 
+lemma sort_key_id_if_sorted: "sorted (map f xs) \<Longrightarrow> sort_key f xs = xs"
+by (induction xs) (auto simp add: insort_is_Cons)
+
+text \<open>Subsumed by @{thm sort_key_id_if_sorted} but easier to find:\<close>
 lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
-by (induct xs) (auto simp add: insort_is_Cons)
+by (simp add: sort_key_id_if_sorted)
 
 lemma insort_key_remove1:
   assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
@@ -5978,10 +5982,10 @@
 end
 
 lemma sort_upt [simp]: "sort [m..<n] = [m..<n]"
-by (rule sorted_sort_id) simp
+by (rule sort_key_id_if_sorted) simp
 
 lemma sort_upto [simp]: "sort [i..j] = [i..j]"
-by (rule sorted_sort_id) simp
+by (rule sort_key_id_if_sorted) simp
 
 lemma sorted_find_Min:
   "sorted xs \<Longrightarrow> \<exists>x \<in> set xs. P x \<Longrightarrow> List.find P xs = Some (Min {x\<in>set xs. P x})"