QuickSort in Isabelle

QuickSort.thy

theory QuickSort imports Main begin

fun quicksort :: "('a :: ord) list ⇒ 'a list" where
  "quicksort [] = []"
| "quicksort (x#xs) = (
    let (smaller, greater) = partition (op ≥ x) xs
    in quicksort smaller @ x # quicksort greater)"

lemma quicksort_content: "set xs = set (quicksort xs)"
proof (induct xs rule: quicksort.induct)
  case 1
  then show ?case
    by simp
next
  case (2 x xs)
  obtain smaller and greater
    where *: "(smaller, greater) = partition (op ≥ x) xs"
    by simp
  then have
    "set smaller = set (quicksort smaller)" and
    "set greater = set (quicksort greater)"
    using 2 by meson+
  then have "set (smaller @ [x] @ greater) =
   set (quicksort smaller @ [x] @ quicksort greater)"
    by simp
  then show ?case
    using * by auto
qed

lemma quicksort_sorts: "sorted (quicksort xs)"
proof (induct xs rule: quicksort.induct)
  case 1
  then show ?case
    by simp
next
  case (2 x xs)
  obtain smaller and greater
    where *: "(smaller, greater) = partition (op ≥ x) xs"
    by simp
  then have
    "sorted (quicksort smaller)" and
    "sorted (quicksort greater)"
    using 2 by blast+
  moreover have "∀g ∈ set greater. x ≤ g"
    using * by auto
  then have "∀g ∈ set (quicksort greater). x ≤ g"
    using quicksort_content by blast
  moreover have "∀s ∈ set smaller. ∀g ∈ set (x # greater). s ≤ g"
    using * by auto
  then have "∀s ∈ set (quicksort smaller). ∀g ∈ set (x # quicksort greater). s ≤ g"
    using quicksort_content by auto
  ultimately have "sorted (quicksort smaller @ x # quicksort greater)"
    using sorted.Cons sorted_append by blast
  then show ?case
    using * by simp
qed

lemma partition_length:
  "partition f xs = (as, bs) ⟹ length xs = length as + length bs"
  by (induct xs arbitrary: as bs) auto

lemma quicksort_length: "length xs = length (quicksort xs)"
proof (induct xs rule: quicksort.induct)
  case 1
  then show ?case
    by simp
next
  case (2 x xs)
  obtain smaller and greater
    where *: "(smaller, greater) = partition (op ≥ x) xs"
    by simp
  then have
    "length smaller = length (quicksort smaller)" and
    "length greater = length (quicksort greater)"
    using 2 by blast+
  moreover have "length (x # xs) = length (smaller @ x # greater)"
    using * partition_length by auto
  ultimately show ?case
    using * by simp
qed

end