src/HOL/Library/Quicksort.thy
changeset 24615 17dbd993293d
child 25062 af5ef0d4d655
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Quicksort.thy	Tue Sep 18 05:42:46 2007 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Tobias Nipkow
     1.6 +    Copyright   1994 TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header{*Quicksort*}
    1.10 +
    1.11 +theory Quicksort
    1.12 +imports Multiset
    1.13 +begin
    1.14 +
    1.15 +context linorder
    1.16 +begin
    1.17 +
    1.18 +function quicksort :: "'a list \<Rightarrow> 'a list" where
    1.19 +"quicksort []     = []" |
    1.20 +"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
    1.21 +by pat_completeness auto
    1.22 +
    1.23 +termination
    1.24 +by (relation "measure size")
    1.25 +   (auto simp: length_filter_le[THEN order_class.le_less_trans])
    1.26 +
    1.27 +end
    1.28 +context linorder
    1.29 +begin
    1.30 +
    1.31 +lemma quicksort_permutes [simp]:
    1.32 +  "multiset_of (quicksort xs) = multiset_of xs"
    1.33 +by (induct xs rule: quicksort.induct) (auto simp: union_ac)
    1.34 +
    1.35 +lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    1.36 +by(simp add: set_count_greater_0)
    1.37 +
    1.38 +lemma sorted_quicksort: "sorted(quicksort xs)"
    1.39 +apply (induct xs rule: quicksort.induct)
    1.40 + apply simp
    1.41 +apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
    1.42 +apply (metis leD le_cases le_less_trans)
    1.43 +done
    1.44 +
    1.45 +end
    1.46 +
    1.47 +end