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

src/HOL/ex/MergeSort.thy

author | paulson |

Thu Dec 10 17:34:18 2009 +0000 (2009-12-10) | |

changeset 34055 | fdf294ee08b2 |

parent 32960 | 69916a850301 |

child 37076 | 4d57f872dc2c |

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

streamlined proofs

1 (* Title: HOL/ex/MergeSort.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 (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)

54 done

56 end

59 end