src/HOL/ex/MergeSort.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 41413 64cd30d6b0b8 child 58889 5b7a9633cfa8 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 (*  Title:      HOL/ex/MergeSort.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   2002 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header{*Merge Sort*}
```
```     7
```
```     8 theory MergeSort
```
```     9 imports "~~/src/HOL/Library/Multiset"
```
```    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   by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
```
```    25
```
```    26 lemma set_merge [simp]:
```
```    27   "set (merge xs ys) = set xs \<union> set ys"
```
```    28   by (induct xs ys rule: merge.induct) auto
```
```    29
```
```    30 lemma sorted_merge [simp]:
```
```    31   "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
```
```    32   by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
```
```    33
```
```    34 fun msort :: "'a list \<Rightarrow> 'a list"
```
```    35 where
```
```    36   "msort [] = []"
```
```    37 | "msort [x] = [x]"
```
```    38 | "msort xs = merge (msort (take (size xs div 2) xs))
```
```    39                     (msort (drop (size xs div 2) xs))"
```
```    40
```
```    41 lemma sorted_msort:
```
```    42   "sorted (msort xs)"
```
```    43   by (induct xs rule: msort.induct) simp_all
```
```    44
```
```    45 lemma multiset_of_msort:
```
```    46   "multiset_of (msort xs) = multiset_of xs"
```
```    47   by (induct xs rule: msort.induct)
```
```    48     (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
```
```    49
```
```    50 theorem msort_sort:
```
```    51   "sort = msort"
```
```    52   by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
```
```    53
```
```    54 end
```
```    55
```
```    56 end
```