src/HOL/ex/Qsort.thy

lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

(*  Title:      HOL/ex/Qsort.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1994 TU Muenchen

Quicksort
*)

theory Qsort = Sorting:

(*Version one: higher-order*)
consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"

recdef qsort "measure (size o snd)"
"qsort(le, [])   = []"
"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
                   qsort(le, [y:xs . le x y])"
(hints recdef_simp: length_filter_le[THEN le_less_trans])

lemma qsort_permutes[simp]:
 "multiset (qsort(le,xs)) x = multiset xs x"
by (induct le xs rule: qsort.induct, auto)


(*Also provable by induction*)
lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
by(simp add: set_via_multiset)

lemma sorted_qsort:
 "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
apply (induct le xs rule: qsort.induct)
 apply simp
apply simp
apply(unfold Sorting.total_def Sorting.transf_def)
apply blast
done


(*Version two: type classes*)

consts quickSort :: "('a::linorder) list => 'a list"

recdef quickSort "measure size"
"quickSort []   = []"
"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
(hints recdef_simp: length_filter_le[THEN le_less_trans])

lemma quickSort_permutes[simp]:
 "multiset (quickSort xs) z = multiset xs z"
by (induct xs rule: quickSort.induct) auto

(*Also provable by induction*)
lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
by(simp add: set_via_multiset)

lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
apply (induct xs rule: quickSort.induct)
 apply simp
apply simp
apply(blast intro: linorder_linear[THEN disjE] order_trans)
done

end