summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/MergeSort.thy

author | haftmann |

Mon Mar 23 08:14:23 2009 +0100 (2009-03-23) | |

changeset 30661 | 54858c8ad226 |

parent 29780 | 1df0e5af40b9 |

child 32960 | 69916a850301 |

permissions | -rw-r--r-- |

tuned header

1 (* Title: HOL/ex/Merge.thy

2 Author: Tobias Nipkow

3 Copyright 2002 TU Muenchen

4 *)

6 header{*Merge Sort*}

8 theory MergeSort

9 imports Sorting

10 begin

12 context linorder

13 begin

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"

22 lemma multiset_of_merge[simp]:

23 "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"

24 apply(induct xs ys rule: merge.induct)

25 apply (auto simp: union_ac)

26 done

28 lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"

29 apply(induct xs ys rule: merge.induct)

30 apply auto

31 done

33 lemma sorted_merge[simp]:

34 "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"

35 apply(induct xs ys rule: merge.induct)

36 apply(simp_all add: ball_Un not_le less_le)

37 apply(blast intro: order_trans)

38 done

40 fun msort :: "'a list \<Rightarrow> 'a list"

41 where

42 "msort [] = []"

43 | "msort [x] = [x]"

44 | "msort xs = merge (msort (take (size xs div 2) xs))

45 (msort (drop (size xs div 2) xs))"

47 theorem sorted_msort: "sorted (op \<le>) (msort xs)"

48 by (induct xs rule: msort.induct) simp_all

50 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"

51 apply (induct xs rule: msort.induct)

52 apply simp_all

53 apply (subst union_commute)

54 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)

55 apply (simp add: union_ac)

56 done

58 end

61 end