retain derived lemma for better findability
authornipkow
Tue, 08 Nov 2022 08:41:29 +0100
changeset 76485 a125c8baf643
parent 76484 defaa0b17424
child 76486 3d281371b213
retain derived lemma for better findability
src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 07 22:16:37 2022 +0100
+++ b/src/HOL/List.thy	Tue Nov 08 08:41:29 2022 +0100
@@ -5882,7 +5882,11 @@
 by (cases xs) auto
 
 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)
+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 (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"