src/HOL/ex/MergeSort.thy
author paulson
Thu Dec 10 17:34:18 2009 +0000 (2009-12-10)
changeset 34055 fdf294ee08b2
parent 32960 69916a850301
child 37076 4d57f872dc2c
permissions -rw-r--r--
streamlined 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 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 (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
    54 done
    55 
    56 end
    57 
    58 
    59 end