Theory Quicksort

(*
  File: Quicksort.thy
  Author: Bohua Zhan
*)

section ‹Quicksort›

theory Quicksort
  imports Arrays_Ex
begin

text ‹
  Functional version of quicksort.

  Implementation of quicksort is largely based on theory
  Imperative\_Quicksort in HOL/Imperative\_HOL/ex in the Isabelle
  library.
›

subsection ‹Outer remains›
  
definition outer_remains :: "'a list ⇒ 'a list ⇒ nat ⇒ nat ⇒ bool" where [rewrite]:
  "outer_remains xs xs' l r ⟷ (length xs = length xs' ∧ (∀i. i < l ∨ r < i ⟶ xs ! i = xs' ! i))"

lemma outer_remains_length [forward]:
  "outer_remains xs xs' l r ⟹ length xs = length xs'" by auto2

lemma outer_remains_eq [rewrite_back]:
  "outer_remains xs xs' l r ⟹ i < l ⟹ xs ! i = xs' ! i"
  "outer_remains xs xs' l r ⟹ r < i ⟹ xs ! i = xs' ! i" by auto2+

lemma outer_remains_sublist [backward2]:
  "outer_remains xs xs' l r ⟹ i < l ⟹ take i xs = take i xs'"
  "outer_remains xs xs' l r ⟹ r < i ⟹ drop i xs = drop i xs'"
  "i ≤ j ⟹ j ≤ length xs ⟹ outer_remains xs xs' l r ⟹ j ≤ l ⟹ sublist i j xs = sublist i j xs'"
  "i ≤ j ⟹ j ≤ length xs ⟹ outer_remains xs xs' l r ⟹ i > r ⟹ sublist i j xs = sublist i j xs'" by auto2+
setup ‹del_prfstep_thm_eqforward @{thm outer_remains_def}›

subsection ‹part1 function›  

function part1 :: "('a::linorder) list ⇒ nat ⇒ nat ⇒ 'a ⇒ (nat × 'a list)" where
  "part1 xs l r a = (
     if r ≤ l then (r, xs)
     else if xs ! l ≤ a then part1 xs (l + 1) r a
     else part1 (list_swap xs l r) l (r - 1) a)"
  by auto
  termination by (relation "measure (λ(_,l,r,_). r - l)") auto
setup ‹register_wellform_data ("part1 xs l r a", ["r < length xs"])›
setup ‹add_prfstep_check_req ("part1 xs l r a", "r < length xs")›

lemma part1_basic:
  "r < length xs ⟹ l ≤ r ⟹ (rs, xs') = part1 xs l r a ⟹
   outer_remains xs xs' l r ∧ mset xs' = mset xs ∧ l ≤ rs ∧ rs ≤ r"
@proof @fun_induct "part1 xs l r a" @unfold "part1 xs l r a" @qed
setup ‹add_forward_prfstep_cond @{thm part1_basic} [with_term "part1 ?xs ?l ?r ?a"]›

lemma part1_partitions1 [backward]:
  "r < length xs ⟹ (rs, xs') = part1 xs l r a ⟹ l ≤ i ⟹ i < rs ⟹ xs' ! i ≤ a"
@proof @fun_induct "part1 xs l r a" @unfold "part1 xs l r a" @qed

lemma part1_partitions2 [backward]:
  "r < length xs ⟹ (rs, xs') = part1 xs l r a ⟹ rs < i ⟹ i ≤ r ⟹ xs' ! i ≥ a"
@proof @fun_induct "part1 xs l r a" @unfold "part1 xs l r a" @qed

subsection ‹Paritition function›

definition partition :: "('a::linorder list) ⇒ nat ⇒ nat ⇒ (nat × 'a list)" where [rewrite]:
  "partition xs l r = (
    let p = xs ! r;
      (m, xs') = part1 xs l (r - 1) p;
      m' = if xs' ! m ≤ p then m + 1 else m
    in
      (m', list_swap xs' m' r))"
setup ‹register_wellform_data ("partition xs l r", ["l < r", "r < length xs"])›

lemma partition_basic:
  "l < r ⟹ r < length xs ⟹ (rs, xs') = partition xs l r ⟹
   outer_remains xs xs' l r ∧ mset xs' = mset xs ∧ l ≤ rs ∧ rs ≤ r" by auto2
setup ‹add_forward_prfstep_cond @{thm partition_basic} [with_term "partition ?xs ?l ?r"]›
  
lemma partition_partitions1 [forward]:
  "l < r ⟹ r < length xs ⟹ (rs, xs') = partition xs l r ⟹
   x ∈ set (sublist l rs xs') ⟹ x ≤ xs' ! rs"
@proof @obtain i where "i ≥ l" "i < rs" "x = xs' ! i" @qed

lemma partition_partitions2 [forward]:
  "l < r ⟹ r < length xs ⟹ (rs, xs'') = partition xs l r ⟹
   x ∈ set (sublist (rs + 1) (r + 1) xs'') ⟹ x ≥ xs'' ! rs"
@proof
  @obtain i where "i ≥ rs + 1" "i < r + 1" "x = xs'' ! i"
  @let "p = xs ! r"
  @let "m = fst (part1 xs l (r - 1) p)"
  @let "xs' = snd (part1 xs l (r - 1) p)"
  @case "xs' ! m ≤ p"
@qed
setup ‹del_prfstep_thm @{thm partition_def}›

lemma quicksort_term1:
  "¬r ≤ l ⟹ ¬ length xs ≤ r ⟹ x = partition xs l r ⟹ (p, xs1) = x ⟹ p - Suc l < r - l"
@proof @have "fst (partition xs l r) - l - 1 < r - l" @qed

lemma quicksort_term2:
  "¬r ≤ l ⟹ ¬ length xs ≤ r ⟹ x = partition xs l r ⟹ (p, xs2) = x ⟹ r - Suc p < r - l"
@proof @have "r - fst (partition xs l r) - 1 < r - l" @qed

subsection ‹Quicksort function›

function quicksort :: "('a::linorder) list ⇒ nat ⇒ nat ⇒ 'a list" where
  "quicksort xs l r = (
    if l ≥ r then xs
    else if r ≥ length xs then xs
    else let
      (p, xs1) = partition xs l r;
      xs2 = quicksort xs1 l (p - 1)
    in
      quicksort xs2 (p + 1) r)"
  by auto termination apply (relation "measure (λ(a, l, r). (r - l))") 
  by (auto simp add: quicksort_term1 quicksort_term2)

lemma quicksort_basic [rewrite_arg]:
  "mset (quicksort xs l r) = mset xs ∧ outer_remains xs (quicksort xs l r) l r"
@proof @fun_induct "quicksort xs l r" @unfold "quicksort xs l r" @qed

lemma quicksort_trivial1 [rewrite]:
  "l ≥ r ⟹ quicksort xs l r = xs"
@proof @unfold "quicksort xs l r" @qed

lemma quicksort_trivial2 [rewrite]:
  "r ≥ length xs ⟹ quicksort xs l r = xs"
@proof @unfold "quicksort xs l r" @qed

lemma quicksort_permutes [resolve]:
  "xs' = quicksort xs l r ⟹ set (sublist l (r + 1) xs') = set (sublist l (r + 1) xs)"
@proof
  @case "l ≥ r" @case "r ≥ length xs"
  @have "xs = take l xs @ sublist l (r + 1) xs @ drop (r + 1) xs"
  @have "xs' = take l xs' @ sublist l (r + 1) xs' @ drop (r + 1) xs'"
  @have "take l xs = take l xs'"
  @have "drop (r + 1) xs = drop (r + 1) xs'"
@qed

lemma quicksort_sorts [forward_arg]:
  "r < length xs ⟹ sorted (sublist l (r + 1) (quicksort xs l r))"
@proof @fun_induct "quicksort xs l r"
  @case "l ≥ r" @with @case "l = r" @end
  @case "r ≥ length xs"
  @let "p = fst (partition xs l r)"
  @let "xs1 = snd (partition xs l r)"
  @let "xs2 = quicksort xs1 l (p - 1)"
  @let "xs3 = quicksort xs2 (p + 1) r"
  @have "sorted (sublist l (r + 1) xs3)" @with
    @have "l ≤ p" @have "p + 1 ≤ r + 1" @have "r + 1 ≤ length xs3"
    @have "sublist l p xs2 = sublist l p xs3"
    @have "set (sublist l p xs1) = set (sublist l p xs2)"
    @have "sublist (p + 1) (r + 1) xs1 = sublist (p + 1) (r + 1) xs2"
    @have "set (sublist (p + 1) (r + 1) xs2) = set (sublist (p + 1) (r + 1) xs3)"
    @have "∀x∈set (sublist l p xs3). x ≤ xs3 ! p"
    @have "∀x∈set (sublist (p + 1) (r + 1) xs3). x ≥ xs3 ! p"
    @have "sorted (sublist l p xs3)"
    @have "sorted (sublist (p + 1) (r + 1) xs3)"
    @have "sublist l (r + 1) xs3 = sublist l p xs3 @ (xs3 ! p) # sublist (p + 1) (r + 1) xs3"
  @end
  @unfold "quicksort xs l r"
@qed

text ‹Main result: correctness of functional quicksort.›
theorem quicksort_sorts_all [rewrite]:
  "xs ≠ [] ⟹ quicksort xs 0 (length xs - 1) = sort xs"
@proof
  @let "xs' = quicksort xs 0 (length xs - 1)"
  @have "sublist 0 (length xs - 1 + 1) xs' = xs'"
@qed

end