Theory Imperative_Quicksort

(*  Title:      HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹An imperative implementation of Quicksort on arrays›

theory Imperative_Quicksort
imports
  "../Imperative_HOL"
  Subarray
  "HOL-Library.Multiset"
  "HOL-Library.Code_Target_Numeral"
begin

text ‹We prove QuickSort correct in the Relational Calculus.›

definition swap :: "'a::heap array ⇒ nat ⇒ nat ⇒ unit Heap"
where
  "swap arr i j =
     do {
       x ← Array.nth arr i;
       y ← Array.nth arr j;
       Array.upd i y arr;
       Array.upd j x arr;
       return ()
     }"

lemma effect_swapI [effect_intros]:
  assumes "i < Array.length h a" "j < Array.length h a"
    "x = Array.get h a ! i" "y = Array.get h a ! j"
    "h' = Array.update a j x (Array.update a i y h)"
  shows "effect (swap a i j) h h' r"
  unfolding swap_def using assms by (auto intro!: effect_intros)

lemma swap_permutes:
  assumes "effect (swap a i j) h h' rs"
  shows "mset (Array.get h' a) 
  = mset (Array.get h a)"
  using assms
  unfolding swap_def
  by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)

function part1 :: "'a::{heap,ord} array ⇒ nat ⇒ nat ⇒ 'a ⇒ nat Heap"
where
  "part1 a left right p = (
     if (right ≤ left) then return right
     else do {
       v ← Array.nth a left;
       (if (v ≤ p) then (part1 a (left + 1) right p)
                    else (do { swap a left right;
  part1 a left (right - 1) p }))
     })"
by pat_completeness auto

termination
by (relation "measure (λ(_,l,r,_). r - l )") auto

declare part1.simps[simp del]

lemma part_permutes:
  assumes "effect (part1 a l r p) h h' rs"
  shows "mset (Array.get h' a) 
  = mset (Array.get h a)"
  using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  case (1 a l r p h h' rs)
  thus ?case
    unfolding part1.simps [of a l r p]
    by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
qed

lemma part_returns_index_in_bounds:
  assumes "effect (part1 a l r p) h h' rs"
  assumes "l ≤ r"
  shows "l ≤ rs ∧ rs ≤ r"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  case (1 a l r p h h' rs)
  note cr = ‹effect (part1 a l r p) h h' rs›
  show ?case
  proof (cases "r ≤ l")
    case True (* Terminating case *)
    with cr ‹l ≤ r› show ?thesis
      unfolding part1.simps[of a l r p]
      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
  next
    case False (* recursive case *)
    note rec_condition = this
    let ?v = "Array.get h a ! l"
    show ?thesis
    proof (cases "?v ≤ p")
      case True
      with cr False
      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from rec_condition have "l + 1 ≤ r" by arith
      from 1(1)[OF rec_condition True rec1 ‹l + 1 ≤ r›]
      show ?thesis by simp
    next
      case False
      with rec_condition cr
      obtain h1 where swp: "effect (swap a l r) h h1 ()"
        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from rec_condition have "l ≤ r - 1" by arith
      from 1(2) [OF rec_condition False rec2 ‹l ≤ r - 1›] show ?thesis by fastforce
    qed
  qed
qed

lemma part_length_remains:
  assumes "effect (part1 a l r p) h h' rs"
  shows "Array.length h a = Array.length h' a"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  case (1 a l r p h h' rs)
  note cr = ‹effect (part1 a l r p) h h' rs›
  
  show ?case
  proof (cases "r ≤ l")
    case True (* Terminating case *)
    with cr show ?thesis
      unfolding part1.simps[of a l r p]
      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
  next
    case False (* recursive case *)
    with cr 1 show ?thesis
      unfolding part1.simps [of a l r p] swap_def
      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce
  qed
qed

lemma part_outer_remains:
  assumes "effect (part1 a l r p) h h' rs"
  shows "∀i. i < l ∨ r < i ⟶ Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
  using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  case (1 a l r p h h' rs)
  note cr = ‹effect (part1 a l r p) h h' rs›
  
  show ?case
  proof (cases "r ≤ l")
    case True (* Terminating case *)
    with cr show ?thesis
      unfolding part1.simps[of a l r p]
      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
  next
    case False (* recursive case *)
    note rec_condition = this
    let ?v = "Array.get h a ! l"
    show ?thesis
    proof (cases "?v ≤ p")
      case True
      with cr False
      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from 1(1)[OF rec_condition True rec1]
      show ?thesis by fastforce
    next
      case False
      with rec_condition cr
      obtain h1 where swp: "effect (swap a l r) h h1 ()"
        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from swp rec_condition have
        "∀i. i < l ∨ r < i ⟶ Array.get h a ! i = Array.get h1 a ! i"
        unfolding swap_def
        by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
      with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce
    qed
  qed
qed


lemma part_partitions:
  assumes "effect (part1 a l r p) h h' rs"
  shows "(∀i. l ≤ i ∧ i < rs ⟶ Array.get h' (a::'a::{heap,linorder} array) ! i ≤ p)
  ∧ (∀i. rs < i ∧ i ≤ r ⟶ Array.get h' a ! i ≥ p)"
  using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  case (1 a l r p h h' rs)
  note cr = ‹effect (part1 a l r p) h h' rs›
  
  show ?case
  proof (cases "r ≤ l")
    case True (* Terminating case *)
    with cr have "rs = r"
      unfolding part1.simps[of a l r p]
      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
    with True
    show ?thesis by auto
  next
    case False (* recursive case *)
    note lr = this
    let ?v = "Array.get h a ! l"
    show ?thesis
    proof (cases "?v ≤ p")
      case True
      with lr cr
      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l ≤ p"
        by fastforce
      have "∀i. (l ≤ i = (l = i ∨ Suc l ≤ i))" by arith
      with 1(1)[OF False True rec1] a_l show ?thesis
        by auto
    next
      case False
      with lr cr
      obtain h1 where swp: "effect (swap a l r) h h1 ()"
        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
        unfolding part1.simps[of a l r p]
        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
      from swp False have "Array.get h1 a ! r ≥ p"
        unfolding swap_def
        by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
      with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r ≥ p"
        by fastforce
      have "∀i. (i ≤ r = (i = r ∨ i ≤ r - 1))" by arith
      with 1(2)[OF lr False rec2] a_r show ?thesis
        by auto
    qed
  qed
qed


fun partition :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ nat Heap"
where
  "partition a left right = do {
     pivot ← Array.nth a right;
     middle ← part1 a left (right - 1) pivot;
     v ← Array.nth a middle;
     m ← return (if (v ≤ pivot) then (middle + 1) else middle);
     swap a m right;
     return m
   }"

declare partition.simps[simp del]

lemma partition_permutes:
  assumes "effect (partition a l r) h h' rs"
  shows "mset (Array.get h' a) 
  = mset (Array.get h a)"
proof -
    from assms part_permutes swap_permutes show ?thesis
      unfolding partition.simps
      by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
qed

lemma partition_length_remains:
  assumes "effect (partition a l r) h h' rs"
  shows "Array.length h a = Array.length h' a"
proof -
  from assms part_length_remains show ?thesis
    unfolding partition.simps swap_def
    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
qed

lemma partition_outer_remains:
  assumes "effect (partition a l r) h h' rs"
  assumes "l < r"
  shows "∀i. i < l ∨ r < i ⟶ Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
proof -
  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
    unfolding partition.simps swap_def
    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
qed

lemma partition_returns_index_in_bounds:
  assumes effect: "effect (partition a l r) h h' rs"
  assumes "l < r"
  shows "l ≤ rs ∧ rs ≤ r"
proof -
  from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
    and rs_equals: "rs = (if Array.get h'' a ! middle ≤ Array.get h a ! r then middle + 1
         else middle)"
    unfolding partition.simps
    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp 
  from ‹l < r› have "l ≤ r - 1" by arith
  from part_returns_index_in_bounds[OF part this] rs_equals ‹l < r› show ?thesis by auto
qed

lemma partition_partitions:
  assumes effect: "effect (partition a l r) h h' rs"
  assumes "l < r"
  shows "(∀i. l ≤ i ∧ i < rs ⟶ Array.get h' (a::'a::{heap,linorder} array) ! i ≤ Array.get h' a ! rs) ∧
  (∀i. rs < i ∧ i ≤ r ⟶ Array.get h' a ! rs ≤ Array.get h' a ! i)"
proof -
  let ?pivot = "Array.get h a ! r" 
  from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
    and swap: "effect (swap a rs r) h1 h' ()"
    and rs_equals: "rs = (if Array.get h1 a ! middle ≤ ?pivot then middle + 1
         else middle)"
    unfolding partition.simps
    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
  from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
    (Array.update a rs (Array.get h1 a ! r) h1)"
    unfolding swap_def
    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
  from swap have in_bounds: "r < Array.length h1 a ∧ rs < Array.length h1 a"
    unfolding swap_def
    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
  from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
    unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
  from ‹l < r› have "l ≤ r - 1" by simp
  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
  from part_outer_remains[OF part] ‹l < r›
  have "Array.get h a ! r = Array.get h1 a ! r"
    by fastforce
  with swap
  have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
    unfolding swap_def
    by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
  from part_partitions [OF part]
  show ?thesis
  proof (cases "Array.get h1 a ! middle ≤ ?pivot")
    case True
    with rs_equals have rs_equals: "rs = middle + 1" by simp
    { 
      fix i
      assume i_is_left: "l ≤ i ∧ i < rs"
      with swap_length_remains in_bounds middle_in_bounds rs_equals ‹l < r›
      have i_props: "i < Array.length h' a" "i ≠ r" "i ≠ rs" by auto
      from i_is_left rs_equals have "l ≤ i ∧ i < middle ∨ i = middle" by arith
      with part_partitions[OF part] right_remains True
      have "Array.get h1 a ! i ≤ Array.get h' a ! rs" by fastforce
      with i_props h'_def in_bounds have "Array.get h' a ! i ≤ Array.get h' a ! rs"
        unfolding Array.update_def Array.length_def by simp
    }
    moreover
    {
      fix i
      assume "rs < i ∧ i ≤ r"

      hence "(rs < i ∧ i ≤ r - 1) ∨ (rs < i ∧ i = r)" by arith
      hence "Array.get h' a ! rs ≤ Array.get h' a ! i"
      proof
        assume i_is: "rs < i ∧ i ≤ r - 1"
        with swap_length_remains in_bounds middle_in_bounds rs_equals
        have i_props: "i < Array.length h' a" "i ≠ r" "i ≠ rs" by auto
        from part_partitions[OF part] rs_equals right_remains i_is
        have "Array.get h' a ! rs ≤ Array.get h1 a ! i"
          by fastforce
        with i_props h'_def show ?thesis by fastforce
      next
        assume i_is: "rs < i ∧ i = r"
        with rs_equals have "Suc middle ≠ r" by arith
        with middle_in_bounds ‹l < r› have "Suc middle ≤ r - 1" by arith
        with part_partitions[OF part] right_remains 
        have "Array.get h' a ! rs ≤ Array.get h1 a ! (Suc middle)"
          by fastforce
        with i_is True rs_equals right_remains h'_def
        show ?thesis using in_bounds
          unfolding Array.update_def Array.length_def
          by auto
      qed
    }
    ultimately show ?thesis by auto
  next
    case False
    with rs_equals have rs_equals: "middle = rs" by simp
    { 
      fix i
      assume i_is_left: "l ≤ i ∧ i < rs"
      with swap_length_remains in_bounds middle_in_bounds rs_equals
      have i_props: "i < Array.length h' a" "i ≠ r" "i ≠ rs" by auto
      from part_partitions[OF part] rs_equals right_remains i_is_left
      have "Array.get h1 a ! i ≤ Array.get h' a ! rs" by fastforce
      with i_props h'_def have "Array.get h' a ! i ≤ Array.get h' a ! rs"
        unfolding Array.update_def by simp
    }
    moreover
    {
      fix i
      assume "rs < i ∧ i ≤ r"
      hence "(rs < i ∧ i ≤ r - 1) ∨ i = r" by arith
      hence "Array.get h' a ! rs ≤ Array.get h' a ! i"
      proof
        assume i_is: "rs < i ∧ i ≤ r - 1"
        with swap_length_remains in_bounds middle_in_bounds rs_equals
        have i_props: "i < Array.length h' a" "i ≠ r" "i ≠ rs" by auto
        from part_partitions[OF part] rs_equals right_remains i_is
        have "Array.get h' a ! rs ≤ Array.get h1 a ! i"
          by fastforce
        with i_props h'_def show ?thesis by fastforce
      next
        assume i_is: "i = r"
        from i_is False rs_equals right_remains h'_def
        show ?thesis using in_bounds
          unfolding Array.update_def Array.length_def
          by auto
      qed
    }
    ultimately
    show ?thesis by auto
  qed
qed


function quicksort :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ unit Heap"
where
  "quicksort arr left right =
     (if (right > left)  then
        do {
          pivotNewIndex ← partition arr left right;
          pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;
          quicksort arr left (pivotNewIndex - 1);
          quicksort arr (pivotNewIndex + 1) right
        }
     else return ())"
by pat_completeness auto

(* For termination, we must show that the pivotNewIndex is between left and right *) 
termination
by (relation "measure (λ(a, l, r). (r - l))") auto

declare quicksort.simps[simp del]


lemma quicksort_permutes:
  assumes "effect (quicksort a l r) h h' rs"
  shows "mset (Array.get h' a) 
  = mset (Array.get h a)"
  using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  case (1 a l r h h' rs)
  with partition_permutes show ?case
    unfolding quicksort.simps [of a l r]
    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
qed

lemma length_remains:
  assumes "effect (quicksort a l r) h h' rs"
  shows "Array.length h a = Array.length h' a"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  case (1 a l r h h' rs)
  with partition_length_remains show ?case
    unfolding quicksort.simps [of a l r]
    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) fastforce+
qed

lemma quicksort_outer_remains:
  assumes "effect (quicksort a l r) h h' rs"
   shows "∀i. i < l ∨ r < i ⟶ Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
  using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  case (1 a l r h h' rs)
  note cr = ‹effect (quicksort a l r) h h' rs›
  thus ?case
  proof (cases "r > l")
    case False
    with cr have "h' = h"
      unfolding quicksort.simps [of a l r]
      by (elim effect_ifE effect_returnE) auto
    thus ?thesis by simp
  next
  case True
   { 
      fix h1 h2 p ret1 ret2 i
      assume part: "effect (partition a l r) h h1 p"
      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
      assume pivot: "l ≤ p ∧ p ≤ r"
      assume i_outer: "i < l ∨ r < i"
      from  partition_outer_remains [OF part True] i_outer
      have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce
      moreover
      from 1(1) [OF True pivot qs1] pivot i_outer 2
      have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto
      moreover
      from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3
      have "Array.get h2 a ! i = Array.get h' a ! i" by auto
      ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
    }
    with cr show ?thesis
      unfolding quicksort.simps [of a l r]
      by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
  qed
qed

lemma quicksort_is_skip:
  assumes "effect (quicksort a l r) h h' rs"
  shows "r ≤ l ⟶ h = h'"
  using assms
  unfolding quicksort.simps [of a l r]
  by (elim effect_ifE effect_returnE) auto
 
lemma quicksort_sorts:
  assumes "effect (quicksort a l r) h h' rs"
  assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
  shows "sorted (subarray l (r + 1) a h')"
  using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  case (1 a l r h h' rs)
  note cr = ‹effect (quicksort a l r) h h' rs›
  thus ?case
  proof (cases "r > l")
    case False
    hence "l ≥ r + 1 ∨ l = r" by arith 
    with length_remains[OF cr] 1(5) show ?thesis
      by (auto simp add: subarray_Nil subarray_single)
  next
    case True
    { 
      fix h1 h2 p
      assume part: "effect (partition a l r) h h1 p"
      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
      from partition_returns_index_in_bounds [OF part True]
      have pivot: "l≤ p ∧ p ≤ r" .
     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
      have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto)
        (*-- First of all, by induction hypothesis both sublists are sorted. *)
      from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
      from quicksort_outer_remains [OF qs2] length_remains
      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
        by (simp add: subarray_eq_samelength_iff)
      with IH1 have IH1': "sorted (subarray l p a h')" by simp
      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
        by (cases "Suc p ≤ r", auto simp add: subarray_Nil)
           (* -- Secondly, both sublists remain partitioned. *)
      from partition_partitions[OF part True]
      have part_conds1: "∀j. j ∈ set (subarray l p a h1) ⟶ j ≤ Array.get h1 a ! p "
        and part_conds2: "∀j. j ∈ set (subarray (p + 1) (r + 1) a h1) ⟶ Array.get h1 a ! p ≤ j"
        by (auto simp add: all_in_set_subarray_conv)
      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
        length_remains 1(5) pivot mset_nths [of l p "Array.get h1 a" "Array.get h2 a"]
      have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
        unfolding Array.length_def subarray_def by (cases p, auto)
      with left_subarray_remains part_conds1 pivot_unchanged
      have part_conds2': "∀j. j ∈ set (subarray l p a h') ⟶ j ≤ Array.get h' a ! p"
        by (simp, subst set_mset_mset[symmetric], simp)
          (* -- These steps are the analogous for the right sublist … *)
      from quicksort_outer_remains [OF qs1] length_remains
      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
        by (auto simp add: subarray_eq_samelength_iff)
      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
        length_remains 1(5) pivot mset_nths [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
      have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
        unfolding Array.length_def subarray_def by auto
      with right_subarray_remains part_conds2 pivot_unchanged
      have part_conds1': "∀j. j ∈ set (subarray (p + 1) (r + 1) a h') ⟶ Array.get h' a ! p ≤ j"
        by (simp, subst set_mset_mset[symmetric], simp)
          (* -- Thirdly and finally, we show that the array is sorted
          following from the facts above. *)
      from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
        by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
        unfolding subarray_def
        apply (auto simp add: sorted_append all_in_set_nths'_conv)
        by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
    }
    with True cr show ?thesis
      unfolding quicksort.simps [of a l r]
      by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
  qed
qed


lemma quicksort_is_sort:
  assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
  shows "Array.get h' a = sort (Array.get h a)"
proof (cases "Array.get h a = []")
  case True
  with quicksort_is_skip[OF effect] show ?thesis
  unfolding Array.length_def by simp
next
  case False
  from quicksort_sorts [OF effect] False have "sorted (nths' 0 (List.length (Array.get h a)) (Array.get h' a))"
    unfolding Array.length_def subarray_def by auto
  with length_remains[OF effect] have "sorted (Array.get h' a)"
    unfolding Array.length_def by simp
  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce
qed

subsection ‹No Errors in quicksort›
text ‹We have proved that quicksort sorts (if no exceptions occur).
We will now show that exceptions do not occur.›

lemma success_part1I: 
  assumes "l < Array.length h a" "r < Array.length h a"
  shows "success (part1 a l r p) h"
  using assms
proof (induct a l r p arbitrary: h rule: part1.induct)
  case (1 a l r p)
  thus ?case unfolding part1.simps [of a l r]
  apply (auto intro!: success_intros simp add: not_le)
  apply (auto intro!: effect_intros)
  done
qed

lemma success_bindI' [success_intros]: (*FIXME move*)
  assumes "success f h"
  assumes "⋀h' r. effect f h h' r ⟹ success (g r) h'"
  shows "success (f ⤜ g) h"
using assms(1) proof (rule success_effectE)
  fix h' r
  assume *: "effect f h h' r"
  with assms(2) have "success (g r) h'" .
  with * show "success (f ⤜ g) h" by (rule success_bind_effectI)
qed

lemma success_partitionI:
  assumes "l < r" "l < Array.length h a" "r < Array.length h a"
  shows "success (partition a l r) h"
using assms unfolding partition.simps swap_def
apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: effect_bindE effect_updE effect_nthE effect_returnE simp add:)
apply (frule part_length_remains)
apply (frule part_returns_index_in_bounds)
apply auto
apply (frule part_length_remains)
apply (frule part_returns_index_in_bounds)
apply auto
apply (frule part_length_remains)
apply auto
done

lemma success_quicksortI:
  assumes "l < Array.length h a" "r < Array.length h a"
  shows "success (quicksort a l r) h"
using assms
proof (induct a l r arbitrary: h rule: quicksort.induct)
  case (1 a l ri h)
  thus ?case
    unfolding quicksort.simps [of a l ri]
    apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI)
    apply (frule partition_returns_index_in_bounds)
    apply auto
    apply (frule partition_returns_index_in_bounds)
    apply auto
    apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
    apply (subgoal_tac "Suc r ≤ ri ∨ r = ri") 
    apply (erule disjE)
    apply auto
    unfolding quicksort.simps [of a "Suc ri" ri]
    apply (auto intro!: success_ifI success_returnI)
    done
qed


subsection ‹Example›

definition "qsort a = do {
    k ← Array.len a;
    quicksort a 0 (k - 1);
    return a
  }"

code_reserved SML upto

definition "example = do {
    a ← Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);
    qsort a
  }"

ML_val ‹@{code example} ()›

export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp

end