Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
(* Author: Tobias Nipkow
Copyright 1994 TU Muenchen
*)
section \<open>Quicksort with function package\<close>
theory Quicksort
imports "HOL-Library.Multiset"
begin
context linorder
fun quicksort :: "'a list \<Rightarrow> 'a list" where
"quicksort [] = []"
| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
lemma [code]:
"quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
by (simp_all add: not_le)
lemma quicksort_permutes [simp]:
"mset (quicksort xs) = mset xs"
by (induction xs rule: quicksort.induct) (simp_all)
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
proof -
have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
by simp
then show ?thesis by (simp only: set_mset_mset)
qed
lemma sorted_quicksort: "sorted (quicksort xs)"
by (induct xs rule: quicksort.induct) (auto simp add: sorted_append not_le less_imp_le)
theorem sort_quicksort:
"sort = quicksort"
by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
end
