author | nipkow |
Sun, 13 May 2018 14:40:40 +0200 | |
changeset 68162 | 61878d2aa6c7 |
parent 68161 | 2053ff42214b |
child 68934 | b825fa94fe56 |
permissions | -rw-r--r-- |
66543 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Sorting |
|
4 |
imports |
|
5 |
Complex_Main |
|
6 |
"HOL-Library.Multiset" |
|
7 |
begin |
|
8 |
||
68160 | 9 |
hide_const List.insort |
66543 | 10 |
|
11 |
declare Let_def [simp] |
|
12 |
||
13 |
||
14 |
subsection "Insertion Sort" |
|
15 |
||
16 |
fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
17 |
"insort x [] = [x]" | |
|
18 |
"insort x (y#ys) = |
|
19 |
(if x \<le> y then x#y#ys else y#(insort x ys))" |
|
20 |
||
21 |
fun isort :: "'a::linorder list \<Rightarrow> 'a list" where |
|
22 |
"isort [] = []" | |
|
23 |
"isort (x#xs) = insort x (isort xs)" |
|
24 |
||
68078 | 25 |
|
66543 | 26 |
subsubsection "Functional Correctness" |
27 |
||
28 |
lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)" |
|
29 |
apply(induction xs) |
|
30 |
apply auto |
|
31 |
done |
|
32 |
||
33 |
lemma mset_isort: "mset (isort xs) = mset xs" |
|
34 |
apply(induction xs) |
|
35 |
apply simp |
|
36 |
apply (simp add: mset_insort) |
|
37 |
done |
|
38 |
||
39 |
lemma set_insort: "set (insort x xs) = insert x (set xs)" |
|
40 |
by (metis mset_insort set_mset_add_mset_insert set_mset_mset) |
|
41 |
||
42 |
lemma sorted_insort: "sorted (insort a xs) = sorted xs" |
|
43 |
apply(induction xs) |
|
44 |
apply(auto simp add: set_insort) |
|
45 |
done |
|
46 |
||
47 |
lemma "sorted (isort xs)" |
|
48 |
apply(induction xs) |
|
49 |
apply(auto simp: sorted_insort) |
|
50 |
done |
|
51 |
||
68078 | 52 |
|
53 |
subsubsection "Time Complexity" |
|
66543 | 54 |
|
55 |
text \<open>We count the number of function calls.\<close> |
|
56 |
||
57 |
text\<open> |
|
58 |
\<open>insort x [] = [x]\<close> |
|
59 |
\<open>insort x (y#ys) = |
|
60 |
(if x \<le> y then x#y#ys else y#(insort x ys))\<close> |
|
61 |
\<close> |
|
62 |
fun t_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
63 |
"t_insort x [] = 1" | |
|
64 |
"t_insort x (y#ys) = |
|
65 |
(if x \<le> y then 0 else t_insort x ys) + 1" |
|
66 |
||
67 |
text\<open> |
|
68 |
\<open>isort [] = []\<close> |
|
69 |
\<open>isort (x#xs) = insort x (isort xs)\<close> |
|
70 |
\<close> |
|
71 |
fun t_isort :: "'a::linorder list \<Rightarrow> nat" where |
|
72 |
"t_isort [] = 1" | |
|
73 |
"t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" |
|
74 |
||
75 |
||
76 |
lemma t_insort_length: "t_insort x xs \<le> length xs + 1" |
|
77 |
apply(induction xs) |
|
78 |
apply auto |
|
79 |
done |
|
80 |
||
81 |
lemma length_insort: "length (insort x xs) = length xs + 1" |
|
82 |
apply(induction xs) |
|
83 |
apply auto |
|
84 |
done |
|
85 |
||
86 |
lemma length_isort: "length (isort xs) = length xs" |
|
87 |
apply(induction xs) |
|
88 |
apply (auto simp: length_insort) |
|
89 |
done |
|
90 |
||
91 |
lemma t_isort_length: "t_isort xs \<le> (length xs + 1) ^ 2" |
|
92 |
proof(induction xs) |
|
93 |
case Nil show ?case by simp |
|
94 |
next |
|
95 |
case (Cons x xs) |
|
96 |
have "t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" by simp |
|
97 |
also have "\<dots> \<le> (length xs + 1) ^ 2 + t_insort x (isort xs) + 1" |
|
98 |
using Cons.IH by simp |
|
99 |
also have "\<dots> \<le> (length xs + 1) ^ 2 + length xs + 1 + 1" |
|
100 |
using t_insort_length[of x "isort xs"] by (simp add: length_isort) |
|
101 |
also have "\<dots> \<le> (length(x#xs) + 1) ^ 2" |
|
102 |
by (simp add: power2_eq_square) |
|
103 |
finally show ?case . |
|
104 |
qed |
|
105 |
||
106 |
||
107 |
subsection "Merge Sort" |
|
108 |
||
109 |
fun merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
110 |
"merge [] ys = ys" | |
|
111 |
"merge xs [] = xs" | |
|
112 |
"merge (x#xs) (y#ys) = (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" |
|
113 |
||
114 |
fun msort :: "'a::linorder list \<Rightarrow> 'a list" where |
|
115 |
"msort xs = (let n = length xs in |
|
116 |
if n \<le> 1 then xs |
|
117 |
else merge (msort (take (n div 2) xs)) (msort (drop (n div 2) xs)))" |
|
118 |
||
119 |
declare msort.simps [simp del] |
|
120 |
||
68078 | 121 |
|
67983 | 122 |
subsubsection "Functional Correctness" |
123 |
||
124 |
lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys" |
|
125 |
by(induction xs ys rule: merge.induct) auto |
|
126 |
||
127 |
lemma "mset (msort xs) = mset xs" |
|
128 |
proof(induction xs rule: msort.induct) |
|
129 |
case (1 xs) |
|
130 |
let ?n = "length xs" |
|
131 |
let ?xs1 = "take (?n div 2) xs" |
|
132 |
let ?xs2 = "drop (?n div 2) xs" |
|
133 |
show ?case |
|
134 |
proof cases |
|
135 |
assume "?n \<le> 1" |
|
136 |
thus ?thesis by(simp add: msort.simps[of xs]) |
|
137 |
next |
|
138 |
assume "\<not> ?n \<le> 1" |
|
139 |
hence "mset (msort xs) = mset (msort ?xs1) + mset (msort ?xs2)" |
|
140 |
by(simp add: msort.simps[of xs] mset_merge) |
|
141 |
also have "\<dots> = mset ?xs1 + mset ?xs2" |
|
142 |
using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH") |
|
143 |
also have "\<dots> = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id) |
|
144 |
also have "\<dots> = mset xs" by simp |
|
145 |
finally show ?thesis . |
|
146 |
qed |
|
147 |
qed |
|
148 |
||
149 |
lemma set_merge: "set(merge xs ys) = set xs \<union> set ys" |
|
150 |
by(induction xs ys rule: merge.induct) (auto) |
|
151 |
||
152 |
lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)" |
|
153 |
by(induction xs ys rule: merge.induct) (auto simp: set_merge) |
|
154 |
||
155 |
lemma "sorted (msort xs)" |
|
156 |
proof(induction xs rule: msort.induct) |
|
157 |
case (1 xs) |
|
158 |
let ?n = "length xs" |
|
159 |
show ?case |
|
160 |
proof cases |
|
161 |
assume "?n \<le> 1" |
|
162 |
thus ?thesis by(simp add: msort.simps[of xs] sorted01) |
|
163 |
next |
|
164 |
assume "\<not> ?n \<le> 1" |
|
165 |
thus ?thesis using "1.IH" |
|
166 |
by(simp add: sorted_merge msort.simps[of xs] mset_merge) |
|
167 |
qed |
|
168 |
qed |
|
169 |
||
68078 | 170 |
|
171 |
subsubsection "Time Complexity" |
|
67983 | 172 |
|
173 |
text \<open>We only count the number of comparisons between list elements.\<close> |
|
66543 | 174 |
|
175 |
fun c_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
176 |
"c_merge [] ys = 0" | |
|
177 |
"c_merge xs [] = 0" | |
|
178 |
"c_merge (x#xs) (y#ys) = 1 + (if x \<le> y then c_merge xs (y#ys) else c_merge (x#xs) ys)" |
|
179 |
||
180 |
lemma c_merge_ub: "c_merge xs ys \<le> length xs + length ys" |
|
181 |
by (induction xs ys rule: c_merge.induct) auto |
|
182 |
||
183 |
fun c_msort :: "'a::linorder list \<Rightarrow> nat" where |
|
184 |
"c_msort xs = |
|
185 |
(let n = length xs; |
|
186 |
ys = take (n div 2) xs; |
|
187 |
zs = drop (n div 2) xs |
|
188 |
in if n \<le> 1 then 0 |
|
189 |
else c_msort ys + c_msort zs + c_merge (msort ys) (msort zs))" |
|
190 |
||
191 |
declare c_msort.simps [simp del] |
|
192 |
||
193 |
lemma length_merge: "length(merge xs ys) = length xs + length ys" |
|
194 |
apply (induction xs ys rule: merge.induct) |
|
195 |
apply auto |
|
196 |
done |
|
197 |
||
198 |
lemma length_msort: "length(msort xs) = length xs" |
|
199 |
proof (induction xs rule: msort.induct) |
|
200 |
case (1 xs) |
|
201 |
thus ?case by (auto simp: msort.simps[of xs] length_merge) |
|
202 |
qed |
|
203 |
text \<open>Why structured proof? |
|
204 |
To have the name "xs" to specialize msort.simps with xs |
|
205 |
to ensure that msort.simps cannot be used recursively. |
|
206 |
Also works without this precaution, but that is just luck.\<close> |
|
207 |
||
208 |
lemma c_msort_le: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> k * 2^k" |
|
209 |
proof(induction k arbitrary: xs) |
|
210 |
case 0 thus ?case by (simp add: c_msort.simps) |
|
211 |
next |
|
212 |
case (Suc k) |
|
213 |
let ?n = "length xs" |
|
214 |
let ?ys = "take (?n div 2) xs" |
|
215 |
let ?zs = "drop (?n div 2) xs" |
|
216 |
show ?case |
|
217 |
proof (cases "?n \<le> 1") |
|
218 |
case True |
|
219 |
thus ?thesis by(simp add: c_msort.simps) |
|
220 |
next |
|
221 |
case False |
|
222 |
have "c_msort(xs) = |
|
223 |
c_msort ?ys + c_msort ?zs + c_merge (msort ?ys) (msort ?zs)" |
|
224 |
by (simp add: c_msort.simps msort.simps) |
|
225 |
also have "\<dots> \<le> c_msort ?ys + c_msort ?zs + length ?ys + length ?zs" |
|
226 |
using c_merge_ub[of "msort ?ys" "msort ?zs"] length_msort[of ?ys] length_msort[of ?zs] |
|
227 |
by arith |
|
228 |
also have "\<dots> \<le> k * 2^k + c_msort ?zs + length ?ys + length ?zs" |
|
229 |
using Suc.IH[of ?ys] Suc.prems by simp |
|
230 |
also have "\<dots> \<le> k * 2^k + k * 2^k + length ?ys + length ?zs" |
|
231 |
using Suc.IH[of ?zs] Suc.prems by simp |
|
232 |
also have "\<dots> = 2 * k * 2^k + 2 * 2 ^ k" |
|
233 |
using Suc.prems by simp |
|
234 |
finally show ?thesis by simp |
|
235 |
qed |
|
236 |
qed |
|
237 |
||
238 |
(* Beware of conversions: *) |
|
239 |
lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)" |
|
240 |
using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps) |
|
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
66543
diff
changeset
|
241 |
by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult) |
66543 | 242 |
|
67983 | 243 |
|
244 |
subsection "Bottom-Up Merge Sort" |
|
245 |
||
246 |
(* Exercise: make tail recursive *) |
|
247 |
fun merge_adj :: "('a::linorder) list list \<Rightarrow> 'a list list" where |
|
248 |
"merge_adj [] = []" | |
|
249 |
"merge_adj [xs] = [xs]" | |
|
250 |
"merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss" |
|
251 |
||
252 |
text \<open>For the termination proof of \<open>merge_all\<close> below.\<close> |
|
253 |
lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2" |
|
254 |
by (induction xs rule: merge_adj.induct) auto |
|
255 |
||
256 |
fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where |
|
257 |
"merge_all [] = undefined" | |
|
258 |
"merge_all [xs] = xs" | |
|
259 |
"merge_all xss = merge_all (merge_adj xss)" |
|
260 |
||
261 |
definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where |
|
262 |
"msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))" |
|
263 |
||
68078 | 264 |
|
67983 | 265 |
subsubsection "Functional Correctness" |
266 |
||
267 |
lemma mset_merge_adj: |
|
268 |
"\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)" |
|
269 |
by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) |
|
270 |
||
271 |
lemma msec_merge_all: |
|
272 |
"xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))" |
|
273 |
by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj) |
|
274 |
||
275 |
lemma sorted_merge_adj: |
|
276 |
"\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs" |
|
277 |
by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge) |
|
278 |
||
279 |
lemma sorted_merge_all: |
|
280 |
"\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> xss \<noteq> [] \<Longrightarrow> sorted (merge_all xss)" |
|
281 |
apply(induction xss rule: merge_all.induct) |
|
282 |
using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj) |
|
283 |
||
284 |
lemma sorted_msort_bu: "sorted (msort_bu xs)" |
|
285 |
by(simp add: msort_bu_def sorted_merge_all) |
|
286 |
||
287 |
lemma mset_msort: "mset (msort_bu xs) = mset xs" |
|
288 |
by(simp add: msort_bu_def msec_merge_all comp_def) |
|
289 |
||
68078 | 290 |
|
291 |
subsubsection "Time Complexity" |
|
67983 | 292 |
|
68139 | 293 |
fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where |
67983 | 294 |
"c_merge_adj [] = 0" | |
68161 | 295 |
"c_merge_adj [xs] = 0" | |
296 |
"c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss" |
|
67983 | 297 |
|
68139 | 298 |
fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where |
68079 | 299 |
"c_merge_all [] = undefined" | |
68161 | 300 |
"c_merge_all [xs] = 0" | |
301 |
"c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)" |
|
67983 | 302 |
|
68139 | 303 |
definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where |
67983 | 304 |
"c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" |
305 |
||
306 |
lemma length_merge_adj: |
|
68161 | 307 |
"\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m" |
308 |
by(induction xss rule: merge_adj.induct) (auto simp: length_merge) |
|
67983 | 309 |
|
68161 | 310 |
lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss" |
311 |
proof(induction xss rule: c_merge_adj.induct) |
|
67983 | 312 |
case 1 thus ?case by simp |
313 |
next |
|
314 |
case 2 thus ?case by simp |
|
315 |
next |
|
316 |
case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps) |
|
317 |
qed |
|
318 |
||
68161 | 319 |
lemma c_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk> |
320 |
\<Longrightarrow> c_merge_all xss \<le> m * k * 2^k" |
|
321 |
proof (induction xss arbitrary: k m rule: c_merge_all.induct) |
|
67983 | 322 |
case 1 thus ?case by simp |
323 |
next |
|
68158 | 324 |
case 2 thus ?case by simp |
67983 | 325 |
next |
68162 | 326 |
case (3 xs ys xss) |
327 |
let ?xss = "xs # ys # xss" |
|
328 |
let ?xss2 = "merge_adj ?xss" |
|
67983 | 329 |
obtain k' where k': "k = Suc k'" using "3.prems"(2) |
330 |
by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
|
68162 | 331 |
have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
67983 | 332 |
from "3.prems"(1) length_merge_adj[OF this] |
68162 | 333 |
have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge) |
334 |
have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto |
|
335 |
have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp |
|
336 |
also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" |
|
67983 | 337 |
using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
338 |
also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
|
68079 | 339 |
using "3.IH"[OF * **] by simp |
67983 | 340 |
also have "\<dots> = m * k * 2^k" |
341 |
using k' by (simp add: algebra_simps) |
|
342 |
finally show ?case . |
|
343 |
qed |
|
344 |
||
345 |
corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k" |
|
346 |
using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def) |
|
347 |
||
66543 | 348 |
end |