Theory Quicksort_Impl

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

section ‹Implementation of quicksort›

theory Quicksort_Impl
  imports Arrays_Impl "../Functional/Quicksort"
begin

text ‹
  Imperative implementation of quicksort. Also verified in
  theory Imperative\_Quicksort in HOL/Imperative\_HOL/ex
  in the Isabelle library.
›

partial_function (heap) part1 :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ 'a ⇒ nat Heap" where
  "part1 a l r p = (
     if r ≤ l then return r
     else do {
       v ← Array.nth a l;
       if v ≤ p then
         part1 a (l + 1) r p
       else do {
         swap a l r;
         part1 a l (r - 1) p }})"

lemma part1_to_fun [hoare_triple]:
  "r < length xs ⟹ <p ↦⇩a xs>
   part1 p l r a
   <λrs. p ↦⇩a snd (Quicksort.part1 xs l r a) * ↑(rs = fst (Quicksort.part1 xs l r a))>"
@proof @fun_induct "Quicksort.part1 xs l r a" @unfold "Quicksort.part1 xs l r a" @qed

text ‹Partition function›
definition partition :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ nat Heap" where
  "partition a l r = do {
     p ← Array.nth a r;
     m ← part1 a l (r - 1) p;
     v ← Array.nth a m;
     m' ← return (if v ≤ p then m + 1 else m);
     swap a m' r;
     return m'
   }"

lemma partition_to_fun [hoare_triple]:
  "l < r ⟹ r < length xs ⟹ <a ↦⇩a xs>
   partition a l r
   <λrs. a ↦⇩a snd (Quicksort.partition xs l r) * ↑(rs = fst (Quicksort.partition xs l r))>"
@proof @unfold "Quicksort.partition xs l r" @qed

text ‹Quicksort function›
partial_function (heap) quicksort :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ unit Heap" where
  "quicksort a l r = do {
     len ← Array.len a;
     if l ≥ r then return ()
     else if r < len then do {
       p ← partition a l r;
       quicksort a l (p - 1);
       quicksort a (p + 1) r
     }
     else return ()
   }"

lemma quicksort_to_fun [hoare_triple]:
  "r < length xs ⟹ <a ↦⇩a xs>
   quicksort a l r
   <λ_. a ↦⇩a Quicksort.quicksort xs l r>"
@proof @fun_induct "Quicksort.quicksort xs l r" @unfold "Quicksort.quicksort xs l r" @qed

definition quicksort_all :: "('a::{heap,linorder}) array ⇒ unit Heap" where
  "quicksort_all a = do {
     n ← Array.len a;
     if n = 0 then return ()
     else quicksort a 0 (n - 1)
   }"

text ‹Correctness of quicksort.›
theorem quicksort_sorts_basic [hoare_triple]:
  "<a ↦⇩a xs>
   quicksort_all a
   <λ_. a ↦⇩a sort xs>" by auto2

end