(*<*)
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
(*>*)