Isabelle/Isar（その18）

　更に２つ目のサブゴールは，帰納法の変数nが1以上，つまり，Suc n_の形の場合なので，場合を設定するコマンドcase Suc を用いて簡素化出来ます．それは

lemma
  fixes "a" :: "nat => real" and "n" :: "nat"
  assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a n + 1"
  shows "a n = 2 ^ n - 1"
proof (induction n)
  show "a 0 = 2 ^ 0 - 1"
    using assms(1) by simp
next
  case Suc
  thus "?case"
    using assms(2) by simp
qed

という書式であり，case Sucは，帰納法の変数nがSuc n_の形の場合をサブゴールにするということで，これにより

  fix n_
  let ?case = "a (Suc n_) = 2 ^ Suc n_ - 1"
  assume Suc: "a n_ = 2 ^ n_ - 1"

という処理がシステム内でなされています．let ?t は見ての通り別名の設定コマンド，右辺の代わりに ?t を使えるようにするものです．また，assumeした式に Suc の名前が自動的に付くので，thusではなく，名指しで

  case Suc
  show "?case"
    using Suc assms(2) by simp

などとしても構いません．

　なお，１つ目のサブゴールの証明にも変数nが0の場合の設定case 0（具体的には，let ?case = "a 0 = 2 ^ 0 - 1"）を用いて

lemma
  fixes "a" :: "nat => real" and "n" :: "nat"
  assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a n + 1"
  shows "a n = 2 ^ n - 1"
proof (induction n)
  case 0
  show "?case"
    using assms(1) by simp
next
  case Suc
  thus "?case"
    using assms(2) by simp
qed

とすれば全体のバランスは良くなりますが，可読性という大儀が損なわれそうです．

　なお，caseコマンドの引数の0やSucは場合の名前であり，(inducton n)が参照する帰納法のルールが略されている（一般にはinduction n rule: ルール名として指定）ので，nが自然数であることより，自動的に適用されたnat_inductの属性case_nameで定められたもので，内容はprint_casesコマンドで次のように確認できます．

cases:
0:
let "?case" = "a 0 = 2 ^ 0 - 1"
Suc:
fix n_
let "?case" = "a (Suc n_) = 2 ^ Suc n_ - 1"
assume Suc.IH: "a n_ = 2 ^ n_ - 1" and Suc.prems:

ここでn_は仮の変数であり，case Suc ではなく例えばcase (Suc m)と入力すればmに置き換わり，それが任意に固定された変数となります．また，見ての通り，帰納法の仮定には，Suc.IHという名も付いているので

  case Suc
  show "?case"
    using Suc.IH assms(2) by simp

でも構いません．Suc.premsというのは，結論がP n ==> Q nの形の際に，帰納法の仮定以外に，メタの含意の前件premiseもP (Suc n_) も仮定に加えられるので，その名前です．