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