src/HOL/ex/Quicksort.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 44604 1ad3159323dc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
introduce order topology
haftmann@30738
     1
(*  Author:     Tobias Nipkow
nipkow@24615
     2
    Copyright   1994 TU Muenchen
nipkow@24615
     3
*)
nipkow@24615
     4
haftmann@40349
     5
header {* Quicksort with function package *}
nipkow@24615
     6
nipkow@24615
     7
theory Quicksort
wenzelm@44604
     8
imports "~~/src/HOL/Library/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
haftmann@37075
    15
  "quicksort []     = []"
haftmann@37075
    16
| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
haftmann@37075
    17
haftmann@37075
    18
lemma [code]:
haftmann@37075
    19
  "quicksort []     = []"
haftmann@37075
    20
  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
haftmann@37075
    21
  by (simp_all add: not_le)
nipkow@24615
    22
nipkow@24615
    23
lemma quicksort_permutes [simp]:
nipkow@24615
    24
  "multiset_of (quicksort xs) = multiset_of xs"
haftmann@37075
    25
  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
nipkow@24615
    26
nipkow@24615
    27
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
haftmann@37075
    28
  by (simp add: set_count_greater_0)
nipkow@24615
    29
haftmann@37075
    30
lemma sorted_quicksort: "sorted (quicksort xs)"
haftmann@37075
    31
  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
haftmann@37075
    32
haftmann@40349
    33
theorem sort_quicksort:
haftmann@37075
    34
  "sort = quicksort"
haftmann@37075
    35
  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
nipkow@24615
    36
nipkow@24615
    37
end
nipkow@24615
    38
nipkow@24615
    39
end