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