17 "merge (x#xs) (y#ys) = |
17 "merge (x#xs) (y#ys) = |
18 (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" |
18 (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" |
19 | "merge xs [] = xs" |
19 | "merge xs [] = xs" |
20 | "merge [] ys = ys" |
20 | "merge [] ys = ys" |
21 |
21 |
22 lemma multiset_of_merge[simp]: |
22 lemma multiset_of_merge [simp]: |
23 "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" |
23 "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" |
24 apply(induct xs ys rule: merge.induct) |
24 by (induct xs ys rule: merge.induct) (simp_all add: ac_simps) |
25 apply (auto simp: union_ac) |
|
26 done |
|
27 |
25 |
28 lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys" |
26 lemma set_merge [simp]: |
29 apply(induct xs ys rule: merge.induct) |
27 "set (merge xs ys) = set xs \<union> set ys" |
30 apply auto |
28 by (induct xs ys rule: merge.induct) auto |
31 done |
|
32 |
29 |
33 lemma sorted_merge[simp]: |
30 lemma sorted_merge [simp]: |
34 "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)" |
31 "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys" |
35 apply(induct xs ys rule: merge.induct) |
32 by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons) |
36 apply(simp_all add: ball_Un not_le less_le) |
|
37 apply(blast intro: order_trans) |
|
38 done |
|
39 |
33 |
40 fun msort :: "'a list \<Rightarrow> 'a list" |
34 fun msort :: "'a list \<Rightarrow> 'a list" |
41 where |
35 where |
42 "msort [] = []" |
36 "msort [] = []" |
43 | "msort [x] = [x]" |
37 | "msort [x] = [x]" |
44 | "msort xs = merge (msort (take (size xs div 2) xs)) |
38 | "msort xs = merge (msort (take (size xs div 2) xs)) |
45 (msort (drop (size xs div 2) xs))" |
39 (msort (drop (size xs div 2) xs))" |
46 |
40 |
47 theorem sorted_msort: "sorted (op \<le>) (msort xs)" |
41 lemma sorted_msort: |
48 by (induct xs rule: msort.induct) simp_all |
42 "sorted (msort xs)" |
|
43 by (induct xs rule: msort.induct) simp_all |
49 |
44 |
50 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs" |
45 lemma multiset_of_msort: |
51 apply (induct xs rule: msort.induct) |
46 "multiset_of (msort xs) = multiset_of xs" |
52 apply simp_all |
47 by (induct xs rule: msort.induct) |
53 apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons) |
48 (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons) |
54 done |
49 |
|
50 theorem msort_sort: |
|
51 "sort = msort" |
|
52 by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+ |
55 |
53 |
56 end |
54 end |
57 |
55 |
58 |
|
59 end |
56 end |