(*
As with the previous exercise, feel free to delete or extend the markup as you prefer.
*)

section \<open>Power, Sum\<close>

(*<*) theory powSum_ex imports Main begin (*>*)

subsection \<open>Power\<close>

text \<open>Define a primitive recursive function $pow~x~n$ that
computes $x^n$ on natural numbers.\<close>

consts
  pow :: "nat => nat => nat"


text \<open>Prove the well known equation $x^{m \cdot n} = (x^m)^n$:\<close>

theorem pow_mult: "pow x (m * n) = pow (pow x m) n"
(*<*) oops (*>*)

text \<open>Hint: prove a suitable lemma first.  If you need to appeal to
associativity and commutativity of multiplication: the corresponding
simplification rules are named @{text mult_ac}.\<close>


subsection \<open>Summation\<close>

(*<*)hide_const sum Sum(*>*)

text \<open>Define a (primitive recursive) function $sum~ns$ that sums a list
of natural numbers: $sum [n_1, \dots, n_k] = n_1 + \cdots + n_k$.\<close>

consts
  sum :: "nat list => nat"

text \<open>Show that $sum$ is compatible with $rev$. You may need a lemma.\<close>

theorem sum_rev: "sum (rev ns) = sum ns"
(*<*) oops (*>*)


text \<open>Define a function $Sum~f~k$ that sums $f$ from $0$ up to $k-1$:
$Sum~f~k = f~0 + \cdots + f(k - 1)$.\<close>

consts
  Sum :: "(nat => nat) => nat => nat"


text \<open>Show the following equations for the pointwise summation of functions.
Determine first what the expression @{text whatever} should be.\<close>

theorem "Sum (%i. f i + g i) k = Sum f k + Sum g k"
(*<*) oops (*>*)

theorem "Sum f (k + l) = Sum f k + Sum whatever l"
(*<*) oops (*>*)


text \<open>What is the relationship between @{term sum} and @{text Sum}?
Prove the following equation, suitably instantiated.\<close>

theorem "Sum f k = sum whatever"
(*<*) oops (*>*)

text \<open>Hint: familiarize yourself with the predefined functions @{term map}
and @{text"[i..<j]"} on lists in theory List.\<close>


text \<open>
\newpage\<close>


(*<*) end (*>*)
