summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sat, 22 May 2010 11:01:59 +0200 | |

changeset 37077 | 3b247fa77c68 |

parent 37057 | e70f9230c608 (current diff) |

parent 37076 | 4d57f872dc2c (diff) |

child 37086 | 3a7c2c949320 |

merged

--- a/src/HOL/Library/Multiset.thy Fri May 21 23:48:48 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Sat May 22 11:01:59 2010 +0200 @@ -826,7 +826,8 @@ This lemma shows which properties suffice to show that a function @{text "f"} with @{text "f xs = ys"} behaves like sort. *} -lemma properties_for_sort: + +lemma (in linorder) properties_for_sort: "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp

--- a/src/HOL/Library/Quicksort.thy Fri May 21 23:48:48 2010 +0200 +++ b/src/HOL/Library/Quicksort.thy Sat May 22 11:01:59 2010 +0200 @@ -2,7 +2,7 @@ Copyright 1994 TU Muenchen *) -header{*Quicksort*} +header {* Quicksort *} theory Quicksort imports Main Multiset @@ -12,22 +12,27 @@ begin fun quicksort :: "'a list \<Rightarrow> 'a list" where -"quicksort [] = []" | -"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])" + "quicksort [] = []" +| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]" + +lemma [code]: + "quicksort [] = []" + "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]" + by (simp_all add: not_le) lemma quicksort_permutes [simp]: "multiset_of (quicksort xs) = multiset_of xs" -by (induct xs rule: quicksort.induct) (auto simp: union_ac) + by (induct xs rule: quicksort.induct) (simp_all add: ac_simps) lemma set_quicksort [simp]: "set (quicksort xs) = set xs" -by(simp add: set_count_greater_0) + by (simp add: set_count_greater_0) -lemma sorted_quicksort: "sorted(quicksort xs)" -apply (induct xs rule: quicksort.induct) - apply simp -apply (simp add:sorted_Cons sorted_append not_le less_imp_le) -apply (metis leD le_cases le_less_trans) -done +lemma sorted_quicksort: "sorted (quicksort xs)" + by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le) + +theorem quicksort_sort [code_unfold]: + "sort = quicksort" + by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+ end

--- a/src/HOL/ex/MergeSort.thy Fri May 21 23:48:48 2010 +0200 +++ b/src/HOL/ex/MergeSort.thy Sat May 22 11:01:59 2010 +0200 @@ -6,7 +6,7 @@ header{*Merge Sort*} theory MergeSort -imports Sorting +imports Multiset begin context linorder @@ -19,23 +19,17 @@ | "merge xs [] = xs" | "merge [] ys = ys" -lemma multiset_of_merge[simp]: - "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" -apply(induct xs ys rule: merge.induct) -apply (auto simp: union_ac) -done +lemma multiset_of_merge [simp]: + "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" + by (induct xs ys rule: merge.induct) (simp_all add: ac_simps) -lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys" -apply(induct xs ys rule: merge.induct) -apply auto -done +lemma set_merge [simp]: + "set (merge xs ys) = set xs \<union> set ys" + by (induct xs ys rule: merge.induct) auto -lemma sorted_merge[simp]: - "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)" -apply(induct xs ys rule: merge.induct) -apply(simp_all add: ball_Un not_le less_le) -apply(blast intro: order_trans) -done +lemma sorted_merge [simp]: + "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys" + by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons) fun msort :: "'a list \<Rightarrow> 'a list" where @@ -44,16 +38,19 @@ | "msort xs = merge (msort (take (size xs div 2) xs)) (msort (drop (size xs div 2) xs))" -theorem sorted_msort: "sorted (op \<le>) (msort xs)" -by (induct xs rule: msort.induct) simp_all +lemma sorted_msort: + "sorted (msort xs)" + by (induct xs rule: msort.induct) simp_all -theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs" -apply (induct xs rule: msort.induct) - apply simp_all -apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons) -done +lemma multiset_of_msort: + "multiset_of (msort xs) = multiset_of xs" + by (induct xs rule: msort.induct) + (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons) + +theorem msort_sort: + "sort = msort" + by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+ end - end