section \Solutions for Session 7\ theory Solutions07 imports Demo07 begin subsection \Exercise 1\ text \ Prove that @{const qsort} produces sorted lists. \ lemma set_qsort [simp]: "set (qsort xs) = set xs" by (metis mset_qsort set_mset_mset) lemma sorted_qsort: "sorted (qsort xs)" by (induction xs rule: qsort.induct) (auto simp: sorted_append) subsection \Exercise 2\ text \ Implement a single recursive function \unstutter\ that eliminates consecutive copies from a given list. For example: \unstutter [1,1,2,1,3,3,2] = [1,2,1,3,2]\ \ fun unstutter :: "'a list \ 'a list" where "unstutter (x # y # ys) = (if x = y then unstutter (y # ys) else x # unstutter (y # ys))" | "unstutter xs = xs" text \ Given the function \group'\ below. Prove that @{const unstutter} can be implemented using only @{const map}, @{const hd}, and \group'\. \ fun group' :: "'a list \ 'a list list" where "group' (x # y # ys) = (if x = y then case group' (y # ys) of u # us \ (x # u) # us else [x] # group' (y # ys))" | "group' [x] = [[x]]" | "group' [] = []" fun split_same :: "'a \ 'a list \ ('a list \ 'a list)" where "split_same x [] = ([], [])" | "split_same x (y # ys) = (if x = y then let (us, vs) = split_same x ys in (y # us, vs) else ([], y # ys))" lemma group'_Cons: "group' (x # xs) = (let (ys, zs) = split_same x xs in (x # ys) # group' zs)" by (induction xs) (auto split: prod.splits) lemma "unstutter xs = map hd (group' xs)" by (induction xs rule: unstutter.induct) (auto split: list.splits prod.splits simp: group'_Cons) subsection \Exercise 3\ text \ Implement a function \c_qsort\ that, given a list \xs\, computes the number of comparisons performed when @{const qsort} is applied to \xs\. Hint: The collection of facts @{thm algebra_simps} might be useful. \ fun c_qsort :: "nat list \ nat" where "c_qsort [] = 0" | "c_qsort (x # xs) = 2 * length xs + c_qsort (filter ((>) x) xs) + c_qsort (filter ((\) x) xs)" text \ Prove that the number of comparisons performed by @{const qsort} is quadratic in the length of the input list. \ lemma c_qsort: "c_qsort xs \ (length xs)\<^sup>2" proof (induction xs rule: c_qsort.induct) case IH: (2 x xs) have "length xs = length (filter ((>) x) xs) + length (filter ((\) x) xs)" by (induction xs) (auto) then show ?case using IH by (auto simp: power2_eq_square algebra_simps) qed simp subsection \Exercise 4\ text \ Implement a function \t_qsort\ that, given a list \xs\, computes the number of recursive calls performed when @{const qsort} is applied to \xs\. \ fun t_qsort :: "nat list \ nat" where "t_qsort [] = 0" | "t_qsort (x # xs) = 2 + t_qsort (filter ((>) x) xs) + t_qsort (filter ((\) x) xs)" text \ Prove that @{const t_qsort} is quadratic in the length of its input. \ lemma t_qsort: "t_qsort xs < (length xs + 1)\<^sup>2" proof (induction xs rule: t_qsort.induct) case IH: (2 x xs) have "length xs = length (filter ((>) x) xs) + length (filter ((\) x) xs)" by (induction xs) auto then show ?case using IH by (auto simp: power2_eq_square algebra_simps) qed simp end