src/HOL/Library/Quicksort.thy
author haftmann
Tue Oct 16 23:12:45 2007 +0200 (2007-10-16)
changeset 25062 af5ef0d4d655
parent 24615 17dbd993293d
child 27368 9f90ac19e32b
permissions -rw-r--r--
global class syntax
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
nipkow@24615
     9
imports Multiset
nipkow@24615
    10
begin
nipkow@24615
    11
nipkow@24615
    12
context linorder
nipkow@24615
    13
begin
nipkow@24615
    14
nipkow@24615
    15
function 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
by pat_completeness auto
nipkow@24615
    19
nipkow@24615
    20
termination
nipkow@24615
    21
by (relation "measure size")
nipkow@24615
    22
   (auto simp: length_filter_le[THEN order_class.le_less_trans])
nipkow@24615
    23
nipkow@24615
    24
end
nipkow@24615
    25
context linorder
nipkow@24615
    26
begin
nipkow@24615
    27
nipkow@24615
    28
lemma quicksort_permutes [simp]:
nipkow@24615
    29
  "multiset_of (quicksort xs) = multiset_of xs"
nipkow@24615
    30
by (induct xs rule: quicksort.induct) (auto simp: union_ac)
nipkow@24615
    31
nipkow@24615
    32
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
nipkow@24615
    33
by(simp add: set_count_greater_0)
nipkow@24615
    34
nipkow@24615
    35
lemma sorted_quicksort: "sorted(quicksort xs)"
nipkow@24615
    36
apply (induct xs rule: quicksort.induct)
nipkow@24615
    37
 apply simp
nipkow@24615
    38
apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
nipkow@24615
    39
apply (metis leD le_cases le_less_trans)
nipkow@24615
    40
done
nipkow@24615
    41
nipkow@24615
    42
end
nipkow@24615
    43
nipkow@24615
    44
end