src/HOL/Library/Quicksort.thy
author huffman
Thu Jun 11 09:03:24 2009 -0700 (2009-06-11)
changeset 31563 ded2364d14d4
parent 30738 0842e906300c
child 37075 a680ce27aa56
permissions -rw-r--r--
cleaned up some proofs
     1 (*  Author:     Tobias Nipkow
     2     Copyright   1994 TU Muenchen
     3 *)
     4 
     5 header{*Quicksort*}
     6 
     7 theory Quicksort
     8 imports Main 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. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
    17 
    18 lemma quicksort_permutes [simp]:
    19   "multiset_of (quicksort xs) = multiset_of xs"
    20 by (induct xs rule: quicksort.induct) (auto simp: union_ac)
    21 
    22 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    23 by(simp add: set_count_greater_0)
    24 
    25 lemma sorted_quicksort: "sorted(quicksort xs)"
    26 apply (induct xs rule: quicksort.induct)
    27  apply simp
    28 apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
    29 apply (metis leD le_cases le_less_trans)
    30 done
    31 
    32 end
    33 
    34 end