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

src/HOL/ex/MergeSort.thy

changeset 29780 | 1df0e5af40b9 |

parent 19872 | 1b53b196f85f |

child 30661 | 54858c8ad226 |

1.1 --- a/src/HOL/ex/MergeSort.thy Tue Feb 03 11:16:28 2009 +0100 1.2 +++ b/src/HOL/ex/MergeSort.thy Tue Feb 03 11:16:28 2009 +0100 1.3 @@ -10,40 +10,40 @@ 1.4 imports Sorting 1.5 begin 1.6 1.7 -consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list" 1.8 +context linorder 1.9 +begin 1.10 1.11 -recdef merge "measure(%(xs,ys). size xs + size ys)" 1.12 - "merge(x#xs, y#ys) = 1.13 - (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))" 1.14 - 1.15 - "merge(xs,[]) = xs" 1.16 - 1.17 - "merge([],ys) = ys" 1.18 +fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 1.19 +where 1.20 + "merge (x#xs) (y#ys) = 1.21 + (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" 1.22 +| "merge xs [] = xs" 1.23 +| "merge [] ys = ys" 1.24 1.25 lemma multiset_of_merge[simp]: 1.26 - "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys" 1.27 + "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" 1.28 apply(induct xs ys rule: merge.induct) 1.29 apply (auto simp: union_ac) 1.30 done 1.31 1.32 -lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys" 1.33 +lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys" 1.34 apply(induct xs ys rule: merge.induct) 1.35 apply auto 1.36 done 1.37 1.38 lemma sorted_merge[simp]: 1.39 - "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)" 1.40 + "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)" 1.41 apply(induct xs ys rule: merge.induct) 1.42 -apply(simp_all add: ball_Un linorder_not_le order_less_le) 1.43 +apply(simp_all add: ball_Un not_le less_le) 1.44 apply(blast intro: order_trans) 1.45 done 1.46 1.47 -consts msort :: "('a::linorder) list \<Rightarrow> 'a list" 1.48 -recdef msort "measure size" 1.49 - "msort [] = []" 1.50 - "msort [x] = [x]" 1.51 - "msort xs = merge(msort(take (size xs div 2) xs), 1.52 - msort(drop (size xs div 2) xs))" 1.53 +fun msort :: "'a list \<Rightarrow> 'a list" 1.54 +where 1.55 + "msort [] = []" 1.56 +| "msort [x] = [x]" 1.57 +| "msort xs = merge (msort (take (size xs div 2) xs)) 1.58 + (msort (drop (size xs div 2) xs))" 1.59 1.60 theorem sorted_msort: "sorted (op \<le>) (msort xs)" 1.61 by (induct xs rule: msort.induct) simp_all 1.62 @@ -57,3 +57,6 @@ 1.63 done 1.64 1.65 end 1.66 + 1.67 + 1.68 +end