src/HOL/ex/Qsort.thy

--- a/src/HOL/ex/Qsort.thy	Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/Qsort.thy	Fri Apr 22 17:32:03 2005 +0200
@@ -2,31 +2,33 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
-
-Quicksort
 *)
 
-theory Qsort = Sorting:
+header{*Quicksort*}
 
-(*Version one: higher-order*)
+theory Qsort
+imports Sorting
+begin
+
+subsection{*Version 1: 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])"
+    "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_of (qsort(le,xs)) = multiset_of xs"
+lemma qsort_permutes [simp]:
+     "multiset_of (qsort(le,xs)) = multiset_of xs"
 by (induct le xs rule: qsort.induct) (auto simp: union_ac)
 
-(*Also provable by induction*)
-lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
+lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs";
 by(simp add: set_count_greater_0)
 
 lemma sorted_qsort:
- "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
+     "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
 apply (induct le xs rule: qsort.induct)
  apply simp
 apply simp
@@ -35,28 +37,23 @@
 done
 
 
-(*Version two: type classes*)
+subsection{*Version 2: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]"
+    "quickSort []   = []"
+    "quickSort (x#l) = quickSort [y:l. ~ x\<le>y] @ [x] @ quickSort [y:l. x\<le>y]"
 (hints recdef_simp: length_filter_le[THEN le_less_trans])
 
 lemma quickSort_permutes[simp]:
  "multiset_of (quickSort xs) = multiset_of xs"
 by (induct xs rule: quickSort.induct) (auto simp: union_ac)
 
-(*Also provable by induction*)
 lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
 by(simp add: set_count_greater_0)
 
-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
+theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)"
+by (induct xs rule: quickSort.induct, auto)
 
 end