src/HOL/ex/Quicksort.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 41413 64cd30d6b0b8
child 44604 1ad3159323dc
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     1 (*  Author:     Tobias Nipkow
     2     Copyright   1994 TU Muenchen
     3 *)
     4 
     5 header {* Quicksort with function package *}
     6 
     7 theory Quicksort
     8 imports Main "~~/src/HOL/Library/Multiset"
     9 begin
    10 
    11 context linorder
    12 begin
    13 
    14 fun quicksort :: "'a list \<Rightarrow> 'a list" where
    15   "quicksort []     = []"
    16 | "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    17 
    18 lemma [code]:
    19   "quicksort []     = []"
    20   "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    21   by (simp_all add: not_le)
    22 
    23 lemma quicksort_permutes [simp]:
    24   "multiset_of (quicksort xs) = multiset_of xs"
    25   by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
    26 
    27 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    28   by (simp add: set_count_greater_0)
    29 
    30 lemma sorted_quicksort: "sorted (quicksort xs)"
    31   by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
    32 
    33 theorem sort_quicksort:
    34   "sort = quicksort"
    35   by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
    36 
    37 end
    38 
    39 end