(*<*)
theory Exercise
imports Main
begin
(*>*)

section {* Two Grammars *}

text{*
  The most natural definition of valid sequences of parentheses is
  this: \[ S \quad\to\quad \epsilon \quad\mid\quad '('~S~')'
  \quad\mid\quad S~S \] where $\epsilon$ is the empty word.

  A second, somewhat unusual grammar is the following one: \[ T
  \quad\to\quad \epsilon \quad\mid\quad T~'('~T~')' \]
*}

text {*
  $\rhd$ Make the definitions of sets @{term S} and @{term
  T} in Isabelle and give structured Isar proofs leading to the
  theorem @{term "S = T"}.

  Hint: use lists over a specific type to repesent words.
*}

text {* The alphabet: *}

datatype alpha = A | B


section {* Polynomial sums *}

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

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

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


theorem -- {* problem *}
  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 -- {* problem *}
  fixes n :: nat
  shows "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
  by (induct n) (simp_all split: nat_diff_split)


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


theorem -- {* problem *}
  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)


(*<*)
end
(*>*)