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