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 |
|
|
13 |
consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
|
|
14 |
|
|
15 |
recdef merge "measure(%(xs,ys). size xs + size ys)"
|
15815
|
16 |
"merge(x#xs, y#ys) =
|
|
17 |
(if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
|
|
18 |
|
|
19 |
"merge(xs,[]) = xs"
|
|
20 |
|
|
21 |
"merge([],ys) = ys"
|
13201
|
22 |
|
15732
|
23 |
lemma multiset_of_merge[simp]:
|
15815
|
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 |
|
15732
|
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]:
|
15815
|
35 |
"sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
|
13201
|
36 |
apply(induct xs ys rule: merge.induct)
|
15815
|
37 |
apply(simp_all add: ball_Un linorder_not_le order_less_le)
|
13201
|
38 |
apply(blast intro: order_trans)
|
|
39 |
done
|
|
40 |
|
|
41 |
consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
|
|
42 |
recdef msort "measure size"
|
15815
|
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
|