src/HOL/ex/MergeSort.thy
author nipkow
Mon Jun 03 09:36:53 2002 +0200 (2002-06-03)
changeset 13201 3cc108872aca
child 15631 cbee04ce413b
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/ex/Merge.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TU Muenchen
     5 
     6 Merge sort
     7 *)
     8 
     9 theory MergeSort = Sorting:
    10 
    11 consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
    12 
    13 recdef merge "measure(%(xs,ys). size xs + size ys)"
    14 "merge(x#xs,y#ys) =
    15  (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
    16 "merge(xs,[]) = xs"
    17 "merge([],ys) = ys"
    18 
    19 lemma [simp]: "multiset(merge(xs,ys)) x = multiset xs x + multiset ys x"
    20 apply(induct xs ys rule: merge.induct)
    21 apply auto
    22 done
    23 
    24 lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
    25 apply(induct xs ys rule: merge.induct)
    26 apply auto
    27 done
    28 
    29 lemma [simp]:
    30  "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
    31 apply(induct xs ys rule: merge.induct)
    32 apply(simp_all add:ball_Un linorder_not_le order_less_le)
    33 apply(blast intro: order_trans)
    34 done
    35 
    36 consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
    37 recdef msort "measure size"
    38 "msort [] = []"
    39 "msort [x] = [x]"
    40 "msort xs = merge(msort(take (size xs div 2) xs),
    41                   msort(drop (size xs div 2) xs))"
    42 
    43 lemma "sorted op <= (msort xs)"
    44 by (induct xs rule: msort.induct) simp_all
    45 
    46 lemma "multiset(msort xs) x = multiset xs x"
    47 apply (induct xs rule: msort.induct)
    48   apply simp
    49  apply simp
    50 apply (simp del:multiset_append add:multiset_append[symmetric])
    51 done
    52 
    53 end