Isabelle/Isar（その12）

　つまり１つ目のサブゴールの証明は

  show "a 0 = 2 ^ 0 - 1"
  proof simp
    show "a 0 = 0"
    proof (simp add: 1)
    qed
  qed

のようにsimpのみで賄えるわけですから，内側のproofを外側に重ねられそうです．実際

  show "a 0 = 2 ^ 0 - 1"
  proof (simp add: 1)
  qed

のように内側のstatementを飛ばすことも出来，proof m1 qedはby m1とも書けましたので

  show "a 0 = 2 ^ 0 - 1"
    by (simp add: 1)

とまとめられます．