src/HOL/ex/MergeSort.thy
author dixon
Tue Jun 13 15:42:52 2006 +0200 (2006-06-13)
changeset 19872 1b53b196f85f
parent 19860 6e44610bdd76
child 29780 1df0e5af40b9
permissions -rw-r--r--
corrected w.r.t. search order for subst.
nipkow@13201
     1
(*  Title:      HOL/ex/Merge.thy
nipkow@13201
     2
    ID:         $Id$
nipkow@13201
     3
    Author:     Tobias Nipkow
nipkow@13201
     4
    Copyright   2002 TU Muenchen
nipkow@13201
     5
*)
nipkow@13201
     6
paulson@15815
     7
header{*Merge Sort*}
paulson@15815
     8
paulson@15815
     9
theory MergeSort
paulson@15815
    10
imports Sorting
paulson@15815
    11
begin
nipkow@13201
    12
nipkow@13201
    13
consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
nipkow@13201
    14
nipkow@13201
    15
recdef merge "measure(%(xs,ys). size xs + size ys)"
paulson@15815
    16
    "merge(x#xs, y#ys) =
paulson@15815
    17
         (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
paulson@15815
    18
paulson@15815
    19
    "merge(xs,[]) = xs"
paulson@15815
    20
paulson@15815
    21
    "merge([],ys) = ys"
nipkow@13201
    22
nipkow@15732
    23
lemma multiset_of_merge[simp]:
paulson@15815
    24
     "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
nipkow@13201
    25
apply(induct xs ys rule: merge.induct)
kleing@15631
    26
apply (auto simp: union_ac)
nipkow@13201
    27
done
nipkow@13201
    28
nipkow@15732
    29
lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
nipkow@13201
    30
apply(induct xs ys rule: merge.induct)
nipkow@13201
    31
apply auto
nipkow@13201
    32
done
nipkow@13201
    33
nipkow@15732
    34
lemma sorted_merge[simp]:
paulson@15815
    35
     "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
nipkow@13201
    36
apply(induct xs ys rule: merge.induct)
paulson@15815
    37
apply(simp_all add: ball_Un linorder_not_le order_less_le)
nipkow@13201
    38
apply(blast intro: order_trans)
nipkow@13201
    39
done
nipkow@13201
    40
nipkow@13201
    41
consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
nipkow@13201
    42
recdef msort "measure size"
paulson@15815
    43
    "msort [] = []"
paulson@15815
    44
    "msort [x] = [x]"
paulson@15815
    45
    "msort xs = merge(msort(take (size xs div 2) xs),
paulson@15815
    46
		      msort(drop (size xs div 2) xs))"
nipkow@13201
    47
paulson@15815
    48
theorem sorted_msort: "sorted (op \<le>) (msort xs)"
nipkow@13201
    49
by (induct xs rule: msort.induct) simp_all
nipkow@13201
    50
paulson@15815
    51
theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
nipkow@13201
    52
apply (induct xs rule: msort.induct)
paulson@15815
    53
  apply simp_all
dixon@19872
    54
apply (subst union_commute)
kleing@15631
    55
apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
kleing@15631
    56
apply (simp add: union_ac)
nipkow@13201
    57
done
nipkow@13201
    58
nipkow@13201
    59
end