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 "\"} symbol can be entered as ``\verb,\,''; recall that
numerals in Isabelle/HOL are polymorphic.
*}
theorem
fixes n :: nat
shows "2 * (\i=0..n. i) = n * (n + 1)"
by (induct n) simp_all
theorem
fixes n :: nat
shows "(\i=0.."
by (induct n) (simp_all add: power_eq_if nat_distrib)
theorem
fixes n :: nat
shows "(\i=0..i=0..i=0.."}'', @{text "?case"}, @{text "?thesis"}.}
\note{Try explicit @{text "\/\"} vs.\ implicit @{text
"\"} abbreviations.}
\note{Which facts are relevant to solve local problems
automatically?}
*}
end