Tue, 18 Sep 2007 07:22:42 +0200
changeset 24617 bc484b2671fd
parent 24616 fac3dd4ade83
child 24618 6ab574864cd4
--- 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
@@ -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"