# HG changeset patch # User bulwahn # Date 1315908869 -7200 # Node ID 840d8c3d91136e625126b23b0380c2072c2b4c35 # Parent f0fd38929d21470beb37421ed64a597fe9bae0e3 added lemma motivated by a more specific lemma in the AFP-KBPs theories diff -r f0fd38929d21 -r 840d8c3d9113 src/HOL/List.thy --- a/src/HOL/List.thy Tue Sep 13 09:56:38 2011 +0200 +++ b/src/HOL/List.thy Tue Sep 13 12:14:29 2011 +0200 @@ -3867,6 +3867,9 @@ lemma insort_is_Cons: "\x\set xs. f a \ f x \ insort_key f a xs = a # xs" by (cases xs) auto +lemma sorted_sort_id: "sorted xs \ sort xs = xs" + by (induct xs) (auto simp add: sorted_Cons insort_is_Cons) + lemma sorted_map_remove1: "sorted (map f xs) \ sorted (map f (remove1 x xs))" by (induct xs) (auto simp add: sorted_Cons)