1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Fri Sep 14 07:31:55 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Fri Sep 14 10:07:59 2018 +0200
     1.3 @@ -351,4 +351,24 @@
     1.4  corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k"
     1.5  using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def)
     1.6  
     1.7 +
     1.8 +subsection "Quicksort"
     1.9 +
    1.10 +fun quicksort :: "('a::linorder) list \<Rightarrow> 'a list" where
    1.11 +"quicksort []     = []" |
    1.12 +"quicksort (x#xs) = quicksort (filter (\<lambda>y. y < x) xs) @ [x] @ quicksort (filter (\<lambda>y. x \<le> y) xs)"
    1.13 +
    1.14 +lemma mset_quicksort: "mset (quicksort xs) = mset xs"
    1.15 +apply (induction xs rule: quicksort.induct)
    1.16 +apply (auto simp: not_le)
    1.17 +done
    1.18 +
    1.19 +lemma set_quicksort: "set (quicksort xs) = set xs"
    1.20 +by(rule mset_eq_setD[OF mset_quicksort])
    1.21 +
    1.22 +lemma sorted_quicksort: "sorted (quicksort xs)"
    1.23 +apply (induction xs rule: quicksort.induct)
    1.24 +apply (auto simp add: sorted_append set_quicksort)
    1.25 +done
    1.26 +
    1.27  end