src/HOL/Library/Quicksort.thy
author wenzelm
Thu Oct 16 22:44:24 2008 +0200 (2008-10-16)
changeset 28615 4c8fa015ec7f
parent 28041 f496e9f343b7
child 30738 0842e906300c
permissions -rw-r--r--
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
     1 (*  ID:         $Id$
     2     Author:     Tobias Nipkow
     3     Copyright   1994 TU Muenchen
     4 *)
     5 
     6 header{*Quicksort*}
     7 
     8 theory Quicksort
     9 imports Plain Multiset
    10 begin
    11 
    12 context linorder
    13 begin
    14 
    15 fun quicksort :: "'a list \<Rightarrow> 'a list" where
    16 "quicksort []     = []" |
    17 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
    18 
    19 lemma quicksort_permutes [simp]:
    20   "multiset_of (quicksort xs) = multiset_of xs"
    21 by (induct xs rule: quicksort.induct) (auto simp: union_ac)
    22 
    23 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    24 by(simp add: set_count_greater_0)
    25 
    26 lemma sorted_quicksort: "sorted(quicksort xs)"
    27 apply (induct xs rule: quicksort.induct)
    28  apply simp
    29 apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
    30 apply (metis leD le_cases le_less_trans)
    31 done
    32 
    33 end
    34 
    35 end