Quelle Quicksort.thy

Sprache: Isabelle

(* Author: Tobias Nipkow
Copyright 1994 TU Muenchen
*)

section ‹

Quicksort
"HOL-Library.Multiset"

linorder

quicksort :: "'a list ==> 'a list" where
"quicksort [] = []"
"quicksort (x#xs) = quicksort [y←xs. ¬ x≤y] @ [x] @ quicksort [y←xs. x≤y]"

[code]:
"quicksort [] = []"
"quicksort (x#xs) = quicksort [y←xs. y<x] @ [x] @ quicksort [y←xs. x≤y]"
by (simp_all add: not_le)

quicksort_permutes [simp]:
"mset (quicksort xs) = mset xs"
(induction xs rule: quicksort.induct) (simp_all)

set_quicksort [simp]: "set (quicksort xs) = set xs"
-
have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
by simp
then show ?thesis by (simp only: set_mset_mset)

sorted_quicksort: "sorted (quicksort xs)"
by (induct xs rule: quicksort.induct) (auto simp add: sorted_append not_le less_imp_le)

sort_quicksort:
"sort = quicksort"
by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.