src/HOL/ex/MergeSort.thy
author krauss
Tue Feb 03 11:16:28 2009 +0100 (2009-02-03)
changeset 29780 1df0e5af40b9
parent 19872 1b53b196f85f
child 30661 54858c8ad226
permissions -rw-r--r--
mergesort example: recdef->fun, localized
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
krauss@29780
    13
context linorder
krauss@29780
    14
begin
nipkow@13201
    15
krauss@29780
    16
fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
krauss@29780
    17
where
krauss@29780
    18
  "merge (x#xs) (y#ys) =
krauss@29780
    19
         (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
krauss@29780
    20
| "merge xs [] = xs"
krauss@29780
    21
| "merge [] ys = ys"
nipkow@13201
    22
nipkow@15732
    23
lemma multiset_of_merge[simp]:
krauss@29780
    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
krauss@29780
    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]:
krauss@29780
    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)
krauss@29780
    37
apply(simp_all add: ball_Un not_le less_le)
nipkow@13201
    38
apply(blast intro: order_trans)
nipkow@13201
    39
done
nipkow@13201
    40
krauss@29780
    41
fun msort :: "'a list \<Rightarrow> 'a list"
krauss@29780
    42
where
krauss@29780
    43
  "msort [] = []"
krauss@29780
    44
| "msort [x] = [x]"
krauss@29780
    45
| "msort xs = merge (msort (take (size xs div 2) xs))
krauss@29780
    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
krauss@29780
    60
krauss@29780
    61
krauss@29780
    62
end