# HG changeset patch # User nipkow # Date 1667893289 -3600 # Node ID a125c8baf643bb04a37f447e34811d3308798d36 # Parent defaa0b1742433130d2150e8ca5cdf14b9a93452 retain derived lemma for better findability diff -r defaa0b17424 -r a125c8baf643 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) \ sort_key f xs = xs" -by (induct xs) (auto simp add: insort_is_Cons) +by (induction xs) (auto simp add: insort_is_Cons) + +text \Subsumed by @{thm sort_key_id_if_sorted} but easier to find:\ +lemma sorted_sort_id: "sorted xs \ sort xs = xs" +by (simp add: sort_key_id_if_sorted) lemma insort_key_remove1: assumes "a \ set xs" and "sorted (map f xs)" and "hd (filter (\x. f a = f x) xs) = a"