header {* Power, Sum *}
(*<*)theory Solution2 imports Main begin(*>*)
subsubsection {* Power *}
text {*
$\rhd$ Define a (primitive recursive) function @{term "pow x n"} that
computes $x^n$ on natural numbers.
*}
fun pow :: "nat \ nat \ nat" where
"pow x 0 = Suc 0"
| "pow x (Suc n) = x * pow x n"
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}.
*}
lemma pow_add: "pow x (m + n) = pow x m * pow x n"
apply (induct n)
apply auto
done
theorem pow_mult: "pow x (m * n) = pow (pow x m) n"
apply (induct n)
apply (auto simp add: pow_add)
done
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$.
*}
fun sum :: "nat list \ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"
text {*
$\rhd$ Show that @{term sum} is compatible with @{term rev}. You may
need a lemma.
*}
lemma sum_append: "sum (xs @ ys) = sum xs + sum ys"
apply (induct xs)
apply auto
done
theorem sum_rev: "sum (rev ns) = sum ns"
apply (induct ns)
apply (auto simp add: sum_append)
done
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)$.
*}
fun Sum :: "(nat \ nat) \ nat \ nat" where
"Sum f 0 = 0"
| "Sum f (Suc n) = Sum f n + f n"
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"
apply (induct k)
apply auto
done
theorem "Sum f (k + l) = Sum f k + Sum (\i. f (k + i)) l"
apply (induct l)
apply auto
done
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..*)