|
(* Author: Tobias Nipkow
Copyright 1994 TU Muenchen
*)
section \<open>Quicksort with function package\<close>
theory Quicksort
imports "HOL-Library.Multiset"
begin
context linorder
begin
fun quicksort :: "'a list \ 'a list" where
"quicksort [] = []"
| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]"
lemma [code]:
"quicksort [] = []"
"quicksort (x#xs) = quicksort [y\xs. yxs. x\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
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
