src/HOL/ex/MergeSort.thy
author nipkow
Thu Apr 14 17:57:23 2005 +0200 (2005-04-14)
changeset 15732 faa48c5b1402
parent 15631 cbee04ce413b
child 15815 62854cac5410
permissions -rw-r--r--
Added thm names
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
Merge sort
nipkow@13201
     7
*)
nipkow@13201
     8
nipkow@13201
     9
theory MergeSort = Sorting:
nipkow@13201
    10
nipkow@13201
    11
consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
nipkow@13201
    12
nipkow@13201
    13
recdef merge "measure(%(xs,ys). size xs + size ys)"
nipkow@13201
    14
"merge(x#xs,y#ys) =
nipkow@13201
    15
 (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
nipkow@13201
    16
"merge(xs,[]) = xs"
nipkow@13201
    17
"merge([],ys) = ys"
nipkow@13201
    18
nipkow@15732
    19
lemma multiset_of_merge[simp]:
nipkow@15732
    20
 "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
nipkow@13201
    21
apply(induct xs ys rule: merge.induct)
kleing@15631
    22
apply (auto simp: union_ac)
nipkow@13201
    23
done
nipkow@13201
    24
nipkow@15732
    25
lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
nipkow@13201
    26
apply(induct xs ys rule: merge.induct)
nipkow@13201
    27
apply auto
nipkow@13201
    28
done
nipkow@13201
    29
nipkow@15732
    30
lemma sorted_merge[simp]:
nipkow@13201
    31
 "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
nipkow@13201
    32
apply(induct xs ys rule: merge.induct)
nipkow@13201
    33
apply(simp_all add:ball_Un linorder_not_le order_less_le)
nipkow@13201
    34
apply(blast intro: order_trans)
nipkow@13201
    35
done
nipkow@13201
    36
nipkow@13201
    37
consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
nipkow@13201
    38
recdef msort "measure size"
nipkow@13201
    39
"msort [] = []"
nipkow@13201
    40
"msort [x] = [x]"
nipkow@13201
    41
"msort xs = merge(msort(take (size xs div 2) xs),
nipkow@13201
    42
                  msort(drop (size xs div 2) xs))"
nipkow@13201
    43
nipkow@15732
    44
lemma sorted_msort: "sorted op <= (msort xs)"
nipkow@13201
    45
by (induct xs rule: msort.induct) simp_all
nipkow@13201
    46
nipkow@15732
    47
lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
nipkow@13201
    48
apply (induct xs rule: msort.induct)
nipkow@13201
    49
  apply simp
nipkow@13201
    50
 apply simp
kleing@15631
    51
apply simp
kleing@15631
    52
apply (subst union_commute)
kleing@15631
    53
apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
kleing@15631
    54
apply (simp add: union_ac)
nipkow@13201
    55
done
nipkow@13201
    56
nipkow@13201
    57
end