bulwahn@36098: (* Title: HOL/Imperative_HOL/ex/Imperative_Quicksort.thy bulwahn@36098: Author: Lukas Bulwahn, TU Muenchen bulwahn@36098: *) bulwahn@36098: wenzelm@58889: section {* An imperative implementation of Quicksort on arrays *} haftmann@30689: haftmann@30689: theory Imperative_Quicksort wenzelm@41413: imports huffman@47108: "~~/src/HOL/Imperative_HOL/Imperative_HOL" wenzelm@41413: Subarray wenzelm@41413: "~~/src/HOL/Library/Multiset" haftmann@51143: "~~/src/HOL/Library/Code_Target_Numeral" bulwahn@27656: begin bulwahn@27656: bulwahn@27656: text {* We prove QuickSort correct in the Relational Calculus. *} bulwahn@27656: bulwahn@27656: definition swap :: "nat array \ nat \ nat \ unit Heap" bulwahn@27656: where krauss@37792: "swap arr i j = krauss@37792: do { haftmann@37798: x \ Array.nth arr i; haftmann@37798: y \ Array.nth arr j; haftmann@37798: Array.upd i y arr; haftmann@37798: Array.upd j x arr; bulwahn@27656: return () krauss@37792: }" bulwahn@27656: haftmann@40671: lemma effect_swapI [effect_intros]: haftmann@37802: assumes "i < Array.length h a" "j < Array.length h a" haftmann@37806: "x = Array.get h a ! i" "y = Array.get h a ! j" haftmann@37798: "h' = Array.update a j x (Array.update a i y h)" haftmann@40671: shows "effect (swap a i j) h h' r" haftmann@40671: unfolding swap_def using assms by (auto intro!: effect_intros) haftmann@37771: bulwahn@27656: lemma swap_permutes: haftmann@40671: assumes "effect (swap a i j) h h' rs" haftmann@37806: shows "multiset_of (Array.get h' a) haftmann@37806: = multiset_of (Array.get h a)" bulwahn@27656: using assms haftmann@28145: unfolding swap_def haftmann@40671: by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE) bulwahn@27656: bulwahn@27656: function part1 :: "nat array \ nat \ nat \ nat \ nat Heap" bulwahn@27656: where bulwahn@27656: "part1 a left right p = ( bulwahn@27656: if (right \ left) then return right krauss@37792: else do { haftmann@37798: v \ Array.nth a left; bulwahn@27656: (if (v \ p) then (part1 a (left + 1) right p) krauss@37792: else (do { swap a left right; krauss@37792: part1 a left (right - 1) p })) krauss@37792: })" bulwahn@27656: by pat_completeness auto bulwahn@27656: bulwahn@27656: termination bulwahn@27656: by (relation "measure (\(_,l,r,_). r - l )") auto bulwahn@27656: bulwahn@27656: declare part1.simps[simp del] bulwahn@27656: bulwahn@27656: lemma part_permutes: haftmann@40671: assumes "effect (part1 a l r p) h h' rs" haftmann@37806: shows "multiset_of (Array.get h' a) haftmann@37806: = multiset_of (Array.get h a)" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h h' rs rule:part1.induct) bulwahn@27656: case (1 a l r p h h' rs) bulwahn@27656: thus ?case haftmann@28145: unfolding part1.simps [of a l r p] haftmann@40671: by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes) bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma part_returns_index_in_bounds: haftmann@40671: assumes "effect (part1 a l r p) h h' rs" bulwahn@27656: assumes "l \ r" bulwahn@27656: shows "l \ rs \ rs \ r" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h h' rs rule:part1.induct) bulwahn@27656: case (1 a l r p h h' rs) haftmann@40671: note cr = `effect (part1 a l r p) h h' rs` bulwahn@27656: show ?case bulwahn@27656: proof (cases "r \ l") bulwahn@27656: case True (* Terminating case *) bulwahn@27656: with cr `l \ r` show ?thesis haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto bulwahn@27656: next bulwahn@27656: case False (* recursive case *) bulwahn@27656: note rec_condition = this haftmann@37806: let ?v = "Array.get h a ! l" bulwahn@27656: show ?thesis bulwahn@27656: proof (cases "?v \ p") bulwahn@27656: case True bulwahn@27656: with cr False haftmann@40671: have rec1: "effect (part1 a (l + 1) r p) h h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto bulwahn@27656: from rec_condition have "l + 1 \ r" by arith bulwahn@27656: from 1(1)[OF rec_condition True rec1 `l + 1 \ r`] bulwahn@27656: show ?thesis by simp bulwahn@27656: next bulwahn@27656: case False bulwahn@27656: with rec_condition cr haftmann@40671: obtain h1 where swp: "effect (swap a l r) h h1 ()" haftmann@40671: and rec2: "effect (part1 a l (r - 1) p) h1 h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto bulwahn@27656: from rec_condition have "l \ r - 1" by arith nipkow@44890: from 1(2) [OF rec_condition False rec2 `l \ r - 1`] show ?thesis by fastforce bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma part_length_remains: haftmann@40671: assumes "effect (part1 a l r p) h h' rs" haftmann@37802: shows "Array.length h a = Array.length h' a" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h h' rs rule:part1.induct) bulwahn@27656: case (1 a l r p h h' rs) haftmann@40671: note cr = `effect (part1 a l r p) h h' rs` bulwahn@27656: bulwahn@27656: show ?case bulwahn@27656: proof (cases "r \ l") bulwahn@27656: case True (* Terminating case *) bulwahn@27656: with cr show ?thesis haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto bulwahn@27656: next bulwahn@27656: case False (* recursive case *) bulwahn@27656: with cr 1 show ?thesis haftmann@28145: unfolding part1.simps [of a l r p] swap_def nipkow@44890: by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma part_outer_remains: haftmann@40671: assumes "effect (part1 a l r p) h h' rs" haftmann@37806: shows "\i. i < l \ r < i \ Array.get h (a::nat array) ! i = Array.get h' a ! i" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h h' rs rule:part1.induct) bulwahn@27656: case (1 a l r p h h' rs) haftmann@40671: note cr = `effect (part1 a l r p) h h' rs` bulwahn@27656: bulwahn@27656: show ?case bulwahn@27656: proof (cases "r \ l") bulwahn@27656: case True (* Terminating case *) bulwahn@27656: with cr show ?thesis haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto bulwahn@27656: next bulwahn@27656: case False (* recursive case *) bulwahn@27656: note rec_condition = this haftmann@37806: let ?v = "Array.get h a ! l" bulwahn@27656: show ?thesis bulwahn@27656: proof (cases "?v \ p") bulwahn@27656: case True bulwahn@27656: with cr False haftmann@40671: have rec1: "effect (part1 a (l + 1) r p) h h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto bulwahn@27656: from 1(1)[OF rec_condition True rec1] nipkow@44890: show ?thesis by fastforce bulwahn@27656: next bulwahn@27656: case False bulwahn@27656: with rec_condition cr haftmann@40671: obtain h1 where swp: "effect (swap a l r) h h1 ()" haftmann@40671: and rec2: "effect (part1 a l (r - 1) p) h1 h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto bulwahn@27656: from swp rec_condition have haftmann@37806: "\i. i < l \ r < i \ Array.get h a ! i = Array.get h1 a ! i" wenzelm@32960: unfolding swap_def haftmann@40671: by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto nipkow@44890: with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: bulwahn@27656: lemma part_partitions: haftmann@40671: assumes "effect (part1 a l r p) h h' rs" haftmann@37806: shows "(\i. l \ i \ i < rs \ Array.get h' (a::nat array) ! i \ p) haftmann@37806: \ (\i. rs < i \ i \ r \ Array.get h' a ! i \ p)" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h h' rs rule:part1.induct) bulwahn@27656: case (1 a l r p h h' rs) haftmann@40671: note cr = `effect (part1 a l r p) h h' rs` bulwahn@27656: bulwahn@27656: show ?case bulwahn@27656: proof (cases "r \ l") bulwahn@27656: case True (* Terminating case *) bulwahn@27656: with cr have "rs = r" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto bulwahn@27656: with True bulwahn@27656: show ?thesis by auto bulwahn@27656: next bulwahn@27656: case False (* recursive case *) bulwahn@27656: note lr = this haftmann@37806: let ?v = "Array.get h a ! l" bulwahn@27656: show ?thesis bulwahn@27656: proof (cases "?v \ p") bulwahn@27656: case True bulwahn@27656: with lr cr haftmann@40671: have rec1: "effect (part1 a (l + 1) r p) h h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto haftmann@37806: from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \ p" nipkow@44890: by fastforce bulwahn@27656: have "\i. (l \ i = (l = i \ Suc l \ i))" by arith bulwahn@27656: with 1(1)[OF False True rec1] a_l show ?thesis wenzelm@32960: by auto bulwahn@27656: next bulwahn@27656: case False bulwahn@27656: with lr cr haftmann@40671: obtain h1 where swp: "effect (swap a l r) h h1 ()" haftmann@40671: and rec2: "effect (part1 a l (r - 1) p) h1 h' rs" haftmann@28145: unfolding part1.simps[of a l r p] haftmann@40671: by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto haftmann@37806: from swp False have "Array.get h1 a ! r \ p" wenzelm@32960: unfolding swap_def haftmann@40671: by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE) haftmann@37806: with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \ p" nipkow@44890: by fastforce bulwahn@27656: have "\i. (i \ r = (i = r \ i \ r - 1))" by arith bulwahn@27656: with 1(2)[OF lr False rec2] a_r show ?thesis wenzelm@32960: by auto bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: bulwahn@27656: fun partition :: "nat array \ nat \ nat \ nat Heap" bulwahn@27656: where krauss@37792: "partition a left right = do { haftmann@37798: pivot \ Array.nth a right; bulwahn@27656: middle \ part1 a left (right - 1) pivot; haftmann@37798: v \ Array.nth a middle; bulwahn@27656: m \ return (if (v \ pivot) then (middle + 1) else middle); bulwahn@27656: swap a m right; bulwahn@27656: return m krauss@37792: }" bulwahn@27656: bulwahn@27656: declare partition.simps[simp del] bulwahn@27656: bulwahn@27656: lemma partition_permutes: haftmann@40671: assumes "effect (partition a l r) h h' rs" haftmann@37806: shows "multiset_of (Array.get h' a) haftmann@37806: = multiset_of (Array.get h a)" bulwahn@27656: proof - bulwahn@27656: from assms part_permutes swap_permutes show ?thesis haftmann@28145: unfolding partition.simps haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma partition_length_remains: haftmann@40671: assumes "effect (partition a l r) h h' rs" haftmann@37802: shows "Array.length h a = Array.length h' a" bulwahn@27656: proof - bulwahn@27656: from assms part_length_remains show ?thesis haftmann@28145: unfolding partition.simps swap_def haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma partition_outer_remains: haftmann@40671: assumes "effect (partition a l r) h h' rs" bulwahn@27656: assumes "l < r" haftmann@37806: shows "\i. i < l \ r < i \ Array.get h (a::nat array) ! i = Array.get h' a ! i" bulwahn@27656: proof - bulwahn@27656: from assms part_outer_remains part_returns_index_in_bounds show ?thesis haftmann@28145: unfolding partition.simps swap_def nipkow@44890: by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma partition_returns_index_in_bounds: haftmann@40671: assumes effect: "effect (partition a l r) h h' rs" bulwahn@27656: assumes "l < r" bulwahn@27656: shows "l \ rs \ rs \ r" bulwahn@27656: proof - haftmann@40671: from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle" haftmann@37806: and rs_equals: "rs = (if Array.get h'' a ! middle \ Array.get h a ! r then middle + 1 bulwahn@27656: else middle)" haftmann@28145: unfolding partition.simps haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp bulwahn@27656: from `l < r` have "l \ r - 1" by arith bulwahn@27656: from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma partition_partitions: haftmann@40671: assumes effect: "effect (partition a l r) h h' rs" bulwahn@27656: assumes "l < r" haftmann@37806: shows "(\i. l \ i \ i < rs \ Array.get h' (a::nat array) ! i \ Array.get h' a ! rs) \ haftmann@37806: (\i. rs < i \ i \ r \ Array.get h' a ! rs \ Array.get h' a ! i)" bulwahn@27656: proof - haftmann@37806: let ?pivot = "Array.get h a ! r" haftmann@40671: from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle" haftmann@40671: and swap: "effect (swap a rs r) h1 h' ()" haftmann@37806: and rs_equals: "rs = (if Array.get h1 a ! middle \ ?pivot then middle + 1 bulwahn@27656: else middle)" haftmann@28145: unfolding partition.simps haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp haftmann@37806: from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs) haftmann@37806: (Array.update a rs (Array.get h1 a ! r) h1)" haftmann@28145: unfolding swap_def haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp haftmann@37802: from swap have in_bounds: "r < Array.length h1 a \ rs < Array.length h1 a" haftmann@28145: unfolding swap_def haftmann@40671: by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp haftmann@37802: from swap have swap_length_remains: "Array.length h1 a = Array.length h' a" haftmann@40671: unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto haftmann@37771: from `l < r` have "l \ r - 1" by simp bulwahn@27656: note middle_in_bounds = part_returns_index_in_bounds[OF part this] bulwahn@27656: from part_outer_remains[OF part] `l < r` haftmann@37806: have "Array.get h a ! r = Array.get h1 a ! r" nipkow@44890: by fastforce bulwahn@27656: with swap haftmann@37806: have right_remains: "Array.get h a ! r = Array.get h' a ! rs" haftmann@28145: unfolding swap_def haftmann@40671: by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto) bulwahn@27656: from part_partitions [OF part] bulwahn@27656: show ?thesis haftmann@37806: proof (cases "Array.get h1 a ! middle \ ?pivot") bulwahn@27656: case True bulwahn@27656: with rs_equals have rs_equals: "rs = middle + 1" by simp bulwahn@27656: { bulwahn@27656: fix i bulwahn@27656: assume i_is_left: "l \ i \ i < rs" bulwahn@27656: with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r` haftmann@37802: have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto bulwahn@27656: from i_is_left rs_equals have "l \ i \ i < middle \ i = middle" by arith bulwahn@27656: with part_partitions[OF part] right_remains True nipkow@44890: have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastforce haftmann@37806: with i_props h'_def in_bounds have "Array.get h' a ! i \ Array.get h' a ! rs" haftmann@37798: unfolding Array.update_def Array.length_def by simp bulwahn@27656: } bulwahn@27656: moreover bulwahn@27656: { bulwahn@27656: fix i bulwahn@27656: assume "rs < i \ i \ r" bulwahn@27656: bulwahn@27656: hence "(rs < i \ i \ r - 1) \ (rs < i \ i = r)" by arith haftmann@37806: hence "Array.get h' a ! rs \ Array.get h' a ! i" bulwahn@27656: proof wenzelm@32960: assume i_is: "rs < i \ i \ r - 1" wenzelm@32960: with swap_length_remains in_bounds middle_in_bounds rs_equals haftmann@37802: have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto wenzelm@32960: from part_partitions[OF part] rs_equals right_remains i_is haftmann@37806: have "Array.get h' a ! rs \ Array.get h1 a ! i" nipkow@44890: by fastforce nipkow@44890: with i_props h'_def show ?thesis by fastforce bulwahn@27656: next wenzelm@32960: assume i_is: "rs < i \ i = r" wenzelm@32960: with rs_equals have "Suc middle \ r" by arith wenzelm@32960: with middle_in_bounds `l < r` have "Suc middle \ r - 1" by arith wenzelm@32960: with part_partitions[OF part] right_remains haftmann@37806: have "Array.get h' a ! rs \ Array.get h1 a ! (Suc middle)" nipkow@44890: by fastforce wenzelm@32960: with i_is True rs_equals right_remains h'_def wenzelm@32960: show ?thesis using in_bounds haftmann@37798: unfolding Array.update_def Array.length_def wenzelm@32960: by auto bulwahn@27656: qed bulwahn@27656: } bulwahn@27656: ultimately show ?thesis by auto bulwahn@27656: next bulwahn@27656: case False bulwahn@27656: with rs_equals have rs_equals: "middle = rs" by simp bulwahn@27656: { bulwahn@27656: fix i bulwahn@27656: assume i_is_left: "l \ i \ i < rs" bulwahn@27656: with swap_length_remains in_bounds middle_in_bounds rs_equals haftmann@37802: have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto bulwahn@27656: from part_partitions[OF part] rs_equals right_remains i_is_left nipkow@44890: have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastforce haftmann@37806: with i_props h'_def have "Array.get h' a ! i \ Array.get h' a ! rs" haftmann@37798: unfolding Array.update_def by simp bulwahn@27656: } bulwahn@27656: moreover bulwahn@27656: { bulwahn@27656: fix i bulwahn@27656: assume "rs < i \ i \ r" bulwahn@27656: hence "(rs < i \ i \ r - 1) \ i = r" by arith haftmann@37806: hence "Array.get h' a ! rs \ Array.get h' a ! i" bulwahn@27656: proof wenzelm@32960: assume i_is: "rs < i \ i \ r - 1" wenzelm@32960: with swap_length_remains in_bounds middle_in_bounds rs_equals haftmann@37802: have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto wenzelm@32960: from part_partitions[OF part] rs_equals right_remains i_is haftmann@37806: have "Array.get h' a ! rs \ Array.get h1 a ! i" nipkow@44890: by fastforce nipkow@44890: with i_props h'_def show ?thesis by fastforce bulwahn@27656: next wenzelm@32960: assume i_is: "i = r" wenzelm@32960: from i_is False rs_equals right_remains h'_def wenzelm@32960: show ?thesis using in_bounds haftmann@37798: unfolding Array.update_def Array.length_def wenzelm@32960: by auto bulwahn@27656: qed bulwahn@27656: } bulwahn@27656: ultimately bulwahn@27656: show ?thesis by auto bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: bulwahn@27656: function quicksort :: "nat array \ nat \ nat \ unit Heap" bulwahn@27656: where bulwahn@27656: "quicksort arr left right = bulwahn@27656: (if (right > left) then krauss@37792: do { bulwahn@27656: pivotNewIndex \ partition arr left right; bulwahn@27656: pivotNewIndex \ assert (\x. left \ x \ x \ right) pivotNewIndex; bulwahn@27656: quicksort arr left (pivotNewIndex - 1); bulwahn@27656: quicksort arr (pivotNewIndex + 1) right krauss@37792: } bulwahn@27656: else return ())" bulwahn@27656: by pat_completeness auto bulwahn@27656: bulwahn@27656: (* For termination, we must show that the pivotNewIndex is between left and right *) bulwahn@27656: termination bulwahn@27656: by (relation "measure (\(a, l, r). (r - l))") auto bulwahn@27656: bulwahn@27656: declare quicksort.simps[simp del] bulwahn@27656: bulwahn@27656: bulwahn@27656: lemma quicksort_permutes: haftmann@40671: assumes "effect (quicksort a l r) h h' rs" haftmann@37806: shows "multiset_of (Array.get h' a) haftmann@37806: = multiset_of (Array.get h a)" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) bulwahn@27656: case (1 a l r h h' rs) bulwahn@27656: with partition_permutes show ?case haftmann@28145: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma length_remains: haftmann@40671: assumes "effect (quicksort a l r) h h' rs" haftmann@37802: shows "Array.length h a = Array.length h' a" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) bulwahn@27656: case (1 a l r h h' rs) bulwahn@27656: with partition_length_remains show ?case haftmann@28145: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma quicksort_outer_remains: haftmann@40671: assumes "effect (quicksort a l r) h h' rs" haftmann@37806: shows "\i. i < l \ r < i \ Array.get h (a::nat array) ! i = Array.get h' a ! i" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) bulwahn@27656: case (1 a l r h h' rs) haftmann@40671: note cr = `effect (quicksort a l r) h h' rs` bulwahn@27656: thus ?case bulwahn@27656: proof (cases "r > l") bulwahn@27656: case False bulwahn@27656: with cr have "h' = h" bulwahn@27656: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_returnE) auto bulwahn@27656: thus ?thesis by simp bulwahn@27656: next bulwahn@27656: case True bulwahn@27656: { bulwahn@27656: fix h1 h2 p ret1 ret2 i haftmann@40671: assume part: "effect (partition a l r) h h1 p" haftmann@40671: assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1" haftmann@40671: assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2" bulwahn@27656: assume pivot: "l \ p \ p \ r" bulwahn@27656: assume i_outer: "i < l \ r < i" bulwahn@27656: from partition_outer_remains [OF part True] i_outer wenzelm@53374: have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce bulwahn@27656: moreover wenzelm@53374: from 1(1) [OF True pivot qs1] pivot i_outer 2 wenzelm@53374: have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto bulwahn@27656: moreover wenzelm@53374: from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3 haftmann@37806: have "Array.get h2 a ! i = Array.get h' a ! i" by auto haftmann@37806: ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp bulwahn@27656: } bulwahn@27656: with cr show ?thesis haftmann@28145: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: lemma quicksort_is_skip: haftmann@40671: assumes "effect (quicksort a l r) h h' rs" bulwahn@27656: shows "r \ l \ h = h'" bulwahn@27656: using assms haftmann@28145: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_returnE) auto bulwahn@27656: bulwahn@27656: lemma quicksort_sorts: haftmann@40671: assumes "effect (quicksort a l r) h h' rs" haftmann@37802: assumes l_r_length: "l < Array.length h a" "r < Array.length h a" bulwahn@27656: shows "sorted (subarray l (r + 1) a h')" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) bulwahn@27656: case (1 a l r h h' rs) haftmann@40671: note cr = `effect (quicksort a l r) h h' rs` bulwahn@27656: thus ?case bulwahn@27656: proof (cases "r > l") bulwahn@27656: case False bulwahn@27656: hence "l \ r + 1 \ l = r" by arith bulwahn@27656: with length_remains[OF cr] 1(5) show ?thesis bulwahn@27656: by (auto simp add: subarray_Nil subarray_single) bulwahn@27656: next bulwahn@27656: case True bulwahn@27656: { bulwahn@27656: fix h1 h2 p haftmann@40671: assume part: "effect (partition a l r) h h1 p" haftmann@40671: assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()" haftmann@40671: assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()" bulwahn@27656: from partition_returns_index_in_bounds [OF part True] bulwahn@27656: have pivot: "l\ p \ p \ r" . bulwahn@27656: note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part] bulwahn@27656: from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1] haftmann@37806: have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto) haftmann@28013: (*-- First of all, by induction hypothesis both sublists are sorted. *) bulwahn@27656: from 1(1)[OF True pivot qs1] length_remains pivot 1(5) bulwahn@27656: have IH1: "sorted (subarray l p a h2)" by (cases p, auto simp add: subarray_Nil) bulwahn@27656: from quicksort_outer_remains [OF qs2] length_remains bulwahn@27656: have left_subarray_remains: "subarray l p a h2 = subarray l p a h'" wenzelm@32960: by (simp add: subarray_eq_samelength_iff) bulwahn@27656: with IH1 have IH1': "sorted (subarray l p a h')" by simp bulwahn@27656: from 1(2)[OF True pivot qs2] pivot 1(5) length_remains bulwahn@27656: have IH2: "sorted (subarray (p + 1) (r + 1) a h')" haftmann@28013: by (cases "Suc p \ r", auto simp add: subarray_Nil) haftmann@28013: (* -- Secondly, both sublists remain partitioned. *) bulwahn@27656: from partition_partitions[OF part True] haftmann@37806: have part_conds1: "\j. j \ set (subarray l p a h1) \ j \ Array.get h1 a ! p " haftmann@37806: and part_conds2: "\j. j \ set (subarray (p + 1) (r + 1) a h1) \ Array.get h1 a ! p \ j" haftmann@28013: by (auto simp add: all_in_set_subarray_conv) bulwahn@27656: from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True haftmann@37806: length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"] bulwahn@27656: have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)" haftmann@37719: unfolding Array.length_def subarray_def by (cases p, auto) bulwahn@27656: with left_subarray_remains part_conds1 pivot_unchanged haftmann@37806: have part_conds2': "\j. j \ set (subarray l p a h') \ j \ Array.get h' a ! p" haftmann@28013: by (simp, subst set_of_multiset_of[symmetric], simp) haftmann@28013: (* -- These steps are the analogous for the right sublist \ *) bulwahn@27656: from quicksort_outer_remains [OF qs1] length_remains bulwahn@27656: have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2" wenzelm@32960: by (auto simp add: subarray_eq_samelength_iff) bulwahn@27656: from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True haftmann@37806: length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"] bulwahn@27656: have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)" haftmann@37719: unfolding Array.length_def subarray_def by auto bulwahn@27656: with right_subarray_remains part_conds2 pivot_unchanged haftmann@37806: have part_conds1': "\j. j \ set (subarray (p + 1) (r + 1) a h') \ Array.get h' a ! p \ j" haftmann@28013: by (simp, subst set_of_multiset_of[symmetric], simp) haftmann@28013: (* -- Thirdly and finally, we show that the array is sorted haftmann@28013: following from the facts above. *) haftmann@37806: 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'" wenzelm@32960: by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) bulwahn@27656: with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis wenzelm@32960: unfolding subarray_def wenzelm@32960: apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv) haftmann@37806: by (auto simp add: set_sublist' dest: le_trans [of _ "Array.get h' a ! p"]) bulwahn@27656: } bulwahn@27656: with True cr show ?thesis haftmann@28145: unfolding quicksort.simps [of a l r] haftmann@40671: by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto bulwahn@27656: qed bulwahn@27656: qed bulwahn@27656: bulwahn@27656: bulwahn@27656: lemma quicksort_is_sort: haftmann@40671: assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs" haftmann@37806: shows "Array.get h' a = sort (Array.get h a)" haftmann@37806: proof (cases "Array.get h a = []") bulwahn@27656: case True haftmann@40671: with quicksort_is_skip[OF effect] show ?thesis haftmann@37719: unfolding Array.length_def by simp bulwahn@27656: next bulwahn@27656: case False haftmann@40671: from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))" haftmann@37719: unfolding Array.length_def subarray_def by auto haftmann@40671: with length_remains[OF effect] have "sorted (Array.get h' a)" haftmann@37719: unfolding Array.length_def by simp nipkow@44890: with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce bulwahn@27656: qed bulwahn@27656: bulwahn@27656: subsection {* No Errors in quicksort *} bulwahn@27656: text {* We have proved that quicksort sorts (if no exceptions occur). bulwahn@27656: We will now show that exceptions do not occur. *} bulwahn@27656: haftmann@37758: lemma success_part1I: haftmann@37802: assumes "l < Array.length h a" "r < Array.length h a" haftmann@37758: shows "success (part1 a l r p) h" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r p arbitrary: h rule: part1.induct) bulwahn@27656: case (1 a l r p) haftmann@37771: thus ?case unfolding part1.simps [of a l r] huffman@47108: apply (auto intro!: success_intros simp add: not_le) huffman@47108: apply (auto intro!: effect_intros) haftmann@37771: done bulwahn@27656: qed bulwahn@27656: haftmann@37758: lemma success_bindI' [success_intros]: (*FIXME move*) haftmann@37758: assumes "success f h" haftmann@40671: assumes "\h' r. effect f h h' r \ success (g r) h'" haftmann@37758: shows "success (f \= g) h" haftmann@40671: using assms(1) proof (rule success_effectE) haftmann@37771: fix h' r wenzelm@53374: assume *: "effect f h h' r" wenzelm@53374: with assms(2) have "success (g r) h'" . wenzelm@53374: with * show "success (f \= g) h" by (rule success_bind_effectI) haftmann@37771: qed haftmann@37758: haftmann@37758: lemma success_partitionI: haftmann@37802: assumes "l < r" "l < Array.length h a" "r < Array.length h a" haftmann@37758: shows "success (partition a l r) h" haftmann@37758: using assms unfolding partition.simps swap_def haftmann@40671: 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:) bulwahn@27656: apply (frule part_length_remains) bulwahn@27656: apply (frule part_returns_index_in_bounds) bulwahn@27656: apply auto bulwahn@27656: apply (frule part_length_remains) bulwahn@27656: apply (frule part_returns_index_in_bounds) bulwahn@27656: apply auto bulwahn@27656: apply (frule part_length_remains) bulwahn@27656: apply auto bulwahn@27656: done bulwahn@27656: haftmann@37758: lemma success_quicksortI: haftmann@37802: assumes "l < Array.length h a" "r < Array.length h a" haftmann@37758: shows "success (quicksort a l r) h" bulwahn@27656: using assms bulwahn@27656: proof (induct a l r arbitrary: h rule: quicksort.induct) bulwahn@27656: case (1 a l ri h) bulwahn@27656: thus ?case haftmann@28145: unfolding quicksort.simps [of a l ri] haftmann@37758: apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI) bulwahn@27656: apply (frule partition_returns_index_in_bounds) bulwahn@27656: apply auto bulwahn@27656: apply (frule partition_returns_index_in_bounds) bulwahn@27656: apply auto haftmann@40671: apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains) bulwahn@27656: apply (subgoal_tac "Suc r \ ri \ r = ri") bulwahn@27656: apply (erule disjE) bulwahn@27656: apply auto haftmann@28145: unfolding quicksort.simps [of a "Suc ri" ri] haftmann@37758: apply (auto intro!: success_ifI success_returnI) bulwahn@27656: done bulwahn@27656: qed bulwahn@27656: haftmann@27674: haftmann@27674: subsection {* Example *} haftmann@27674: krauss@37792: definition "qsort a = do { haftmann@37798: k \ Array.len a; haftmann@27674: quicksort a 0 (k - 1); haftmann@27674: return a krauss@37792: }" haftmann@27674: haftmann@35041: code_reserved SML upto haftmann@35041: haftmann@51143: definition "example = do { haftmann@51143: a \ Array.of_list [42, 2, 3, 5, 0, 1705, 8, 3, 15]; haftmann@51143: qsort a haftmann@51143: }" haftmann@51143: wenzelm@51272: ML_val {* @{code example} () *} haftmann@27674: haftmann@50630: export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp haftmann@27674: haftmann@37845: end