author | haftmann |
Sun, 04 Nov 2018 15:00:30 +0000 | |
changeset 69246 | c1fe9dcc274a |
parent 69194 | 6d514e128a85 |
child 69250 | 1011f0b46af7 |
permissions | -rw-r--r-- |
69194 | 1 |
(* Title: HOL/Library/Sorting_Algorithms.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
theory Sorting_Algorithms |
|
6 |
imports Main Multiset Comparator |
|
7 |
begin |
|
8 |
||
9 |
section \<open>Stably sorted lists\<close> |
|
10 |
||
11 |
abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
12 |
where "stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)" |
|
13 |
||
14 |
fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool" |
|
15 |
where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True" |
|
16 |
| sorted_single: "sorted cmp [x] \<longleftrightarrow> True" |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
17 |
| sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)" |
69194 | 18 |
|
19 |
lemma sorted_ConsI: |
|
20 |
"sorted cmp (x # xs)" if "sorted cmp xs" |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
21 |
and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
22 |
using that by (cases xs) simp_all |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
23 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
24 |
lemma sorted_Cons_imp_sorted: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
25 |
"sorted cmp xs" if "sorted cmp (x # xs)" |
69194 | 26 |
using that by (cases xs) simp_all |
27 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
28 |
lemma sorted_Cons_imp_not_less: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
29 |
"compare cmp y x \<noteq> Greater" if "sorted cmp (y # xs)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
30 |
and "x \<in> set xs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
31 |
using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
32 |
|
69194 | 33 |
lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]: |
34 |
"P xs" if "sorted cmp xs" and "P []" |
|
35 |
and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
36 |
\<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)" |
69194 | 37 |
using \<open>sorted cmp xs\<close> proof (induction xs) |
38 |
case Nil |
|
39 |
show ?case |
|
40 |
by (rule \<open>P []\<close>) |
|
41 |
next |
|
42 |
case (Cons x xs) |
|
43 |
from \<open>sorted cmp (x # xs)\<close> have "sorted cmp xs" |
|
44 |
by (cases xs) simp_all |
|
45 |
moreover have "P xs" using \<open>sorted cmp xs\<close> |
|
46 |
by (rule Cons.IH) |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
47 |
moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y |
69194 | 48 |
using that \<open>sorted cmp (x # xs)\<close> proof (induction xs) |
49 |
case Nil |
|
50 |
then show ?case |
|
51 |
by simp |
|
52 |
next |
|
53 |
case (Cons z zs) |
|
54 |
then show ?case |
|
55 |
proof (cases zs) |
|
56 |
case Nil |
|
57 |
with Cons.prems show ?thesis |
|
58 |
by simp |
|
59 |
next |
|
60 |
case (Cons w ws) |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
61 |
with Cons.prems have "compare cmp z w \<noteq> Greater" "compare cmp x z \<noteq> Greater" |
69194 | 62 |
by auto |
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
63 |
then have "compare cmp x w \<noteq> Greater" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
64 |
by (auto dest: compare.trans_not_greater) |
69194 | 65 |
with Cons show ?thesis |
66 |
using Cons.prems Cons.IH by auto |
|
67 |
qed |
|
68 |
qed |
|
69 |
ultimately show ?case |
|
70 |
by (rule *) |
|
71 |
qed |
|
72 |
||
73 |
lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]: |
|
74 |
"P xs" if "sorted cmp xs" and "P []" |
|
75 |
and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs) |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
76 |
\<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) |
69194 | 77 |
\<Longrightarrow> P xs" |
78 |
using \<open>sorted cmp xs\<close> proof (induction xs) |
|
79 |
case Nil |
|
80 |
show ?case |
|
81 |
by (rule \<open>P []\<close>) |
|
82 |
next |
|
83 |
case (Cons x xs) |
|
84 |
then have "sorted cmp (x # xs)" |
|
85 |
by (simp add: sorted_ConsI) |
|
86 |
moreover note Cons.IH |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
87 |
moreover have "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False" |
69194 | 88 |
using Cons.hyps by simp |
89 |
ultimately show ?case |
|
90 |
by (auto intro!: * [of "x # xs" x]) blast |
|
91 |
qed |
|
92 |
||
93 |
lemma sorted_remove1: |
|
94 |
"sorted cmp (remove1 x xs)" if "sorted cmp xs" |
|
95 |
proof (cases "x \<in> set xs") |
|
96 |
case False |
|
97 |
with that show ?thesis |
|
98 |
by (simp add: remove1_idem) |
|
99 |
next |
|
100 |
case True |
|
101 |
with that show ?thesis proof (induction xs) |
|
102 |
case Nil |
|
103 |
then show ?case |
|
104 |
by simp |
|
105 |
next |
|
106 |
case (Cons y ys) |
|
107 |
show ?case proof (cases "x = y") |
|
108 |
case True |
|
109 |
with Cons.hyps show ?thesis |
|
110 |
by simp |
|
111 |
next |
|
112 |
case False |
|
113 |
then have "sorted cmp (remove1 x ys)" |
|
114 |
using Cons.IH Cons.prems by auto |
|
115 |
then have "sorted cmp (y # remove1 x ys)" |
|
116 |
proof (rule sorted_ConsI) |
|
117 |
fix z zs |
|
118 |
assume "remove1 x ys = z # zs" |
|
119 |
with \<open>x \<noteq> y\<close> have "z \<in> set ys" |
|
120 |
using notin_set_remove1 [of z ys x] by auto |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
121 |
then show "compare cmp y z \<noteq> Greater" |
69194 | 122 |
by (rule Cons.hyps(2)) |
123 |
qed |
|
124 |
with False show ?thesis |
|
125 |
by simp |
|
126 |
qed |
|
127 |
qed |
|
128 |
qed |
|
129 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
130 |
lemma sorted_stable_segment: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
131 |
"sorted cmp (stable_segment cmp x xs)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
132 |
proof (induction xs) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
133 |
case Nil |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
134 |
show ?case |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
135 |
by simp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
136 |
next |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
137 |
case (Cons y ys) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
138 |
then show ?case |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
139 |
by (auto intro!: sorted_ConsI simp add: filter_eq_Cons_iff compare.sym) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
140 |
(auto dest: compare.trans_equiv simp add: compare.sym compare.greater_iff_sym_less) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
141 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
142 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
143 |
|
69194 | 144 |
primrec insort :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
145 |
where "insort cmp y [] = [y]" |
|
146 |
| "insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater |
|
147 |
then y # x # xs |
|
148 |
else x # insort cmp y xs)" |
|
149 |
||
150 |
lemma mset_insort [simp]: |
|
151 |
"mset (insort cmp x xs) = add_mset x (mset xs)" |
|
152 |
by (induction xs) simp_all |
|
153 |
||
154 |
lemma length_insort [simp]: |
|
155 |
"length (insort cmp x xs) = Suc (length xs)" |
|
156 |
by (induction xs) simp_all |
|
157 |
||
158 |
lemma sorted_insort: |
|
159 |
"sorted cmp (insort cmp x xs)" if "sorted cmp xs" |
|
160 |
using that proof (induction xs) |
|
161 |
case Nil |
|
162 |
then show ?case |
|
163 |
by simp |
|
164 |
next |
|
165 |
case (Cons y ys) |
|
166 |
then show ?case by (cases ys) |
|
167 |
(auto, simp_all add: compare.greater_iff_sym_less) |
|
168 |
qed |
|
169 |
||
170 |
lemma stable_insort_equiv: |
|
171 |
"stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs" |
|
172 |
if "compare cmp y x = Equiv" |
|
173 |
proof (induction xs) |
|
174 |
case Nil |
|
175 |
from that show ?case |
|
176 |
by simp |
|
177 |
next |
|
178 |
case (Cons z xs) |
|
179 |
moreover from that have "compare cmp y z = Equiv \<Longrightarrow> compare cmp z x = Equiv" |
|
180 |
by (auto intro: compare.trans_equiv simp add: compare.sym) |
|
181 |
ultimately show ?case |
|
182 |
using that by (auto simp add: compare.greater_iff_sym_less) |
|
183 |
qed |
|
184 |
||
185 |
lemma stable_insort_not_equiv: |
|
186 |
"stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs" |
|
187 |
if "compare cmp y x \<noteq> Equiv" |
|
188 |
using that by (induction xs) simp_all |
|
189 |
||
190 |
lemma remove1_insort_same_eq [simp]: |
|
191 |
"remove1 x (insort cmp x xs) = xs" |
|
192 |
by (induction xs) simp_all |
|
193 |
||
194 |
lemma insort_eq_ConsI: |
|
195 |
"insort cmp x xs = x # xs" |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
196 |
if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater" |
69194 | 197 |
using that by (induction xs) (simp_all add: compare.greater_iff_sym_less) |
198 |
||
199 |
lemma remove1_insort_not_same_eq [simp]: |
|
200 |
"remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)" |
|
201 |
if "sorted cmp xs" "x \<noteq> y" |
|
202 |
using that proof (induction xs) |
|
203 |
case Nil |
|
204 |
then show ?case |
|
205 |
by simp |
|
206 |
next |
|
207 |
case (Cons z zs) |
|
208 |
show ?case |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
209 |
proof (cases "compare cmp x z = Greater") |
69194 | 210 |
case True |
211 |
with Cons show ?thesis |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
212 |
by simp |
69194 | 213 |
next |
214 |
case False |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
215 |
then have "compare cmp x y \<noteq> Greater" if "y \<in> set zs" for y |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
216 |
using that Cons.hyps |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
217 |
by (auto dest: compare.trans_not_greater) |
69194 | 218 |
with Cons show ?thesis |
219 |
by (simp add: insort_eq_ConsI) |
|
220 |
qed |
|
221 |
qed |
|
222 |
||
223 |
lemma insort_remove1_same_eq: |
|
224 |
"insort cmp x (remove1 x xs) = xs" |
|
225 |
if "sorted cmp xs" and "x \<in> set xs" and "hd (stable_segment cmp x xs) = x" |
|
226 |
using that proof (induction xs) |
|
227 |
case Nil |
|
228 |
then show ?case |
|
229 |
by simp |
|
230 |
next |
|
231 |
case (Cons y ys) |
|
232 |
then have "compare cmp x y \<noteq> Less" |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
233 |
by (auto simp add: compare.greater_iff_sym_less) |
69194 | 234 |
then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv" |
235 |
by (cases "compare cmp x y") auto |
|
236 |
then show ?case proof cases |
|
237 |
case 1 |
|
238 |
with Cons.prems Cons.IH show ?thesis |
|
239 |
by auto |
|
240 |
next |
|
241 |
case 2 |
|
242 |
with Cons.prems have "x = y" |
|
243 |
by simp |
|
244 |
with Cons.hyps show ?thesis |
|
245 |
by (simp add: insort_eq_ConsI) |
|
246 |
qed |
|
247 |
qed |
|
248 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
249 |
lemma sorted_append_iff: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
250 |
"sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
251 |
\<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q") |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
252 |
proof |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
253 |
assume ?P |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
254 |
have ?R |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
255 |
using \<open>?P\<close> by (induction xs) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
256 |
(auto simp add: sorted_Cons_imp_not_less, |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
257 |
auto simp add: sorted_Cons_imp_sorted intro: sorted_ConsI) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
258 |
moreover have ?S |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
259 |
using \<open>?P\<close> by (induction xs) (auto dest: sorted_Cons_imp_sorted) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
260 |
moreover have ?Q |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
261 |
using \<open>?P\<close> by (induction xs) (auto simp add: sorted_Cons_imp_not_less, |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
262 |
simp add: sorted_Cons_imp_sorted) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
263 |
ultimately show "?R \<and> ?S \<and> ?Q" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
264 |
by simp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
265 |
next |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
266 |
assume "?R \<and> ?S \<and> ?Q" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
267 |
then have ?R ?S ?Q |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
268 |
by simp_all |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
269 |
then show ?P |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
270 |
by (induction xs) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
271 |
(auto simp add: append_eq_Cons_conv intro!: sorted_ConsI) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
272 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
273 |
|
69194 | 274 |
definition sort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list" |
275 |
where "sort cmp xs = foldr (insort cmp) xs []" |
|
276 |
||
277 |
lemma sort_simps [simp]: |
|
278 |
"sort cmp [] = []" |
|
279 |
"sort cmp (x # xs) = insort cmp x (sort cmp xs)" |
|
280 |
by (simp_all add: sort_def) |
|
281 |
||
282 |
lemma mset_sort [simp]: |
|
283 |
"mset (sort cmp xs) = mset xs" |
|
284 |
by (induction xs) simp_all |
|
285 |
||
286 |
lemma length_sort [simp]: |
|
287 |
"length (sort cmp xs) = length xs" |
|
288 |
by (induction xs) simp_all |
|
289 |
||
290 |
lemma sorted_sort [simp]: |
|
291 |
"sorted cmp (sort cmp xs)" |
|
292 |
by (induction xs) (simp_all add: sorted_insort) |
|
293 |
||
294 |
lemma stable_sort: |
|
295 |
"stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs" |
|
296 |
by (induction xs) (simp_all add: stable_insort_equiv stable_insort_not_equiv) |
|
297 |
||
298 |
lemma sort_remove1_eq [simp]: |
|
299 |
"sort cmp (remove1 x xs) = remove1 x (sort cmp xs)" |
|
300 |
by (induction xs) simp_all |
|
301 |
||
302 |
lemma set_insort [simp]: |
|
303 |
"set (insort cmp x xs) = insert x (set xs)" |
|
304 |
by (induction xs) auto |
|
305 |
||
306 |
lemma set_sort [simp]: |
|
307 |
"set (sort cmp xs) = set xs" |
|
308 |
by (induction xs) auto |
|
309 |
||
310 |
lemma sort_eqI: |
|
311 |
"sort cmp ys = xs" |
|
312 |
if permutation: "mset ys = mset xs" |
|
313 |
and sorted: "sorted cmp xs" |
|
314 |
and stable: "\<And>y. y \<in> set ys \<Longrightarrow> |
|
315 |
stable_segment cmp y ys = stable_segment cmp y xs" |
|
316 |
proof - |
|
317 |
have stable': "stable_segment cmp y ys = |
|
318 |
stable_segment cmp y xs" for y |
|
319 |
proof (cases "\<exists>x\<in>set ys. compare cmp y x = Equiv") |
|
320 |
case True |
|
321 |
then obtain z where "z \<in> set ys" and "compare cmp y z = Equiv" |
|
322 |
by auto |
|
323 |
then have "compare cmp y x = Equiv \<longleftrightarrow> compare cmp z x = Equiv" for x |
|
324 |
by (meson compare.sym compare.trans_equiv) |
|
325 |
moreover have "stable_segment cmp z ys = |
|
326 |
stable_segment cmp z xs" |
|
327 |
using \<open>z \<in> set ys\<close> by (rule stable) |
|
328 |
ultimately show ?thesis |
|
329 |
by simp |
|
330 |
next |
|
331 |
case False |
|
332 |
moreover from permutation have "set ys = set xs" |
|
333 |
by (rule mset_eq_setD) |
|
334 |
ultimately show ?thesis |
|
335 |
by simp |
|
336 |
qed |
|
337 |
show ?thesis |
|
338 |
using sorted permutation stable' proof (induction xs arbitrary: ys rule: sorted_induct_remove1) |
|
339 |
case Nil |
|
340 |
then show ?case |
|
341 |
by simp |
|
342 |
next |
|
343 |
case (minimum x xs) |
|
344 |
from \<open>mset ys = mset xs\<close> have ys: "set ys = set xs" |
|
345 |
by (rule mset_eq_setD) |
|
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
346 |
then have "compare cmp x y \<noteq> Greater" if "y \<in> set ys" for y |
69194 | 347 |
using that minimum.hyps by simp |
348 |
from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs" |
|
349 |
by simp |
|
350 |
have "sort cmp (remove1 x ys) = remove1 x xs" |
|
351 |
by (rule minimum.IH) (simp_all add: minimum.prems filter_remove1) |
|
352 |
then have "remove1 x (sort cmp ys) = remove1 x xs" |
|
353 |
by simp |
|
354 |
then have "insort cmp x (remove1 x (sort cmp ys)) = |
|
355 |
insort cmp x (remove1 x xs)" |
|
356 |
by simp |
|
357 |
also from minimum.hyps ys stable have "insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys" |
|
358 |
by (simp add: stable_sort insort_remove1_same_eq) |
|
359 |
also from minimum.hyps have "insort cmp x (remove1 x xs) = xs" |
|
360 |
by (simp add: insort_remove1_same_eq) |
|
361 |
finally show ?case . |
|
362 |
qed |
|
363 |
qed |
|
364 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
365 |
lemma filter_insort: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
366 |
"filter P (insort cmp x xs) = insort cmp x (filter P xs)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
367 |
if "sorted cmp xs" and "P x" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
368 |
using that by (induction xs) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
369 |
(auto simp add: compare.trans_not_greater insort_eq_ConsI) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
370 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
371 |
lemma filter_insort_triv: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
372 |
"filter P (insort cmp x xs) = filter P xs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
373 |
if "\<not> P x" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
374 |
using that by (induction xs) simp_all |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
375 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
376 |
lemma filter_sort: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
377 |
"filter P (sort cmp xs) = sort cmp (filter P xs)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
378 |
by (induction xs) (auto simp add: filter_insort filter_insort_triv) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
379 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
380 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
381 |
section \<open>Alternative sorting algorithms\<close> |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
382 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
383 |
subsection \<open>Quicksort\<close> |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
384 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
385 |
definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
386 |
where quicksort_is_sort [simp]: "quicksort = sort" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
387 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
388 |
lemma sort_by_quicksort: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
389 |
"sort = quicksort" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
390 |
by simp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
391 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
392 |
lemma sort_by_quicksort_rec: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
393 |
"sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less] |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
394 |
@ stable_segment cmp (xs ! (length xs div 2)) xs |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
395 |
@ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "sort cmp ?lhs = ?rhs") |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
396 |
proof (rule sort_eqI) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
397 |
show "mset ?lhs = mset ?rhs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
398 |
by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
399 |
next |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
400 |
show "sorted cmp ?rhs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
401 |
by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
402 |
next |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
403 |
let ?pivot = "xs ! (length xs div 2)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
404 |
fix l |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
405 |
assume "l \<in> set xs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
406 |
have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
407 |
\<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
408 |
proof - |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
409 |
have "compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
410 |
if "compare cmp l x = Equiv" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
411 |
using that by (simp add: compare.equiv_subst_left compare.sym) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
412 |
then show ?thesis by blast |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
413 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
414 |
then show "stable_segment cmp l ?lhs = stable_segment cmp l ?rhs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
415 |
by (simp add: stable_sort compare.sym [of _ ?pivot]) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
416 |
(cases "compare cmp l ?pivot", simp_all) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
417 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
418 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
419 |
context |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
420 |
begin |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
421 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
422 |
qualified definition partition :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
423 |
where "partition cmp pivot xs = |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
424 |
([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
425 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
426 |
qualified lemma partition_code [code]: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
427 |
"partition cmp pivot [] = ([], [], [])" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
428 |
"partition cmp pivot (x # xs) = |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
429 |
(let (lts, eqs, gts) = partition cmp pivot xs |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
430 |
in case compare cmp x pivot of |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
431 |
Less \<Rightarrow> (x # lts, eqs, gts) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
432 |
| Equiv \<Rightarrow> (lts, x # eqs, gts) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
433 |
| Greater \<Rightarrow> (lts, eqs, x # gts))" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
434 |
using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot]) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
435 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
436 |
lemma quicksort_code [code]: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
437 |
"quicksort cmp xs = |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
438 |
(case xs of |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
439 |
[] \<Rightarrow> [] |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
440 |
| [x] \<Rightarrow> xs |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
441 |
| [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x]) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
442 |
| _ \<Rightarrow> |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
443 |
let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
444 |
in quicksort cmp lts @ eqs @ quicksort cmp gts)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
445 |
proof (cases "length xs \<ge> 3") |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
446 |
case False |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
447 |
then have "length xs \<le> 2" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
448 |
by simp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
449 |
then have "length xs = 0 \<or> length xs = 1 \<or> length xs = 2" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
450 |
using le_neq_trans less_2_cases by auto |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
451 |
then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
452 |
by (auto simp add: length_Suc_conv numeral_2_eq_2) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
453 |
then show ?thesis |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
454 |
by cases simp_all |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
455 |
next |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
456 |
case True |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
457 |
then obtain x y z zs where "xs = x # y # z # zs" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
458 |
by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
459 |
moreover have "quicksort cmp xs = |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
460 |
(let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
461 |
in quicksort cmp lts @ eqs @ quicksort cmp gts)" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
462 |
using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
463 |
ultimately show ?thesis |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
464 |
by simp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
465 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
466 |
|
69194 | 467 |
end |
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
468 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
469 |
text \<open>Evaluation example\<close> |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
470 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
471 |
value "let cmp = key abs (reversed default) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
472 |
in quicksort cmp [65, 1705, -2322, 734, 4, (-17::int)]" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
473 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
474 |
end |