changeset 61702 | 2e89bc578935 |
parent 60515 | 484559628038 |
child 62026 | ea3b1b0413b4 |
61701:e89cfc004f18 | 61702:2e89bc578935 |
---|---|
12 "~~/src/HOL/Library/Code_Target_Numeral" |
12 "~~/src/HOL/Library/Code_Target_Numeral" |
13 begin |
13 begin |
14 |
14 |
15 text {* We prove QuickSort correct in the Relational Calculus. *} |
15 text {* We prove QuickSort correct in the Relational Calculus. *} |
16 |
16 |
17 definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |
17 definition swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |
18 where |
18 where |
19 "swap arr i j = |
19 "swap arr i j = |
20 do { |
20 do { |
21 x \<leftarrow> Array.nth arr i; |
21 x \<leftarrow> Array.nth arr i; |
22 y \<leftarrow> Array.nth arr j; |
22 y \<leftarrow> Array.nth arr j; |
38 = mset (Array.get h a)" |
38 = mset (Array.get h a)" |
39 using assms |
39 using assms |
40 unfolding swap_def |
40 unfolding swap_def |
41 by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE) |
41 by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE) |
42 |
42 |
43 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap" |
43 function part1 :: "'a::{heap,ord} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat Heap" |
44 where |
44 where |
45 "part1 a left right p = ( |
45 "part1 a left right p = ( |
46 if (right \<le> left) then return right |
46 if (right \<le> left) then return right |
47 else do { |
47 else do { |
48 v \<leftarrow> Array.nth a left; |
48 v \<leftarrow> Array.nth a left; |
132 qed |
132 qed |
133 qed |
133 qed |
134 |
134 |
135 lemma part_outer_remains: |
135 lemma part_outer_remains: |
136 assumes "effect (part1 a l r p) h h' rs" |
136 assumes "effect (part1 a l r p) h h' rs" |
137 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" |
137 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i" |
138 using assms |
138 using assms |
139 proof (induct a l r p arbitrary: h h' rs rule:part1.induct) |
139 proof (induct a l r p arbitrary: h h' rs rule:part1.induct) |
140 case (1 a l r p h h' rs) |
140 case (1 a l r p h h' rs) |
141 note cr = `effect (part1 a l r p) h h' rs` |
141 note cr = `effect (part1 a l r p) h h' rs` |
142 |
142 |
176 qed |
176 qed |
177 |
177 |
178 |
178 |
179 lemma part_partitions: |
179 lemma part_partitions: |
180 assumes "effect (part1 a l r p) h h' rs" |
180 assumes "effect (part1 a l r p) h h' rs" |
181 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p) |
181 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::'a::{heap,linorder} array) ! i \<le> p) |
182 \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)" |
182 \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)" |
183 using assms |
183 using assms |
184 proof (induct a l r p arbitrary: h h' rs rule:part1.induct) |
184 proof (induct a l r p arbitrary: h h' rs rule:part1.induct) |
185 case (1 a l r p h h' rs) |
185 case (1 a l r p h h' rs) |
186 note cr = `effect (part1 a l r p) h h' rs` |
186 note cr = `effect (part1 a l r p) h h' rs` |
227 qed |
227 qed |
228 qed |
228 qed |
229 qed |
229 qed |
230 |
230 |
231 |
231 |
232 fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap" |
232 fun partition :: "'a::{heap,linorder} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap" |
233 where |
233 where |
234 "partition a left right = do { |
234 "partition a left right = do { |
235 pivot \<leftarrow> Array.nth a right; |
235 pivot \<leftarrow> Array.nth a right; |
236 middle \<leftarrow> part1 a left (right - 1) pivot; |
236 middle \<leftarrow> part1 a left (right - 1) pivot; |
237 v \<leftarrow> Array.nth a middle; |
237 v \<leftarrow> Array.nth a middle; |
247 shows "mset (Array.get h' a) |
247 shows "mset (Array.get h' a) |
248 = mset (Array.get h a)" |
248 = mset (Array.get h a)" |
249 proof - |
249 proof - |
250 from assms part_permutes swap_permutes show ?thesis |
250 from assms part_permutes swap_permutes show ?thesis |
251 unfolding partition.simps |
251 unfolding partition.simps |
252 by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto |
252 by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce |
253 qed |
253 qed |
254 |
254 |
255 lemma partition_length_remains: |
255 lemma partition_length_remains: |
256 assumes "effect (partition a l r) h h' rs" |
256 assumes "effect (partition a l r) h h' rs" |
257 shows "Array.length h a = Array.length h' a" |
257 shows "Array.length h a = Array.length h' a" |
262 qed |
262 qed |
263 |
263 |
264 lemma partition_outer_remains: |
264 lemma partition_outer_remains: |
265 assumes "effect (partition a l r) h h' rs" |
265 assumes "effect (partition a l r) h h' rs" |
266 assumes "l < r" |
266 assumes "l < r" |
267 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" |
267 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i" |
268 proof - |
268 proof - |
269 from assms part_outer_remains part_returns_index_in_bounds show ?thesis |
269 from assms part_outer_remains part_returns_index_in_bounds show ?thesis |
270 unfolding partition.simps swap_def |
270 unfolding partition.simps swap_def |
271 by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce |
271 by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce |
272 qed |
272 qed |
286 qed |
286 qed |
287 |
287 |
288 lemma partition_partitions: |
288 lemma partition_partitions: |
289 assumes effect: "effect (partition a l r) h h' rs" |
289 assumes effect: "effect (partition a l r) h h' rs" |
290 assumes "l < r" |
290 assumes "l < r" |
291 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and> |
291 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::'a::{heap,linorder} array) ! i \<le> Array.get h' a ! rs) \<and> |
292 (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)" |
292 (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)" |
293 proof - |
293 proof - |
294 let ?pivot = "Array.get h a ! r" |
294 let ?pivot = "Array.get h a ! r" |
295 from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle" |
295 from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle" |
296 and swap: "effect (swap a rs r) h1 h' ()" |
296 and swap: "effect (swap a rs r) h1 h' ()" |
400 show ?thesis by auto |
400 show ?thesis by auto |
401 qed |
401 qed |
402 qed |
402 qed |
403 |
403 |
404 |
404 |
405 function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |
405 function quicksort :: "'a::{heap,linorder} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |
406 where |
406 where |
407 "quicksort arr left right = |
407 "quicksort arr left right = |
408 (if (right > left) then |
408 (if (right > left) then |
409 do { |
409 do { |
410 pivotNewIndex \<leftarrow> partition arr left right; |
410 pivotNewIndex \<leftarrow> partition arr left right; |
440 using assms |
440 using assms |
441 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) |
441 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) |
442 case (1 a l r h h' rs) |
442 case (1 a l r h h' rs) |
443 with partition_length_remains show ?case |
443 with partition_length_remains show ?case |
444 unfolding quicksort.simps [of a l r] |
444 unfolding quicksort.simps [of a l r] |
445 by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto |
445 by (elim effect_ifE effect_bindE effect_assertE effect_returnE) fastforce+ |
446 qed |
446 qed |
447 |
447 |
448 lemma quicksort_outer_remains: |
448 lemma quicksort_outer_remains: |
449 assumes "effect (quicksort a l r) h h' rs" |
449 assumes "effect (quicksort a l r) h h' rs" |
450 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" |
450 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i" |
451 using assms |
451 using assms |
452 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) |
452 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) |
453 case (1 a l r h h' rs) |
453 case (1 a l r h h' rs) |
454 note cr = `effect (quicksort a l r) h h' rs` |
454 note cr = `effect (quicksort a l r) h h' rs` |
455 thus ?case |
455 thus ?case |
555 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'" |
555 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'" |
556 by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) |
556 by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) |
557 with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis |
557 with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis |
558 unfolding subarray_def |
558 unfolding subarray_def |
559 apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv) |
559 apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv) |
560 by (auto simp add: set_sublist' dest: le_trans [of _ "Array.get h' a ! p"]) |
560 by (auto simp add: set_sublist' dest: order.trans [of _ "Array.get h' a ! p"]) |
561 } |
561 } |
562 with True cr show ?thesis |
562 with True cr show ?thesis |
563 unfolding quicksort.simps [of a l r] |
563 unfolding quicksort.simps [of a l r] |
564 by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto |
564 by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto |
565 qed |
565 qed |
656 }" |
656 }" |
657 |
657 |
658 code_reserved SML upto |
658 code_reserved SML upto |
659 |
659 |
660 definition "example = do { |
660 definition "example = do { |
661 a \<leftarrow> Array.of_list [42, 2, 3, 5, 0, 1705, 8, 3, 15]; |
661 a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list); |
662 qsort a |
662 qsort a |
663 }" |
663 }" |
664 |
664 |
665 ML_val {* @{code example} () *} |
665 ML_val {* @{code example} () *} |
666 |
666 |