# HG changeset patch
# User paulson
# Date 954169443 -7200
# Node ID 89675b444abef747b3101189788512b10d846295
# Parent  a24f7e5ee7effe6d886df3653bd5aa0a9fd78383
added an order-sorted version of quickSort

diff -r a24f7e5ee7ef -r 89675b444abe src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Mon Mar 27 16:25:53 2000 +0200
+++ b/src/HOL/ex/Qsort.ML	Mon Mar 27 17:04:03 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/qsort.ML
+(*  Title:      HOL/ex/Qsort.ML
     ID:         $Id$
     Author:     Tobias Nipkow (tidied by lcp)
     Copyright   1994 TU Muenchen
@@ -6,6 +6,8 @@
 The verification of Quicksort
 *)
 
+(*** Version one: higher-order ***)
+
 Addsimps qsort.rules;
 
 Goal "multiset (qsort(le,xs)) x = multiset xs x";
@@ -26,3 +28,26 @@
 by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
 by (Blast_tac 1);
 qed_spec_mp "sorted_qsort";
+
+
+(*** Version two: type classes ***)
+
+Addsimps quickSort.rules;
+
+Goal "multiset (quickSort xs) z = multiset xs z";
+by (res_inst_tac [("u","xs")] quickSort.induct 1);
+by Auto_tac;
+qed "quickSort_permutes";
+Addsimps [quickSort_permutes];
+
+(*Also provable by induction*)
+Goal "set (quickSort xs) = set xs";
+by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
+qed "set_quickSort";
+Addsimps [set_quickSort];
+
+Goal "sorted (op <=) (quickSort xs)";
+by (res_inst_tac [("u","xs")] quickSort.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
+qed_spec_mp "sorted_quickSort";
diff -r a24f7e5ee7ef -r 89675b444abe src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Mon Mar 27 16:25:53 2000 +0200
+++ b/src/HOL/ex/Qsort.thy	Mon Mar 27 17:04:03 2000 +0200
@@ -7,6 +7,8 @@
 *)
 
 Qsort = Sorting +
+
+(*Version one: higher-order*)
 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
 
 recdef qsort "measure (size o snd)"
@@ -17,4 +19,15 @@
     "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
                        @ (x # qsort(le, [y:xs . le x y]))"
 
+
+(*Version two: type classes*)
+consts quickSort :: "('a::linorder) list => 'a list"
+
+recdef quickSort "measure size"
+    simpset "simpset() addsimps [length_filter RS le_less_trans]"
+    
+    "quickSort []   = []"
+    
+    "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"
+
 end