src/HOL/Library/Quicksort.thy
author nipkow
Tue Sep 18 05:42:46 2007 +0200 (2007-09-18)
changeset 24615 17dbd993293d
child 25062 af5ef0d4d655
permissions -rw-r--r--
Added function package to PreList
Added sorted/sort to List
Moved qsort from ex to Library
     1 (*  ID:         $Id$
     2     Author:     Tobias Nipkow
     3     Copyright   1994 TU Muenchen
     4 *)
     5 
     6 header{*Quicksort*}
     7 
     8 theory Quicksort
     9 imports Multiset
    10 begin
    11 
    12 context linorder
    13 begin
    14 
    15 function quicksort :: "'a list \<Rightarrow> 'a list" where
    16 "quicksort []     = []" |
    17 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
    18 by pat_completeness auto
    19 
    20 termination
    21 by (relation "measure size")
    22    (auto simp: length_filter_le[THEN order_class.le_less_trans])
    23 
    24 end
    25 context linorder
    26 begin
    27 
    28 lemma quicksort_permutes [simp]:
    29   "multiset_of (quicksort xs) = multiset_of xs"
    30 by (induct xs rule: quicksort.induct) (auto simp: union_ac)
    31 
    32 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    33 by(simp add: set_count_greater_0)
    34 
    35 lemma sorted_quicksort: "sorted(quicksort xs)"
    36 apply (induct xs rule: quicksort.induct)
    37  apply simp
    38 apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
    39 apply (metis leD le_cases le_less_trans)
    40 done
    41 
    42 end
    43 
    44 end