src/HOL/List.thy
changeset 44916 840d8c3d9113
parent 44890 22f665a2e91c
child 44921 58eef4843641
--- 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: "\<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"
+  by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
   by (induct xs) (auto simp add: sorted_Cons)