# HG changeset patch
# User nipkow
# Date 1536912479 -7200
# Node ID e6678381151899a8e67b6ec6cded77a2176aca4e
# Parent  8f7d3241ed68db3e0da33889b10d030d4b1b1343
added quicksort

diff -r 8f7d3241ed68 -r e66783811518 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Fri Sep 14 07:31:55 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Fri Sep 14 10:07:59 2018 +0200
@@ -351,4 +351,24 @@
 corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k"
 using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def)
 
+
+subsection "Quicksort"
+
+fun quicksort :: "('a::linorder) list \<Rightarrow> 'a list" where
+"quicksort []     = []" |
+"quicksort (x#xs) = quicksort (filter (\<lambda>y. y < x) xs) @ [x] @ quicksort (filter (\<lambda>y. x \<le> y) xs)"
+
+lemma mset_quicksort: "mset (quicksort xs) = mset xs"
+apply (induction xs rule: quicksort.induct)
+apply (auto simp: not_le)
+done
+
+lemma set_quicksort: "set (quicksort xs) = set xs"
+by(rule mset_eq_setD[OF mset_quicksort])
+
+lemma sorted_quicksort: "sorted (quicksort xs)"
+apply (induction xs rule: quicksort.induct)
+apply (auto simp add: sorted_append set_quicksort)
+done
+
 end