src/HOL/ex/MergeSort.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 19872 1b53b196f85f
child 29780 1df0e5af40b9
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     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