src/HOL/ex/MergeSort.thy
 author paulson Fri Apr 22 17:32:03 2005 +0200 (2005-04-22) changeset 15815 62854cac5410 parent 15732 faa48c5b1402 child 19860 6e44610bdd76 permissions -rw-r--r--
tidied
```     1 (*  Title:      HOL/ex/Merge.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4     Copyright   2002 TU Muenchen
```
```     5 *)
```
```     6
```
```     7 header{*Merge Sort*}
```
```     8
```
```     9 theory MergeSort
```
```    10 imports Sorting
```
```    11 begin
```
```    12
```
```    13 consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
```
```    14
```
```    15 recdef merge "measure(%(xs,ys). size xs + size ys)"
```
```    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"
```
```    22
```
```    23 lemma multiset_of_merge[simp]:
```
```    24      "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
```
```    25 apply(induct xs ys rule: merge.induct)
```
```    26 apply (auto simp: union_ac)
```
```    27 done
```
```    28
```
```    29 lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
```
```    30 apply(induct xs ys rule: merge.induct)
```
```    31 apply auto
```
```    32 done
```
```    33
```
```    34 lemma sorted_merge[simp]:
```
```    35      "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
```
```    36 apply(induct xs ys rule: merge.induct)
```
```    37 apply(simp_all add: ball_Un linorder_not_le order_less_le)
```
```    38 apply(blast intro: order_trans)
```
```    39 done
```
```    40
```
```    41 consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
```
```    42 recdef msort "measure size"
```
```    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))"
```
```    47
```
```    48 theorem sorted_msort: "sorted (op \<le>) (msort xs)"
```
```    49 by (induct xs rule: msort.induct) simp_all
```
```    50
```
```    51 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
```
```    52 apply (induct xs rule: msort.induct)
```
```    53   apply simp_all
```
```    54 apply (subst union_commute)
```
```    55 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
```
```    56 apply (simp add: union_ac)
```
```    57 done
```
```    58
```
```    59 end
```