(*<*) theory sol06 imports Complex_Main "~~/src/HOL/Library/Multiset" begin (* From Sorting.thy *) hide_const List.sorted List.insort List.insort_key fun sorted :: "'a::linorder list \ bool" where "sorted [] = True" | "sorted (x # xs) = ((\y\set xs. x \ y) & sorted xs)" lemma sorted_append: "sorted (xs@ys) = (sorted xs & sorted ys & (\x \ set xs. \y \ set ys. x\y))" by (induct xs) (auto) (*>*) text {* \ExerciseSheet{6}{2.~6.~2017} *} text \\Exercise{Selection Sort} Selection sort (also known as MinSort) sorts a list by repeatedly moving the smallest element of the remaining list to the front. \ text \ Define a function that takes a non-empty list, and returns the minimum element and the list with the minimum element removed \ fun find_min :: "'a::linorder list \ 'a \ 'a list" (*<*) where "find_min [x] = (x,[])" | "find_min (x#xs) = ( let (y,ys) = find_min xs in if (x*) text \Show that \find_min\ returns the minimum element\ lemma find_min_min: assumes "find_min xs = (y,ys)" assumes "xs\[]" shows "a\set xs \ y \ a" (*<*) using assms apply (induction xs arbitrary: y ys rule: find_min.induct) apply (auto split: prod.splits if_splits) apply force+ done (*>*) text \Show that \find_min\ returns exactly the elements from the list\ lemma find_min_mset: assumes "find_min xs = (y,ys)" assumes "xs\[]" shows "mset xs = add_mset y (mset ys)" (*<*) using assms apply (induction xs arbitrary: y ys rule: find_min.induct) apply (auto split: prod.splits if_splits) done (*>*) (*<*) lemma find_min_set: "find_min xs = (y,ys) \ xs\[] \ set xs = insert y (set ys)" by (metis find_min_mset set_mset_add_mset_insert set_mset_mset) lemma find_min_min': "find_min xs = (y,ys) \ xs\[] \ a\set ys \ y \ a" by (simp add: find_min_min find_min_set) (*>*) text \Show the following lemma on the length of the returned list, and register it as \[dest]\. The function package will require this to show termination of the selection sort function\ lemma find_min_snd_len_decr[dest]: assumes "(y,ys) = find_min (x#xs)" shows "length ys < length (x#xs)" (*<*) using assms[symmetric] apply (induction xs arbitrary: x y ys) apply (auto split: prod.splits if_splits) done (*>*) text \Selection sort can now be written as follows:\ fun sel_sort where "sel_sort [] = []" | "sel_sort xs = (let (y,ys) = find_min xs in y#sel_sort ys)" text \Show that selection sort is a sorting algorithm:\ lemma sel_sort_mset[simp]: "mset (sel_sort xs) = mset xs" (*<*) apply (induction xs rule: sel_sort.induct) apply (auto split: prod.split dest: find_min_mset) done (*>*) (*<*) lemma sel_sort_set[simp]: "set (sel_sort xs) = set xs" by (metis sel_sort_mset set_mset_mset) (*>*) lemma "sorted (sel_sort xs)" (*<*) apply (induction xs rule: sel_sort.induct) apply (auto split: prod.split dest: find_min_min') done (*>*) text \Define cost functions for the number of comparisons of \find_min\ and \sel_sort\. \ fun c_find_min :: "'a list \ nat" (*<*) where "c_find_min [_] = 0" | "c_find_min (x#xs) = c_find_min xs + 1" (*>*) fun c_sel_sort (*<*) where "c_sel_sort [] = 0" | "c_sel_sort xs = (let (y,ys) = find_min xs in c_find_min xs + c_sel_sort ys)" (*>*) (*<*) lemma c_find_min_est: "xs\[] \ c_find_min xs = length xs - 1" apply (induction xs rule: c_find_min.induct) by auto lemma find_min_len_aux: "find_min (x#xs) = (y, ys) \ length xs = length ys" apply (induction xs arbitrary: x y ys) apply (auto split: prod.splits if_splits) done (*>*) (* Recurrence equation: C(0) = 0; C(k+1) = C(k) + k Solving: Educated guess: Must be order-2 polynomial c\<^sub>1k\<^sup>2 + c\<^sub>2k + c\<^sub>3 C(0) = 1 \ c\<^sub>3=1 from C(k+1) = \, we get the other factors c\<^sub>1 = 1/2 and c\<^sub>2 = -1/2 *) text \Try to find a closed formula for \c_sel_sort\! If you do not succeed, try to find a good estimate. (Hint: Should be \O(n\<^sup>2)\) To find a closed formula: On paper: \<^item> Put up a recurrence equation (depending only on the length of the list) \<^item> Solve the equation (Assume that the solution is an order-2 polynomial) In Isabelle: \<^item> Insert the solution into the lemma below, and try to prove it \ lemma c_sel_sort_cmpx: "c_sel_sort xs = undefined" oops (*<*) lemma c_sel_sort_cmpx: "c_sel_sort xs = ((length xs)\<^sup>2 - length xs ) / 2" proof (induction xs rule: c_sel_sort.induct) case 1 then show ?case by auto next case (2 x xs) obtain y ys where FM: "find_min (x # xs) = (y, ys)" by (cases "find_min (x # xs)") have [simp]: "a\<^sup>2 \ a" for a :: nat by (auto simp: eval_nat_numeral) have [simp]: "a\b \ real (a - b) = real a - real b" for a b :: nat by auto have "c_sel_sort (x # xs) = length xs + c_sel_sort ys" by (simp split: prod.split add: FM c_find_min_est) also from "2.IH"[OF refl] FM have "\ = length xs + ((length ys)\<^sup>2 - length ys) / 2" by auto also from find_min_len_aux[OF FM] have "\ = length xs + ((length xs)\<^sup>2 - length xs) / 2" by auto also have "\ = (length xs + (length xs)\<^sup>2)/2" by (auto simp: field_simps) also have "\ = ((length (x # xs))\<^sup>2 - length (x # xs)) / 2" by (auto simp: eval_nat_numeral) finally show ?case . qed (*>*) (*<*) (* Alternative solution: Explicit recurrence equation! *) fun c_sel_sort' where "c_sel_sort' 0 = 0" | "c_sel_sort' (Suc n) = (n + c_sel_sort' n)" lemma "c_sel_sort xs = c_sel_sort' (length xs)" apply (induction xs rule: c_sel_sort.induct) apply (auto split: prod.split simp: find_min_len_aux c_find_min_est) done lemma c_sel_sort_cmpx': "c_sel_sort' n = (n\<^sup>2 - n) / 2" apply (induction n) apply (auto simp: eval_nat_numeral field_simps) done (*>*) (*<*) end (*>*)