src/HOL/ex/MergeSort.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 30661 54858c8ad226
child 34055 fdf294ee08b2
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     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