Quelle Imperative_Quicksort.thy Sprache: Isabelle

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

section \<open>An imperative implementation of Quicksort on arrays\<close>

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

text \<open>We prove QuickSort correct in the Relational Calculus.\<close>

definition swap :: "'a::heap array \ nat \ nat \ unit Heap"
where
 "swap arr i j =
 do {
 x \<leftarrow> Array.nth arr i;
 y \<leftarrow> 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 \<le> left) then return right
 else do {
 v \<leftarrow> Array.nth a left;
 (if (v \<le> 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 = \<open>effect (part1 a l r p) h h' rs\<close>
 show ?case
 proof (cases "r \ l")
 case True (* Terminating case *)
 with cr \<open>l \<le> r\<close> 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 \<open>l + 1 \<le> r\<close>]
 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 \<open>l \<le> r - 1\<close>] 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 = \<open>effect (part1 a l r p) h h' rs\<close>

 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 effect (part1 a l r p) h h' rs\<close>

 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)
 \<and> (\<forall>i. rs i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> 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 = \<open>effect (part1 a l r p) h h' rs\<close>

 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 \<leftarrow> Array.nth a right;
 middle \<leftarrow> part1 a left (right - 1) pivot;
 v \<leftarrow> Array.nth a middle;
 m \<leftarrow> return (if (v \<le> 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 \<open>l < r\<close> have "l \<le> r - 1" by arith
 from part_returns_index_in_bounds[OF part this] rs_equals \<open>l < r\<close> 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) \
 (\<forall>i. rs i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> 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 \<open>l < r\<close> have "l \<le> r - 1" by simp
 note middle_in_bounds = part_returns_index_in_bounds[OF part this]
 from part_outer_remains[OF part] \<open>l < r\<close>
 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 \<open>l < r\<close>
 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 \<le> 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 l < r\<close> have "Suc middle \<le> 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 \<le> 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 \<leftarrow> partition arr left right;
 pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> 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 effect (quicksort a l r) h h' rs\<close>
 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 = \<open>effect (quicksort a l r) h h' rs\<close>
 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 \<dots> *)
 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 \<open>No Errors in quicksort\<close>
text \<open>We have proved that quicksort sorts (if no exceptions occur).
We will now show that exceptions do not occur.\<close>

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 \<open>Example\<close>

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

code_reserved (SML) upto

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

ML_val \<open>@{code example} ()\<close>

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

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.37Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.