1.1 --- a/src/HOL/ex/Qsort.ML	Mon Mar 27 16:25:53 2000 +0200
     1.2 +++ b/src/HOL/ex/Qsort.ML	Mon Mar 27 17:04:03 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/ex/qsort.ML
     1.5 +(*  Title:      HOL/ex/Qsort.ML
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow (tidied by lcp)
     1.8      Copyright   1994 TU Muenchen
     1.9 @@ -6,6 +6,8 @@
    1.10  The verification of Quicksort
    1.11  *)
    1.12  
    1.13 +(*** Version one: higher-order ***)
    1.14 +
    1.15  Addsimps qsort.rules;
    1.16  
    1.17  Goal "multiset (qsort(le,xs)) x = multiset xs x";
    1.18 @@ -26,3 +28,26 @@
    1.19  by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
    1.20  by (Blast_tac 1);
    1.21  qed_spec_mp "sorted_qsort";
    1.22 +
    1.23 +
    1.24 +(*** Version two: type classes ***)
    1.25 +
    1.26 +Addsimps quickSort.rules;
    1.27 +
    1.28 +Goal "multiset (quickSort xs) z = multiset xs z";
    1.29 +by (res_inst_tac [("u","xs")] quickSort.induct 1);
    1.30 +by Auto_tac;
    1.31 +qed "quickSort_permutes";
    1.32 +Addsimps [quickSort_permutes];
    1.33 +
    1.34 +(*Also provable by induction*)
    1.35 +Goal "set (quickSort xs) = set xs";
    1.36 +by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
    1.37 +qed "set_quickSort";
    1.38 +Addsimps [set_quickSort];
    1.39 +
    1.40 +Goal "sorted (op <=) (quickSort xs)";
    1.41 +by (res_inst_tac [("u","xs")] quickSort.induct 1);
    1.42 +by (ALLGOALS Asm_simp_tac);
    1.43 +by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
    1.44 +qed_spec_mp "sorted_quickSort";

     2.1 --- a/src/HOL/ex/Qsort.thy	Mon Mar 27 16:25:53 2000 +0200
     2.2 +++ b/src/HOL/ex/Qsort.thy	Mon Mar 27 17:04:03 2000 +0200
     2.3 @@ -7,6 +7,8 @@
     2.4  *)
     2.5  
     2.6  Qsort = Sorting +
     2.7 +
     2.8 +(*Version one: higher-order*)
     2.9  consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
    2.10  
    2.11  recdef qsort "measure (size o snd)"
    2.12 @@ -17,4 +19,15 @@
    2.13      "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
    2.14                         @ (x # qsort(le, [y:xs . le x y]))"
    2.15  
    2.16 +
    2.17 +(*Version two: type classes*)
    2.18 +consts quickSort :: "('a::linorder) list => 'a list"
    2.19 +
    2.20 +recdef quickSort "measure size"
    2.21 +    simpset "simpset() addsimps [length_filter RS le_less_trans]"
    2.22 +    
    2.23 +    "quickSort []   = []"
    2.24 +    
    2.25 +    "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"
    2.26 +
    2.27  end