author nipkow Tue, 18 Sep 2007 07:22:42 +0200 changeset 24617 bc484b2671fd parent 24616 fac3dd4ade83 child 24618 6ab574864cd4
sorting
 src/HOL/List.thy file | annotate | diff | comparison | revisions
```--- 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"```