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

src/HOL/ex/MergeSort.thy

author | nipkow |

Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) | |

changeset 30313 | b2441b0c8d38 |

parent 29780 | 1df0e5af40b9 |

child 30661 | 54858c8ad226 |

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

added lemmas

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

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 2002 TU Muenchen

5 *)

7 header{*Merge Sort*}

9 theory MergeSort

10 imports Sorting

11 begin

13 context linorder

14 begin

16 fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

17 where

18 "merge (x#xs) (y#ys) =

19 (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"

20 | "merge xs [] = xs"

21 | "merge [] ys = ys"

23 lemma multiset_of_merge[simp]:

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

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

26 apply (auto simp: union_ac)

27 done

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

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

31 apply auto

32 done

34 lemma sorted_merge[simp]:

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

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

37 apply(simp_all add: ball_Un not_le less_le)

38 apply(blast intro: order_trans)

39 done

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

42 where

43 "msort [] = []"

44 | "msort [x] = [x]"

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

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

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

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

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

52 apply (induct xs rule: msort.induct)

53 apply simp_all

54 apply (subst union_commute)

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

56 apply (simp add: union_ac)

57 done

59 end

62 end