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 |
|
15631
|
19 |
lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
|
13201
|
20 |
apply(induct xs ys rule: merge.induct)
|
15631
|
21 |
apply (auto simp: union_ac)
|
13201
|
22 |
done
|
|
23 |
|
|
24 |
lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
|
|
25 |
apply(induct xs ys rule: merge.induct)
|
|
26 |
apply auto
|
|
27 |
done
|
|
28 |
|
|
29 |
lemma [simp]:
|
|
30 |
"sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
|
|
31 |
apply(induct xs ys rule: merge.induct)
|
|
32 |
apply(simp_all add:ball_Un linorder_not_le order_less_le)
|
|
33 |
apply(blast intro: order_trans)
|
|
34 |
done
|
|
35 |
|
|
36 |
consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
|
|
37 |
recdef msort "measure size"
|
|
38 |
"msort [] = []"
|
|
39 |
"msort [x] = [x]"
|
|
40 |
"msort xs = merge(msort(take (size xs div 2) xs),
|
|
41 |
msort(drop (size xs div 2) xs))"
|
|
42 |
|
|
43 |
lemma "sorted op <= (msort xs)"
|
|
44 |
by (induct xs rule: msort.induct) simp_all
|
|
45 |
|
15631
|
46 |
lemma "multiset_of (msort xs) = multiset_of xs"
|
13201
|
47 |
apply (induct xs rule: msort.induct)
|
|
48 |
apply simp
|
|
49 |
apply simp
|
15631
|
50 |
apply simp
|
|
51 |
apply (subst union_commute)
|
|
52 |
apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
|
|
53 |
apply (simp add: union_ac)
|
13201
|
54 |
done
|
|
55 |
|
|
56 |
end
|