src/HOL/Library/Quicksort.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 30738 0842e906300c
child 37075 a680ce27aa56
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@30738
     1
(*  Author:     Tobias Nipkow
nipkow@24615
     2
    Copyright   1994 TU Muenchen
nipkow@24615
     3
*)
nipkow@24615
     4
nipkow@24615
     5
header{*Quicksort*}
nipkow@24615
     6
nipkow@24615
     7
theory Quicksort
haftmann@30738
     8
imports Main Multiset
nipkow@24615
     9
begin
nipkow@24615
    10
nipkow@24615
    11
context linorder
nipkow@24615
    12
begin
nipkow@24615
    13
krauss@28041
    14
fun quicksort :: "'a list \<Rightarrow> 'a list" where
nipkow@24615
    15
"quicksort []     = []" |
haftmann@25062
    16
"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
nipkow@24615
    17
nipkow@24615
    18
lemma quicksort_permutes [simp]:
nipkow@24615
    19
  "multiset_of (quicksort xs) = multiset_of xs"
nipkow@24615
    20
by (induct xs rule: quicksort.induct) (auto simp: union_ac)
nipkow@24615
    21
nipkow@24615
    22
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
nipkow@24615
    23
by(simp add: set_count_greater_0)
nipkow@24615
    24
nipkow@24615
    25
lemma sorted_quicksort: "sorted(quicksort xs)"
nipkow@24615
    26
apply (induct xs rule: quicksort.induct)
nipkow@24615
    27
 apply simp
nipkow@24615
    28
apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
nipkow@24615
    29
apply (metis leD le_cases le_less_trans)
nipkow@24615
    30
done
nipkow@24615
    31
nipkow@24615
    32
end
nipkow@24615
    33
nipkow@24615
    34
end