author | paulson |
Thu, 10 Dec 2009 17:34:18 +0000 | |
changeset 34055 | fdf294ee08b2 |
parent 32960 | 69916a850301 |
child 37076 | 4d57f872dc2c |
permissions | -rw-r--r-- |
34055 | 1 |
(* Title: HOL/ex/MergeSort.thy |
13201 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 2002 TU Muenchen |
|
4 |
*) |
|
5 |
||
15815 | 6 |
header{*Merge Sort*} |
7 |
||
8 |
theory MergeSort |
|
9 |
imports Sorting |
|
10 |
begin |
|
13201 | 11 |
|
29780 | 12 |
context linorder |
13 |
begin |
|
13201 | 14 |
|
29780 | 15 |
fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
16 |
where |
|
17 |
"merge (x#xs) (y#ys) = |
|
18 |
(if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" |
|
19 |
| "merge xs [] = xs" |
|
20 |
| "merge [] ys = ys" |
|
13201 | 21 |
|
15732 | 22 |
lemma multiset_of_merge[simp]: |
29780 | 23 |
"multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" |
13201 | 24 |
apply(induct xs ys rule: merge.induct) |
15631 | 25 |
apply (auto simp: union_ac) |
13201 | 26 |
done |
27 |
||
29780 | 28 |
lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys" |
13201 | 29 |
apply(induct xs ys rule: merge.induct) |
30 |
apply auto |
|
31 |
done |
|
32 |
||
15732 | 33 |
lemma sorted_merge[simp]: |
29780 | 34 |
"sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)" |
13201 | 35 |
apply(induct xs ys rule: merge.induct) |
29780 | 36 |
apply(simp_all add: ball_Un not_le less_le) |
13201 | 37 |
apply(blast intro: order_trans) |
38 |
done |
|
39 |
||
29780 | 40 |
fun msort :: "'a list \<Rightarrow> 'a list" |
41 |
where |
|
42 |
"msort [] = []" |
|
43 |
| "msort [x] = [x]" |
|
44 |
| "msort xs = merge (msort (take (size xs div 2) xs)) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30661
diff
changeset
|
45 |
(msort (drop (size xs div 2) xs))" |
13201 | 46 |
|
15815 | 47 |
theorem sorted_msort: "sorted (op \<le>) (msort xs)" |
13201 | 48 |
by (induct xs rule: msort.induct) simp_all |
49 |
||
15815 | 50 |
theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs" |
13201 | 51 |
apply (induct xs rule: msort.induct) |
15815 | 52 |
apply simp_all |
34055 | 53 |
apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons) |
13201 | 54 |
done |
55 |
||
56 |
end |
|
29780 | 57 |
|
58 |
||
59 |
end |