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