Theory HOL-ex.Quicksort

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

section ‹Quicksort with function package›

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. y<x] @ [x] @ quicksort [y←xs. 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