# Theory MergeSort

Up to index of Isabelle/HOL/ex

theory MergeSort
imports Sorting
begin

    (*  Title:      HOL/ex/Merge.thy
        ID:         $Id: MergeSort.thy,v 1.4 2005/04/22 15:32:03 paulson Exp $
        Author:     Tobias Nipkow
        Copyright   2002 TU Muenchen
    *)

    header{*Merge Sort*}

    theory MergeSort
    imports Sorting
    begin

    consts merge :: "('a::linorder)list * 'a list => 'a list"

    recdef merge "measure(%(xs,ys). size xs + size ys)"
        "merge(x#xs, y#ys) =
             (if x ≤ y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"

        "merge(xs,[]) = xs"

        "merge([],ys) = ys"

    lemma multiset_of_merge[simp]:
         "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    apply(induct xs ys rule: merge.induct)
    apply (auto simp: union_ac)
    done

    lemma set_merge[simp]: "set(merge(xs,ys)) = set xs ∪ set ys"
    apply(induct xs ys rule: merge.induct)
    apply auto
    done

    lemma sorted_merge[simp]:
         "sorted (op ≤) (merge(xs,ys)) = (sorted (op ≤) xs & sorted (op ≤) ys)"
    apply(induct xs ys rule: merge.induct)
    apply(simp_all add: ball_Un linorder_not_le order_less_le)
    apply(blast intro: order_trans)
    done

    consts msort :: "('a::linorder) list => 'a list"
    recdef msort "measure size"
        "msort [] = []"
        "msort [x] = [x]"
        "msort xs = merge(msort(take (size xs div 2) xs),
                          msort(drop (size xs div 2) xs))"

    theorem sorted_msort: "sorted (op ≤) (msort xs)"
    by (induct xs rule: msort.induct) simp_all

    theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    apply (induct xs rule: msort.induct)
      apply simp_all
    apply (subst union_commute)
    apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    apply (simp add: union_ac)
    done

    end

lemma multiset_of_merge:

      multiset_of (merge (xs, ys)) = multiset_of xs + multiset_of ys

lemma set_merge:

      set (merge (xs, ys)) = set xs ∪ set ys

lemma sorted_merge:

      sorted op ≤ (merge (xs, ys)) = (sorted op ≤ xs ∧ sorted op ≤ ys)

theorem sorted_msort:

      sorted op ≤ (msort xs)

theorem multiset_of_msort:

      multiset_of (msort xs) = multiset_of xs