src/HOL/Library/Quicksort.thy
author krauss
Thu Aug 28 15:33:33 2008 +0200 (2008-08-28 ago)
changeset 28041 f496e9f343b7
parent 27682 25aceefd4786
child 30738 0842e906300c
permissions -rw-r--r--
quicksort: function -> fun
nipkow@24615
     1
(*  ID:         $Id$
nipkow@24615
     2
    Author:     Tobias Nipkow
nipkow@24615
     3
    Copyright   1994 TU Muenchen
nipkow@24615
     4
*)
nipkow@24615
     5
nipkow@24615
     6
header{*Quicksort*}
nipkow@24615
     7
nipkow@24615
     8
theory Quicksort
haftmann@27368
     9
imports Plain Multiset
nipkow@24615
    10
begin
nipkow@24615
    11
nipkow@24615
    12
context linorder
nipkow@24615
    13
begin
nipkow@24615
    14
krauss@28041
    15
fun quicksort :: "'a list \<Rightarrow> 'a list" where
nipkow@24615
    16
"quicksort []     = []" |
haftmann@25062
    17
"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
nipkow@24615
    18
nipkow@24615
    19
lemma quicksort_permutes [simp]:
nipkow@24615
    20
  "multiset_of (quicksort xs) = multiset_of xs"
nipkow@24615
    21
by (induct xs rule: quicksort.induct) (auto simp: union_ac)
nipkow@24615
    22
nipkow@24615
    23
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
nipkow@24615
    24
by(simp add: set_count_greater_0)
nipkow@24615
    25
nipkow@24615
    26
lemma sorted_quicksort: "sorted(quicksort xs)"
nipkow@24615
    27
apply (induct xs rule: quicksort.induct)
nipkow@24615
    28
 apply simp
nipkow@24615
    29
apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
nipkow@24615
    30
apply (metis leD le_cases le_less_trans)
nipkow@24615
    31
done
nipkow@24615
    32
nipkow@24615
    33
end
nipkow@24615
    34
nipkow@24615
    35
end