--- 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