QSort.thy

theory QSort
imports Main
begin

fun qsort :: "'a::ord list ⇒ 'a list" where 
   "qsort [] = []"
 | "qsort (x#xs) =   (qsort (filter (λy. y≤x) xs))
                 @ x#(qsort (filter (λy. y>x) xs))"


fun sorted :: "'a::ord list ⇒ bool" where
   "sorted [] = True"
 | "sorted [x] = True"
 | "sorted (x#y#zs) = ((x ≤ y) ∧ sorted (y#zs))"


theorem "∀xs::('a::ord list). sorted (qsort xs)"
  sorry

end