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