section \Solutions for Session 2\
theory Solutions02
imports Main
begin
declare [[names_short]]
subsection \Exercise 1\
text \
Define a recursive function \pow x n\ that computes \x\<^sup>n\ on natural numbers.
\
fun pow :: "nat \ nat \ nat"
where
"pow x 0 = 1"
| "pow x (Suc n) = x * pow x n"
text \
Prove the well-known equation \x\<^sup>m\<^sup>\\<^sup>n = (x\<^sup>m)\<^sup>n\.
Hint: Prove suitable auxiliary results as required. If you need to appeal
to associativity and commutativity of multiplication use @{thm mult_ac}.
\
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 \Exercise 2\
text \
Define a recursive function \sum ns\ that sums a list of natural numbers:
\sum [n\<^sub>1, \, n\<^sub>k] = n\<^sub>1 + \ + n\<^sub>k\.
\
fun sum :: "nat list \ nat"
where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"
text \
Show that @{const sum} is compatible with @{const rev}.
(You will need an auxiliary result.)
\
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 \Exercise 3\
text \
Define a recursive function \Sum f k\ that sums \f\ from \0\ up to \k - 1\:
\Sum f k = f 0 + \ + f (k - 1)\
\
fun Sum :: "(nat \ nat) \ nat \ nat"
where
"Sum f 0 = 0"
| "Sum f (Suc k) = Sum f k + f k"
text \
Show the following equations for the pointwise summation of functions.
\
lemma Sum_add_pointwise: "Sum (\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 (\i. f (k + i)) l"
by (induction l) auto
subsection \Exercise 4\
text \
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 \[i..) on lists
in @{theory HOL.List}.
\
lemma Sum_sum_conv: "Sum f k = sum (map f [0..