# 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: "\<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)