header {* Power, Sum *}
(*<*)theory Exercises2 imports Main begin(*>*)
subsubsection {* Power *}
text {*
$\rhd$ Define a (primitive recursive) function @{term "pow x n"} that
computes $x^n$ on natural numbers.
*}
(*<*)consts(*>*) pow :: "nat \ nat \ nat"
text {*
$\rhd$ Prove the well known equation $x^{m \cdot n} = (x^m)^n$:
*}
theorem pow_mult: "pow x (m * n) = pow (pow x m) n"
(*<*)oops(*>*)
text {*
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}.
*}
subsubsection {* Summation *}
(*<*)hide_const sum(*>*)
text {*
$\rhd$ Define a (primitive recursive) function @{term "sum ns"} that
sums a list of natural numbers: $\mathit{sum}\ [n_1, \dots, n_k] = n_1
+ \cdots + n_k$.
*}
(*<*)consts(*>*) sum :: "nat list \ nat"
text {*
$\rhd$ Show that @{term sum} is compatible with @{term rev}. You may
need a lemma.
*}
theorem sum_rev: "sum (rev ns) = sum ns"
(*<*)oops(*>*)
text {*
$\rhd$ Define a function @{term "Sum f k"} that sums $f$ from $0$ up
to $k-1$: $\mathit{Sum}~f~k = f~0 + \cdots + f(k - 1)$.
*}
(*<*)consts(*>*) Sum :: "(nat \ nat) \ nat \ nat"
text {*
$\rhd$ Show the following equations for the pointwise summation of
functions. Determine first what the expression @{text whatever}
should be.
*}
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 {*
$\rhd$ What is the relationship between @{term sum} and @{term Sum}?
Prove the following equation, suitably instantiated.
*}
theorem "Sum f k = sum whatever"
(*<*)oops(*>*)
text {*
Hint: familiarize yourself with the predefined functions @{term map}
and @{term "[i..*)