(*<*)
theory Solution
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


text {* Standard grammar: *}

inductive_set S :: "alpha list set"
  where
    S1: "[] \<in> S"
  | S2: "w \<in> S \<Longrightarrow> [A] @ w @ [B] \<in> S"
  | S3: "v \<in> S \<Longrightarrow> w \<in> S \<Longrightarrow> v @ w \<in> S"


text {* Nonstandard grammar: *}

inductive_set T :: "alpha list set"
  where
    T1: "[] \<in> T"
  | T23: "v \<in> T \<Longrightarrow> w \<in> T \<Longrightarrow> v @ ([A] @ w @ [B]) \<in> T"


text {* Equivalence proof *}

lemma T_in_S: "w \<in> T \<Longrightarrow> w \<in> S"
proof (induct set: T)
  case T1
  show "[] \<in> S" by (rule S1)
next
  case (T23 v w)
  have "v \<in> S" .
  moreover
  {
    have "w \<in> S" .
    then have "[A] @ w @ [B] \<in> S" by (rule S2)
  }
  ultimately
  show "v @ ([A] @ w @ [B]) \<in> S" by (rule S3)
qed

lemma T2: "w \<in> T \<Longrightarrow> [A] @ w @ [B] \<in> T"
proof -
  have "[] \<in> T" by (rule T1)
  moreover assume "w \<in> T"
  ultimately have "[] @ ([A] @ w @ [B]) \<in> T" by (rule T23)
  then show ?thesis by simp
qed

lemma T3:
  assumes u: "u \<in> T"
    and v: "v \<in> T"
  shows "u @ v \<in> T"
  using v
proof induct
  case T1
  from u show "u @ [] \<in> T" by simp
next
  case (T23 v w)
  have "u @ v \<in> T" .
  moreover have "w \<in> T" .
  ultimately have "(u @ v) @ ([A] @ w @ [B]) \<in> T" by (rule T.T23)
  then show "u @ (v @ [A] @ w @ [B]) \<in> T" by simp
qed

lemma S_in_T: "w \<in> S \<Longrightarrow> w \<in> T"
proof (induct set: S)
  case S1
  show "[] \<in> T" by (rule T1)
next
  case (S2 w)
  have "w \<in> T" .
  then show "[A] @ w @ [B] \<in> T" by (rule T2)
next
  case (S3 v w)
  have "v \<in> T" and "w \<in> T" .
  then show "v @ w \<in> T" by (rule T3)
qed

theorem "S = T"
  using S_in_T T_in_S by blast


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 -- {* solution *}
  fixes n :: nat
  shows "2 * (\<Sum>i=0..n. i) = n * (n + 1)"
proof (induct n)
  case 0
  have "2 * (\<Sum>i=0..0. i) = (0::nat)" by simp
  also have "(0::nat) = 0 * (0 + 1)" by simp
  finally show ?case .
next
  case (Suc n)
  have "2 * (\<Sum>i=0..Suc n. i) = 2 * (\<Sum>i=0..n. i) + 2 * (n + 1)" by simp
  also have "2 * (\<Sum>i=0..n. i) = n * (n + 1)" by (rule Suc.hyps)
  also have "n * (n + 1) + 2 * (n + 1) = Suc n * (Suc n + 1)" by simp
  finally show ?case .
qed

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 -- {* solution *}
  fixes n :: nat
  shows "(\<Sum>i=0..<n. 2 * i + 1) = n\<twosuperior>"
proof (induct n)
  case 0
  have "(\<Sum>i=0..<0. 2 * i + 1) = (0::nat)" by simp
  also have "(0::nat) = 0\<twosuperior>" by simp
  finally show ?case .
next
  case (Suc n)
  have "(\<Sum>i=0..<Suc n. 2 * i + 1) = (\<Sum>i=0..<n. 2 * i + 1) + 2 * n + 1"
    by simp
  also have "(\<Sum>i=0..<n. 2 * i + 1) = n\<twosuperior>"
    by (rule Suc.hyps)
  also have "n^2 + 2 * n + 1 = (Suc n)\<twosuperior>"
    by (simp add: power_eq_if nat_distrib)
  finally show ?case .
qed

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 -- {* solution *}
  fixes n :: nat
  shows "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
proof (induct n)
  case 0
  have "(\<Sum>i=0..<0. 2^i) = (0::nat)" by simp
  also have "(0::nat) = 2^0 - (1::nat)" by simp
  finally show ?case .
next
  case (Suc n)
  have "(\<Sum>i=0..<Suc n. 2^i) = (\<Sum>i=0..<n. 2^i) + 2^n"
    by simp
  also have "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
    by (rule Suc.hyps)
  also have "(2^n - (1::nat)) + 2^n = 2^(Suc n) - (1::nat)"
    by (simp split: nat_diff_split)
  finally show ?case .
qed

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 -- {* solution *}
  fixes n :: nat
  shows "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
proof (induct n)
  case 0
  have "2 * (\<Sum>i=0..<0. 3^i) = (0::nat)" by simp
  also have "(0::nat) = 3^0 - (1::nat)" by simp
  finally show ?case .
next
  case (Suc n)
  have "(2::nat) * (\<Sum>i=0..<Suc n. 3^i) = 2 * (\<Sum>i=0..<n. 3^i) + 2 * 3^n"
    by (simp add: nat_distrib)
  also have "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
    by (rule Suc.hyps)
  also have "(3^n - 1) + 2 * 3^n = 3^(Suc n) - (1::nat)"
    by simp
  finally show ?case .
qed

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)

theorem -- {* solution *}
  fixes n :: nat
  assumes k: "0 < k"
  shows "(k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
proof (induct n)
  case 0
  have "(k - 1) * (\<Sum>i=0..<0. k^i) = (0::nat)" by simp
  also have "(0::nat) = k^0 - (1::nat)" by simp
  finally show ?case .
next
  case (Suc n)
  have "(k - 1) * (\<Sum>i=0..<Suc n. k^i) =
      (k - 1) * (\<Sum>i=0..<n. k^i) + (k - 1) * k^n"
    using k by (simp add: nat_distrib)
  also have "(k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
    by (rule Suc.hyps)
  also have "(k^n - 1) + (k - 1) * k^n = k^(Suc n) - (1::nat)"
    using k by (simp add: nat_distrib)
  finally show ?case .
qed

(*<*)
end
(*>*)