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

author | haftmann |

Sun, 04 Nov 2018 15:00:30 +0000 | |

changeset 69246 | c1fe9dcc274a |

parent 69245 | 3e9f812c308c |

child 69249 | 27423819534c |

concrecte sorting algorithms beyond insertion sort

src/HOL/Library/Comparator.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Sorting_Algorithms.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Comparator.thy Mon Nov 05 23:15:58 2018 +0100 +++ b/src/HOL/Library/Comparator.thy Sun Nov 04 15:00:30 2018 +0000 @@ -76,6 +76,24 @@ "asymp (\<lambda>a b. cmp a b = Greater)" using irreflp_greater by (auto intro!: asympI dest: asym_greater) +lemma trans_equiv_less: + "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less" + using that + by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) + +lemma trans_less_equiv: + "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv" + using that + by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) + +lemma trans_equiv_greater: + "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater" + using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv) + +lemma trans_greater_equiv: + "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv" + using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less) + lemma transp_less: "transp (\<lambda>a b. cmp a b = Less)" by (rule transpI) (fact trans_less) @@ -118,6 +136,26 @@ "transp (\<lambda>a b. cmp a b \<noteq> Greater)" by (rule transpI) (fact trans_not_greater) +text \<open>Substitution under equivalences\<close> + +lemma equiv_subst_left: + "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp +proof - + from that have "cmp x z = Equiv" + by (simp add: sym) + with that show ?thesis + by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater) +qed + +lemma equiv_subst_right: + "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp +proof - + from that have "cmp y z = Equiv" + by (simp add: sym) + with that show ?thesis + by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv) +qed + end typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"

--- a/src/HOL/Library/Sorting_Algorithms.thy Mon Nov 05 23:15:58 2018 +0100 +++ b/src/HOL/Library/Sorting_Algorithms.thy Sun Nov 04 15:00:30 2018 +0000 @@ -6,11 +6,6 @@ imports Main Multiset Comparator begin -text \<open>Prelude\<close> - -hide_const (open) sorted insort sort - - section \<open>Stably sorted lists\<close> abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" @@ -19,17 +14,26 @@ fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool" where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True" | sorted_single: "sorted cmp [x] \<longleftrightarrow> True" - | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp x y \<noteq> Less \<and> sorted cmp (x # xs)" + | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)" lemma sorted_ConsI: "sorted cmp (x # xs)" if "sorted cmp xs" - and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp y x \<noteq> Less" + and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater" + using that by (cases xs) simp_all + +lemma sorted_Cons_imp_sorted: + "sorted cmp xs" if "sorted cmp (x # xs)" using that by (cases xs) simp_all +lemma sorted_Cons_imp_not_less: + "compare cmp y x \<noteq> Greater" if "sorted cmp (y # xs)" + and "x \<in> set xs" + using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater) + lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]: "P xs" if "sorted cmp xs" and "P []" and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs - \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less) \<Longrightarrow> P (x # xs)" + \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)" using \<open>sorted cmp xs\<close> proof (induction xs) case Nil show ?case @@ -40,7 +44,7 @@ by (cases xs) simp_all moreover have "P xs" using \<open>sorted cmp xs\<close> by (rule Cons.IH) - moreover have "compare cmp y x \<noteq> Less" if "y \<in> set xs" for y + moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y using that \<open>sorted cmp (x # xs)\<close> proof (induction xs) case Nil then show ?case @@ -54,10 +58,10 @@ by simp next case (Cons w ws) - with Cons.prems have "compare cmp w z \<noteq> Less" "compare cmp z x \<noteq> Less" + with Cons.prems have "compare cmp z w \<noteq> Greater" "compare cmp x z \<noteq> Greater" by auto - then have "compare cmp w x \<noteq> Less" - by (auto dest: compare.trans_not_less) + then have "compare cmp x w \<noteq> Greater" + by (auto dest: compare.trans_not_greater) with Cons show ?thesis using Cons.prems Cons.IH by auto qed @@ -69,7 +73,7 @@ lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]: "P xs" if "sorted cmp xs" and "P []" and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs) - \<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less) + \<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P xs" using \<open>sorted cmp xs\<close> proof (induction xs) case Nil @@ -80,7 +84,7 @@ then have "sorted cmp (x # xs)" by (simp add: sorted_ConsI) moreover note Cons.IH - moreover have "\<And>y. compare cmp y x = Less \<Longrightarrow> y \<in> set xs \<Longrightarrow> False" + moreover have "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False" using Cons.hyps by simp ultimately show ?case by (auto intro!: * [of "x # xs" x]) blast @@ -114,7 +118,7 @@ assume "remove1 x ys = z # zs" with \<open>x \<noteq> y\<close> have "z \<in> set ys" using notin_set_remove1 [of z ys x] by auto - then show "compare cmp z y \<noteq> Less" + then show "compare cmp y z \<noteq> Greater" by (rule Cons.hyps(2)) qed with False show ?thesis @@ -123,6 +127,20 @@ qed qed +lemma sorted_stable_segment: + "sorted cmp (stable_segment cmp x xs)" +proof (induction xs) + case Nil + show ?case + by simp +next + case (Cons y ys) + then show ?case + by (auto intro!: sorted_ConsI simp add: filter_eq_Cons_iff compare.sym) + (auto dest: compare.trans_equiv simp add: compare.sym compare.greater_iff_sym_less) + +qed + primrec insort :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where "insort cmp y [] = [y]" | "insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater @@ -175,7 +193,7 @@ lemma insort_eq_ConsI: "insort cmp x xs = x # xs" - if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less" + if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater" using that by (induction xs) (simp_all add: compare.greater_iff_sym_less) lemma remove1_insort_not_same_eq [simp]: @@ -188,14 +206,15 @@ next case (Cons z zs) show ?case - proof (cases "compare cmp z x = Less") + proof (cases "compare cmp x z = Greater") case True with Cons show ?thesis - by (simp add: compare.greater_iff_sym_less) + by simp next case False - have "compare cmp y x \<noteq> Less" if "y \<in> set zs" for y - using that False Cons.hyps by (auto dest: compare.trans_not_less) + then have "compare cmp x y \<noteq> Greater" if "y \<in> set zs" for y + using that Cons.hyps + by (auto dest: compare.trans_not_greater) with Cons show ?thesis by (simp add: insort_eq_ConsI) qed @@ -211,7 +230,7 @@ next case (Cons y ys) then have "compare cmp x y \<noteq> Less" - by auto + by (auto simp add: compare.greater_iff_sym_less) then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv" by (cases "compare cmp x y") auto then show ?case proof cases @@ -227,6 +246,31 @@ qed qed +lemma sorted_append_iff: + "sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys + \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q") +proof + assume ?P + have ?R + using \<open>?P\<close> by (induction xs) + (auto simp add: sorted_Cons_imp_not_less, + auto simp add: sorted_Cons_imp_sorted intro: sorted_ConsI) + moreover have ?S + using \<open>?P\<close> by (induction xs) (auto dest: sorted_Cons_imp_sorted) + moreover have ?Q + using \<open>?P\<close> by (induction xs) (auto simp add: sorted_Cons_imp_not_less, + simp add: sorted_Cons_imp_sorted) + ultimately show "?R \<and> ?S \<and> ?Q" + by simp +next + assume "?R \<and> ?S \<and> ?Q" + then have ?R ?S ?Q + by simp_all + then show ?P + by (induction xs) + (auto simp add: append_eq_Cons_conv intro!: sorted_ConsI) +qed + definition sort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list" where "sort cmp xs = foldr (insort cmp) xs []" @@ -299,7 +343,7 @@ case (minimum x xs) from \<open>mset ys = mset xs\<close> have ys: "set ys = set xs" by (rule mset_eq_setD) - then have "compare cmp y x \<noteq> Less" if "y \<in> set ys" for y + then have "compare cmp x y \<noteq> Greater" if "y \<in> set ys" for y using that minimum.hyps by simp from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs" by simp @@ -318,4 +362,113 @@ qed qed +lemma filter_insort: + "filter P (insort cmp x xs) = insort cmp x (filter P xs)" + if "sorted cmp xs" and "P x" + using that by (induction xs) + (auto simp add: compare.trans_not_greater insort_eq_ConsI) + +lemma filter_insort_triv: + "filter P (insort cmp x xs) = filter P xs" + if "\<not> P x" + using that by (induction xs) simp_all + +lemma filter_sort: + "filter P (sort cmp xs) = sort cmp (filter P xs)" + by (induction xs) (auto simp add: filter_insort filter_insort_triv) + + +section \<open>Alternative sorting algorithms\<close> + +subsection \<open>Quicksort\<close> + +definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list" + where quicksort_is_sort [simp]: "quicksort = sort" + +lemma sort_by_quicksort: + "sort = quicksort" + by simp + +lemma sort_by_quicksort_rec: + "sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less] + @ stable_segment cmp (xs ! (length xs div 2)) xs + @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "sort cmp ?lhs = ?rhs") +proof (rule sort_eqI) + show "mset ?lhs = mset ?rhs" + by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust) +next + show "sorted cmp ?rhs" + by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater) +next + let ?pivot = "xs ! (length xs div 2)" + fix l + assume "l \<in> set xs" + have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv + \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp + proof - + have "compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp" + if "compare cmp l x = Equiv" + using that by (simp add: compare.equiv_subst_left compare.sym) + then show ?thesis by blast + qed + then show "stable_segment cmp l ?lhs = stable_segment cmp l ?rhs" + by (simp add: stable_sort compare.sym [of _ ?pivot]) + (cases "compare cmp l ?pivot", simp_all) +qed + +context +begin + +qualified definition partition :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list" + where "partition cmp pivot xs = + ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])" + +qualified lemma partition_code [code]: + "partition cmp pivot [] = ([], [], [])" + "partition cmp pivot (x # xs) = + (let (lts, eqs, gts) = partition cmp pivot xs + in case compare cmp x pivot of + Less \<Rightarrow> (x # lts, eqs, gts) + | Equiv \<Rightarrow> (lts, x # eqs, gts) + | Greater \<Rightarrow> (lts, eqs, x # gts))" + using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot]) + +lemma quicksort_code [code]: + "quicksort cmp xs = + (case xs of + [] \<Rightarrow> [] + | [x] \<Rightarrow> xs + | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x]) + | _ \<Rightarrow> + let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs + in quicksort cmp lts @ eqs @ quicksort cmp gts)" +proof (cases "length xs \<ge> 3") + case False + then have "length xs \<le> 2" + by simp + then have "length xs = 0 \<or> length xs = 1 \<or> length xs = 2" + using le_neq_trans less_2_cases by auto + then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" + by (auto simp add: length_Suc_conv numeral_2_eq_2) + then show ?thesis + by cases simp_all +next + case True + then obtain x y z zs where "xs = x # y # z # zs" + by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) + moreover have "quicksort cmp xs = + (let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs + in quicksort cmp lts @ eqs @ quicksort cmp gts)" + using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def) + ultimately show ?thesis + by simp +qed + end + +text \<open>Evaluation example\<close> + +value "let cmp = key abs (reversed default) + in quicksort cmp [65, 1705, -2322, 734, 4, (-17::int)]" + +end