# 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 \ set xs \ 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"