src/HOL/ex/MergeSort.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29780 1df0e5af40b9
child 30661 54858c8ad226
permissions -rw-r--r--
added lemmas
     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 context linorder
    14 begin
    15 
    16 fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    17 where
    18   "merge (x#xs) (y#ys) =
    19          (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
    20 | "merge xs [] = xs"
    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 not_le less_le)
    38 apply(blast intro: order_trans)
    39 done
    40 
    41 fun msort :: "'a list \<Rightarrow> 'a list"
    42 where
    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
    60 
    61 
    62 end