summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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"