# HG changeset patch
# User paulson
# Date 952707168 -3600
# Node ID 5983668cac15e2cad413f4cdfbac371b63463cfb
# Parent  09db77a084aa9a6e8466f27faad2d90523be3f75
now uses recdef instead of "rules"

diff -r 09db77a084aa -r 5983668cac15 src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Mar 10 17:51:59 2000 +0100
+++ b/src/HOL/ex/Qsort.ML	Fri Mar 10 17:52:48 2000 +0100
@@ -1,56 +1,28 @@
 (*  Title:      HOL/ex/qsort.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Tobias Nipkow (tidied by lcp)
     Copyright   1994 TU Muenchen
 
-Two verifications of Quicksort
+The verification of Quicksort
 *)
 
-Addsimps [ball_Un];
-
-(* Towards a proof of qsort_ind
-
-A short proof of Konrad's wf_minimal in WF1.ML:
-
-val [p1] = goalw WF.thy [wf_def]
-"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
-by (rtac allI 1);
-by (cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
-by (fast_tac HOL_cs 1);
-val wf_minimal = result();
+Addsimps qsort.rules;
 
-*)
-
-
-Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
+Goal "multiset (qsort(le,xs)) x = multiset xs x";
+by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
+by Auto_tac;
+qed "qsort_permutes";
+Addsimps [qsort_permutes];
 
-Goal "!x. mset (qsort le xs) x = mset xs x";
-by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (ALLGOALS Asm_simp_tac);
-qed "qsort_permutes";
-
-Goal "set(qsort le xs) = set xs";
-by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
+(*Also provable by induction*)
+Goal "set (qsort(le,xs)) = set xs";
+by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
 qed "set_qsort";
 Addsimps [set_qsort];
 
-goal List.thy
-  "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed"Ball_set_filter";
-Addsimps [Ball_set_filter];
-
-Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
-\                     (!x:set xs. !y:set ys. le x y))";
-by (induct_tac "xs" 1);
+Goal "total(le) & transf(le) --> sorted le (qsort(le,xs))";
+by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
 by (ALLGOALS Asm_simp_tac);
-qed "sorted_append";
-Addsimps [sorted_append];
-
-Goal "[| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
-by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (ALLGOALS Asm_simp_tac);
-by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by (Fast_tac 1);
-qed "sorted_qsort";
+by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
+by (Blast_tac 1);
+qed_spec_mp "sorted_qsort";
diff -r 09db77a084aa -r 5983668cac15 src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Fri Mar 10 17:51:59 2000 +0100
+++ b/src/HOL/ex/Qsort.thy	Fri Mar 10 17:52:48 2000 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/qsort.thy
+(*  Title:      HOL/ex/Qsort.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
@@ -7,21 +7,14 @@
 *)
 
 Qsort = Sorting +
-consts
-  qsort  :: [['a,'a] => bool, 'a list] => 'a list
-
-rules
-
-qsort_Nil  "qsort le [] = []"
-qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
-                            (x# qsort le [y:xs . le x y])"
+consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
 
-(* computational induction.
-   The dependence of p on x but not xs is intentional.
-*)
-qsort_ind
- "[| P([]); 
-    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
-            P(x#xs) |] 
- ==> P(xs)"
+recdef qsort "measure (size o snd)"
+    simpset "simpset() addsimps [less_Suc_eq_le]"
+    
+    "qsort(le, [])   = []"
+    
+    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
+                       @ (x # qsort(le, [y:xs . le x y]))"
+
 end