--- a/src/HOL/Library/Poly_Mapping.thy Sun Nov 06 23:10:28 2022 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy Mon Nov 07 22:16:37 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
--- a/src/HOL/List.thy Sun Nov 06 23:10:28 2022 +0100
+++ b/src/HOL/List.thy Mon Nov 07 22:16:37 2022 +0100
@@ -5881,7 +5881,7 @@
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 sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+lemma sort_key_id_if_sorted: "sorted (map f xs) \<Longrightarrow> sort_key f xs = xs"
by (induct xs) (auto simp add: insort_is_Cons)
lemma insort_key_remove1:
@@ -5978,10 +5978,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})"