src/HOL/ex/Qsort.thy
changeset 8590 89675b444abe
parent 8524 f990040535c9
child 13159 2af7b94892ce
--- 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