src/HOL/ex/MergeSort.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 41413 64cd30d6b0b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
paulson@34055
     1
(*  Title:      HOL/ex/MergeSort.thy
nipkow@13201
     2
    Author:     Tobias Nipkow
nipkow@13201
     3
    Copyright   2002 TU Muenchen
nipkow@13201
     4
*)
nipkow@13201
     5
paulson@15815
     6
header{*Merge Sort*}
paulson@15815
     7
paulson@15815
     8
theory MergeSort
wenzelm@41413
     9
imports "~~/src/HOL/Library/Multiset"
paulson@15815
    10
begin
nipkow@13201
    11
krauss@29780
    12
context linorder
krauss@29780
    13
begin
nipkow@13201
    14
krauss@29780
    15
fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
krauss@29780
    16
where
krauss@29780
    17
  "merge (x#xs) (y#ys) =
krauss@29780
    18
         (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
krauss@29780
    19
| "merge xs [] = xs"
krauss@29780
    20
| "merge [] ys = ys"
nipkow@13201
    21
haftmann@37076
    22
lemma multiset_of_merge [simp]:
haftmann@37076
    23
  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
haftmann@37076
    24
  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
nipkow@13201
    25
haftmann@37076
    26
lemma set_merge [simp]:
haftmann@37076
    27
  "set (merge xs ys) = set xs \<union> set ys"
haftmann@37076
    28
  by (induct xs ys rule: merge.induct) auto
nipkow@13201
    29
haftmann@37076
    30
lemma sorted_merge [simp]:
haftmann@37076
    31
  "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
haftmann@37076
    32
  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
nipkow@13201
    33
krauss@29780
    34
fun msort :: "'a list \<Rightarrow> 'a list"
krauss@29780
    35
where
krauss@29780
    36
  "msort [] = []"
krauss@29780
    37
| "msort [x] = [x]"
krauss@29780
    38
| "msort xs = merge (msort (take (size xs div 2) xs))
wenzelm@32960
    39
                    (msort (drop (size xs div 2) xs))"
nipkow@13201
    40
haftmann@37076
    41
lemma sorted_msort:
haftmann@37076
    42
  "sorted (msort xs)"
haftmann@37076
    43
  by (induct xs rule: msort.induct) simp_all
nipkow@13201
    44
haftmann@37076
    45
lemma multiset_of_msort:
haftmann@37076
    46
  "multiset_of (msort xs) = multiset_of xs"
haftmann@37076
    47
  by (induct xs rule: msort.induct)
haftmann@37076
    48
    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
haftmann@37076
    49
haftmann@37076
    50
theorem msort_sort:
haftmann@37076
    51
  "sort = msort"
haftmann@37076
    52
  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
nipkow@13201
    53
nipkow@13201
    54
end
krauss@29780
    55
krauss@29780
    56
end