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

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 *)

6 section{*Merge Sort*}

8 theory MergeSort

9 imports "~~/src/HOL/Library/Multiset"

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 by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)

26 lemma set_merge [simp]:

27 "set (merge xs ys) = set xs \<union> set ys"

28 by (induct xs ys rule: merge.induct) auto

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)

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))"

41 lemma sorted_msort:

42 "sorted (msort xs)"

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

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)

50 theorem msort_sort:

51 "sort = msort"

52 by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+

54 end

56 end