diff -r c1a3020635a1 -r b503da67d2f7 ex/qsort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/qsort.thy Mon Jan 24 16:00:37 1994 +0100 @@ -0,0 +1,27 @@ +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