*** empty log message ***
authornipkow
Mon Jun 03 09:36:53 2002 +0200 (2002-06-03)
changeset 132013cc108872aca
parent 13200 7618f289c9c1
child 13202 53022e5f73ff
*** empty log message ***
src/HOL/ex/MergeSort.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Mon Jun 03 09:36:53 2002 +0200
     1.3 @@ -0,0 +1,53 @@
     1.4 +(*  Title:      HOL/ex/Merge.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2002 TU Muenchen
     1.8 +
     1.9 +Merge sort
    1.10 +*)
    1.11 +
    1.12 +theory MergeSort = Sorting:
    1.13 +
    1.14 +consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
    1.15 +
    1.16 +recdef merge "measure(%(xs,ys). size xs + size ys)"
    1.17 +"merge(x#xs,y#ys) =
    1.18 + (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
    1.19 +"merge(xs,[]) = xs"
    1.20 +"merge([],ys) = ys"
    1.21 +
    1.22 +lemma [simp]: "multiset(merge(xs,ys)) x = multiset xs x + multiset ys x"
    1.23 +apply(induct xs ys rule: merge.induct)
    1.24 +apply auto
    1.25 +done
    1.26 +
    1.27 +lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
    1.28 +apply(induct xs ys rule: merge.induct)
    1.29 +apply auto
    1.30 +done
    1.31 +
    1.32 +lemma [simp]:
    1.33 + "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
    1.34 +apply(induct xs ys rule: merge.induct)
    1.35 +apply(simp_all add:ball_Un linorder_not_le order_less_le)
    1.36 +apply(blast intro: order_trans)
    1.37 +done
    1.38 +
    1.39 +consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
    1.40 +recdef msort "measure size"
    1.41 +"msort [] = []"
    1.42 +"msort [x] = [x]"
    1.43 +"msort xs = merge(msort(take (size xs div 2) xs),
    1.44 +                  msort(drop (size xs div 2) xs))"
    1.45 +
    1.46 +lemma "sorted op <= (msort xs)"
    1.47 +by (induct xs rule: msort.induct) simp_all
    1.48 +
    1.49 +lemma "multiset(msort xs) x = multiset xs x"
    1.50 +apply (induct xs rule: msort.induct)
    1.51 +  apply simp
    1.52 + apply simp
    1.53 +apply (simp del:multiset_append add:multiset_append[symmetric])
    1.54 +done
    1.55 +
    1.56 +end