13201
|
1 |
(* Title: HOL/ex/Merge.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2002 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
15815
|
7 |
header{*Merge Sort*}
|
|
8 |
|
|
9 |
theory MergeSort
|
|
10 |
imports Sorting
|
|
11 |
begin
|
13201
|
12 |
|
29780
|
13 |
context linorder
|
|
14 |
begin
|
13201
|
15 |
|
29780
|
16 |
fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
|
17 |
where
|
|
18 |
"merge (x#xs) (y#ys) =
|
|
19 |
(if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
|
|
20 |
| "merge xs [] = xs"
|
|
21 |
| "merge [] ys = ys"
|
13201
|
22 |
|
15732
|
23 |
lemma multiset_of_merge[simp]:
|
29780
|
24 |
"multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
|
13201
|
25 |
apply(induct xs ys rule: merge.induct)
|
15631
|
26 |
apply (auto simp: union_ac)
|
13201
|
27 |
done
|
|
28 |
|
29780
|
29 |
lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
|
13201
|
30 |
apply(induct xs ys rule: merge.induct)
|
|
31 |
apply auto
|
|
32 |
done
|
|
33 |
|
15732
|
34 |
lemma sorted_merge[simp]:
|
29780
|
35 |
"sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
|
13201
|
36 |
apply(induct xs ys rule: merge.induct)
|
29780
|
37 |
apply(simp_all add: ball_Un not_le less_le)
|
13201
|
38 |
apply(blast intro: order_trans)
|
|
39 |
done
|
|
40 |
|
29780
|
41 |
fun msort :: "'a list \<Rightarrow> 'a list"
|
|
42 |
where
|
|
43 |
"msort [] = []"
|
|
44 |
| "msort [x] = [x]"
|
|
45 |
| "msort xs = merge (msort (take (size xs div 2) xs))
|
|
46 |
(msort (drop (size xs div 2) xs))"
|
13201
|
47 |
|
15815
|
48 |
theorem sorted_msort: "sorted (op \<le>) (msort xs)"
|
13201
|
49 |
by (induct xs rule: msort.induct) simp_all
|
|
50 |
|
15815
|
51 |
theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
|
13201
|
52 |
apply (induct xs rule: msort.induct)
|
15815
|
53 |
apply simp_all
|
19872
|
54 |
apply (subst union_commute)
|
15631
|
55 |
apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
|
|
56 |
apply (simp add: union_ac)
|
13201
|
57 |
done
|
|
58 |
|
|
59 |
end
|
29780
|
60 |
|
|
61 |
|
|
62 |
end
|