# HG changeset patch
# User haftmann
# Date 1288711917 -3600
# Node ID 62bdd1bfcd903691935515f79d1902255cdbf45c
# Parent  2d507370e8797aab0883fb5657f2fab57a275774
lemmas sorted_map_same, sorted_same

diff -r 2d507370e879 -r 62bdd1bfcd90 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Nov 02 16:31:56 2010 +0100
+++ b/src/HOL/List.thy	Tue Nov 02 16:31:57 2010 +0100
@@ -3949,17 +3949,21 @@
   "filter P (sort_key f xs) = sort_key f (filter P xs)"
   by (induct xs) (simp_all add: filter_insort_triv filter_insort)
 
-lemma sorted_same [simp]:
-  "sorted [x\<leftarrow>xs. x = f xs]"
-proof (induct xs arbitrary: f)
+lemma sorted_map_same:
+  "sorted (map f [x\<leftarrow>xs. f x = g xs])"
+proof (induct xs arbitrary: g)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
-  then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
-  moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
+  then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
+  moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
   ultimately show ?case by (simp_all add: sorted_Cons)
 qed
 
+lemma sorted_same:
+  "sorted [x\<leftarrow>xs. x = g xs]"
+  using sorted_map_same [of "\<lambda>x. x"] by simp
+
 lemma remove1_insort [simp]:
   "remove1 x (insort x xs) = xs"
   by (induct xs) simp_all