imports Imperative_HOL Subarray Code_Target_Numeral

(* 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 "~~/src/HOL/Imperative_HOL/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 sorted_Cons 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