# HG changeset patch
# User nipkow
# Date 1190092962 -7200
# Node ID bc484b2671fd08cd6f099838b7e57b4cc9e68e16
# Parent  fac3dd4ade836b156cdae3e740a42592c57321fb
sorting

diff -r fac3dd4ade83 -r bc484b2671fd src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 18 06:21:40 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 18 07:22:42 2007 +0200
@@ -2493,6 +2493,12 @@
 
 subsection {*Sorting*}
 
+text{* Currently it is not shown that @{const sort} returns a
+permutation of its input because the nicest proof is via multisets,
+which are not yet available. Alternatively one could define a function
+that counts the number of occurrences of an element in a list and use
+that instead of multisets to state the correctness property. *}
+
 context linorder
 begin
 
@@ -2507,13 +2513,13 @@
 lemma set_insort: "set(insort x xs) = insert x (set xs)"
 by (induct xs) auto
 
-lemma set_sort: "set(sort xs) = set xs"
+lemma set_sort[simp]: "set(sort xs) = set xs"
 by (induct xs) (simp_all add:set_insort)
 
 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
 by(induct xs)(auto simp:set_insort)
 
-lemma distinct_sort: "distinct (sort xs) = distinct xs"
+lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
 by(induct xs)(simp_all add:distinct_insort set_sort)
 
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"