src/HOL/ex/MergeSort.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61343 5b5656a63bd6
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
bundle lifting_syntax;
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
wenzelm@61343
     6
section\<open>Merge Sort\<close>
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
nipkow@60515
    22
lemma mset_merge [simp]:
nipkow@60515
    23
  "mset (merge xs ys) = mset xs + mset 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
nipkow@60515
    45
lemma mset_msort:
nipkow@60515
    46
  "mset (msort xs) = mset xs"
haftmann@37076
    47
  by (induct xs rule: msort.induct)
nipkow@60515
    48
    (simp_all, metis append_take_drop_id drop_Suc_Cons mset.simps(2) mset_append take_Suc_Cons)
haftmann@37076
    49
haftmann@37076
    50
theorem msort_sort:
haftmann@37076
    51
  "sort = msort"
nipkow@60515
    52
  by (rule ext, rule properties_for_sort) (fact mset_msort sorted_msort)+
nipkow@13201
    53
nipkow@13201
    54
end
krauss@29780
    55
krauss@29780
    56
end