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

theory Solutions02
  imports Main
begin

declare [[names_short]]

subsection \<open>Exercise 1\<close>

text \<open>
Define a recursive function \<open>pow x n\<close> that computes \<open>x\<^sup>n\<close> on natural numbers.
\<close>
fun pow :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  where
    "pow x 0 = 1"
  | "pow x (Suc n) = x * pow x n"

text \<open>
Prove the well-known equation \<open>x\<^sup>m\<^sup>\<cdot>\<^sup>n = (x\<^sup>m)\<^sup>n\<close>.

Hint: Prove suitable auxiliary results as required. If you need to appeal
to associativity and commutativity of multiplication use @{thm mult_ac}.
\<close>
lemma pow_1: "pow (Suc 0) m = Suc 0"
  by (induction m) auto

lemma pow_add: "pow x (m + n) = pow x m * pow x n"
  by (induction m) (auto)

lemma pow_mult_distrib: "pow (x * y) m = pow x m * pow y m"
  by (induction m) auto

lemma pow_mult: "pow x (m * n) = pow (pow x m) n"
  by (induction m) (auto simp: pow_1 pow_add pow_mult_distrib)


subsection \<open>Exercise 2\<close>

text \<open>
Define a recursive function \<open>sum ns\<close> that sums a list of natural numbers:

  \<open>sum [n\<^sub>1, \<dots>, n\<^sub>k] = n\<^sub>1 + \<cdots> + n\<^sub>k\<close>.
\<close>
fun sum :: "nat list \<Rightarrow> nat"
  where
    "sum [] = 0"
  | "sum (x#xs) = x + sum xs"

text \<open>
Show that @{const sum} is compatible with @{const rev}.
(You will need an auxiliary result.)
\<close>
lemma sum_append: "sum (xs @ ys) = sum xs + sum ys"
  by (induction xs) auto

lemma sum_rev: "sum (rev ns) = sum ns"
  by (induction ns) (auto simp: sum_append)


subsection \<open>Exercise 3\<close>

text \<open>
Define a recursive function \<open>Sum f k\<close> that sums \<open>f\<close> from \<open>0\<close> up to \<open>k - 1\<close>:

  \<open>Sum f k = f 0 + \<cdots> + f (k - 1)\<close>
\<close>
fun Sum :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
  where
    "Sum f 0 = 0"
  | "Sum f (Suc k) = Sum f k + f k"

text \<open>
Show the following equations for the pointwise summation of functions.
\<close>
lemma Sum_add_pointwise: "Sum (\<lambda>i. f i + g i) k = Sum f k + Sum g k"
  by (induction k) auto

lemma Sum_add: "Sum f (k + l) = Sum f k + Sum (\<lambda>i. f (k + i)) l"
  by (induction l) auto


subsection \<open>Exercise 4\<close>

text \<open>
What is the relationship between @{const sum} and @{const Sum}?
Prove the following equation.

Hint: Familiarize yourself with the predefined functions @{const map}
and @{const upt} (with syntactic sugar \<open>[i..<j]\<close>) on lists
in @{theory HOL.List}.
\<close>

lemma Sum_sum_conv: "Sum f k = sum (map f [0..<k])"
  by (induction k) (auto simp: sum_append)

end