section \<open>Solutions for Session 7\<close>

theory Solutions07
  imports Demo07
begin

subsection \<open>Exercise 1\<close>

text \<open>
Prove that @{const qsort} produces sorted lists.
\<close>

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 \<open>Exercise 2\<close>

text \<open>
Implement a single recursive function \<open>unstutter\<close> that eliminates consecutive copies from a given
list. For example:

  \<open>unstutter [1,1,2,1,3,3,2] = [1,2,1,3,2]\<close>
\<close>
fun unstutter :: "'a list \<Rightarrow> 'a list"
  where
    "unstutter (x # y # ys) = (if x = y then unstutter (y # ys) else x # unstutter (y # ys))"
  | "unstutter xs = xs"

text \<open>
Given the function \<open>group'\<close> below. Prove that @{const unstutter} can be implemented
using only @{const map}, @{const hd}, and \<open>group'\<close>.
\<close>
fun group' :: "'a list \<Rightarrow> 'a list list"
  where
    "group' (x # y # ys) =
      (if x = y then case group' (y # ys) of u # us \<Rightarrow> (x # u) # us
      else [x] # group' (y # ys))"
  | "group' [x] = [[x]]"
  | "group' [] = []"

fun split_same :: "'a \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> '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 \<open>Exercise 3\<close>

text \<open>
Implement a function \<open>c_qsort\<close> that, given a list \<open>xs\<close>, computes the number of comparisons
performed when @{const qsort} is applied to \<open>xs\<close>.

Hint: The collection of facts @{thm algebra_simps} might be useful.
\<close>

fun c_qsort :: "nat list \<Rightarrow> nat"
  where
    "c_qsort [] = 0"
  | "c_qsort (x # xs) = 2 * length xs + c_qsort (filter ((>) x) xs) + c_qsort (filter ((\<le>) x) xs)"

text \<open>
Prove that the number of comparisons performed by @{const qsort} is quadratic in the
length of the input list.
\<close>

lemma c_qsort: "c_qsort xs \<le> (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 ((\<le>) x) xs)"
    by (induction xs) (auto)
  then show ?case
    using IH
    by (auto simp: power2_eq_square algebra_simps)
qed simp


subsection \<open>Exercise 4\<close>

text \<open>
Implement a function \<open>t_qsort\<close> that, given a list \<open>xs\<close>, computes the number of recursive calls
performed when @{const qsort} is applied to \<open>xs\<close>.
\<close>

fun t_qsort :: "nat list \<Rightarrow> nat"
  where
    "t_qsort [] = 0"
  | "t_qsort (x # xs) = 2 + t_qsort (filter ((>) x) xs) + t_qsort (filter ((\<le>) x) xs)"

text \<open>
Prove that @{const t_qsort} is quadratic in the length of its input.
\<close>

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 ((\<le>) x) xs)"
    by (induction xs) auto
  then show ?case
    using IH
    by (auto simp: power2_eq_square algebra_simps)
qed simp

end