ex/Qsort.thy

+Qsort = List +
+consts
+  sorted :: "[['a,'a] => bool, 'a list] => bool"
+  mset   :: "'a list => ('a => nat)"
+  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
+
+rules
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+qsort_Nil  "qsort(le,[]) = []"
+qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
+
+(* 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(Cons(x,xs)) |] \
+\ ==> P(xs)"
+end