theory Exercise06
imports Main
begin

subsection {* Polynomial sums *}

text {*
  \note{Produce structured proofs of the following theorems, using
  induction and calculational reasoning in Isar.}

  Note that existing tactic scripts are of limited use in
  reconstructing structured proofs; nevertheless the lemmas used in
  automated steps below can be re-used to finish sub-problems.
  The @{text "\<Sum>"} symbol can be entered as ``\verb,\<Sum>,''; recall that
  numerals in Isabelle/HOL are polymorphic.
*}

theorem
  fixes n :: nat
  shows "2 * (\<Sum>i=0..n. i) = n * (n + 1)"
  by (induct n) simp_all

theorem
  fixes n :: nat
  shows "(\<Sum>i=0..<n. 2 * i + 1) = n\<twosuperior>"
  by (induct n) (simp_all add: power_eq_if nat_distrib)

theorem
  fixes n :: nat
  shows "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
  by (induct n) (simp_all split: nat_diff_split)

theorem
  fixes n :: nat
  shows "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
  by (induct n) (simp_all add: nat_distrib)

theorem
  fixes n :: nat
  assumes k: "0 < k"
  shows "(k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
  by (induct n) (insert k, simp_all add: nat_distrib)

text {*
  \medskip \note{Try explicit statements vs.\ term abbreviations:
  implicit ``@{text "\<dots>"}'', @{text "?case"}, @{text "?thesis"}.}

  \note{Try explicit @{text "\<FIX>/\<ASSUME>"} vs.\ implicit @{text
  "\<CASE>"} abbreviations.}

  \note{Which facts are relevant to solve local problems
  automatically?}
*}

end