1(* Author: Tobias Nipkow *)
2
3theory Sorting
4imports
5  Complex_Main
6  "HOL-Library.Multiset"
7begin
8
9hide_const List.insort
10
11declare Let_def [simp]
12
13
14subsection "Insertion Sort"
15
16fun 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
21fun isort :: "'a::linorder list \<Rightarrow> 'a list" where
22"isort [] = []" |
23"isort (x#xs) = insort x (isort xs)"
24
25
26subsubsection "Functional Correctness"
27
28lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)"
29apply(induction xs)
30apply auto
31done
32
33lemma mset_isort: "mset (isort xs) = mset xs"
34apply(induction xs)
35apply simp
36apply (simp add: mset_insort)
37done
38
39lemma set_insort: "set (insort x xs) = insert x (set xs)"
40by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
41
42lemma sorted_insort: "sorted (insort a xs) = sorted xs"
43apply(induction xs)
44apply(auto simp add: set_insort)
45done
46
47lemma "sorted (isort xs)"
48apply(induction xs)
49apply(auto simp: sorted_insort)
50done
51
52
53subsubsection "Time Complexity"
54
55text \<open>We count the number of function calls.\<close>
56
57text\<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>
62fun 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
67text\<open>
68\<open>isort [] = []\<close>
69\<open>isort (x#xs) = insort x (isort xs)\<close>
70\<close>
71fun 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
76lemma t_insort_length: "t_insort x xs \<le> length xs + 1"
77apply(induction xs)
78apply auto
79done
80
81lemma length_insort: "length (insort x xs) = length xs + 1"
82apply(induction xs)
83apply auto
84done
85
86lemma length_isort: "length (isort xs) = length xs"
87apply(induction xs)
88apply (auto simp: length_insort)
89done
90
91lemma t_isort_length: "t_isort xs \<le> (length xs + 1) ^ 2"
92proof(induction xs)
93  case Nil show ?case by simp
94next
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 .
104qed
105
106
107subsection "Merge Sort"
108
109fun 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
114fun 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
119declare msort.simps [simp del]
120
121
122subsubsection "Functional Correctness"
123
124lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys"
125by(induction xs ys rule: merge.induct) auto
126
127lemma "mset (msort xs) = mset xs"
128proof(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
147qed
148
149lemma set_merge: "set(merge xs ys) = set xs \<union> set ys"
150by(induction xs ys rule: merge.induct) (auto)
151
152lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)"
153by(induction xs ys rule: merge.induct) (auto simp: set_merge)
154
155lemma "sorted (msort xs)"
156proof(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
168qed
169
170
171subsubsection "Time Complexity"
172
173text \<open>We only count the number of comparisons between list elements.\<close>
174
175fun 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
180lemma c_merge_ub: "c_merge xs ys \<le> length xs + length ys"
181by (induction xs ys rule: c_merge.induct) auto
182
183fun 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
191declare c_msort.simps [simp del]
192
193lemma length_merge: "length(merge xs ys) = length xs + length ys"
194apply (induction xs ys rule: merge.induct)
195apply auto
196done
197
198lemma length_msort: "length(msort xs) = length xs"
199proof (induction xs rule: msort.induct)
200  case (1 xs)
201  thus ?case by (auto simp: msort.simps[of xs] length_merge)
202qed
203text \<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.
206Also works without this precaution, but that is just luck.\<close>
207
208lemma c_msort_le: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> k * 2^k"
209proof(induction k arbitrary: xs)
210  case 0 thus ?case by (simp add: c_msort.simps)
211next
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
236qed
237
238(* Beware of conversions: *)
239lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
240using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
241by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
242
243
244subsection "Bottom-Up Merge Sort"
245
246(* Exercise: make tail recursive *)
247fun 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
252text \<open>For the termination proof of \<open>merge_all\<close> below.\<close>
253lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2"
254by (induction xs rule: merge_adj.induct) auto
255
256fun 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
261definition 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
264
265subsubsection "Functional Correctness"
266
267lemma mset_merge_adj:
268  "\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)"
269by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
270
271lemma msec_merge_all:
272  "xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
273by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
274
275lemma sorted_merge_adj:
276  "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"
277by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
278
279lemma sorted_merge_all:
280  "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> xss \<noteq> [] \<Longrightarrow> sorted (merge_all xss)"
281apply(induction xss rule: merge_all.induct)
282using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
283
284lemma sorted_msort_bu: "sorted (msort_bu xs)"
285by(simp add: msort_bu_def sorted_merge_all)
286
287lemma mset_msort: "mset (msort_bu xs) = mset xs"
288by(simp add: msort_bu_def msec_merge_all comp_def)
289
290
291subsubsection "Time Complexity"
292
293fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
294"c_merge_adj [] = 0" |
295"c_merge_adj [xs] = 0" |
296"c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss"
297
298fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
299"c_merge_all [] = undefined" |
300"c_merge_all [xs] = 0" |
301"c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)"
302
303definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
304"c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
305
306lemma length_merge_adj:
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"
308by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
309
310lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss"
311proof(induction xss rule: c_merge_adj.induct)
312  case 1 thus ?case by simp
313next
314  case 2 thus ?case by simp
315next
316  case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps)
317qed
318
319lemma 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"
321proof (induction xss arbitrary: k m rule: c_merge_all.induct)
322  case 1 thus ?case by simp
323next
324  case 2 thus ?case by simp
325next
326  case (3 xs ys xss)
327  let ?xss = "xs # ys # xss"
328  let ?xss2 = "merge_adj ?xss"
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)
331  have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce
332  from "3.prems"(1) length_merge_adj[OF this]
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"
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'"
339    using "3.IH"[OF * **] by simp
340  also have "\<dots> = m * k * 2^k"
341    using k' by (simp add: algebra_simps)
342  finally show ?case .
343qed
344
345corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k"
346using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def)
347
348end
349