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..*)