Isabelle/Isar（その17）

　Isarに負けないよう，くどく続けます．

　仮に以上の計算過程を省略するなら，これまでの話から，次のように書けることが判るでしょう．

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
  fix n
  assume "a n = 2 ^ n - 1"
  thus "a (Suc n) = 2 ^ Suc n - 1"
    using assms(2) by simp
qed

先に挙げたものに比べれば簡潔で，処理も統一されています．

　しかし，大きな結論の場合，show，assume，thusの後に，showsのときと同じ形の式を繰り返し入力するのはやはり面倒です．Isarではassumesで設定した仮定をassmsとして参照できるように，マッチングによりshowsで設定した結論の形を証明内で用いることが出来ます．つまり

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" (is "?P n")
proof (induction n)
  show "?P 0"
    using assms(1) by simp
next
  fix n
  assume "?P n"
  thus "?P (Suc n)"
    using assms(2) by simp
qed

のように「これを ?P n とおくと」というお約束です．設定には利用する形に応じて

  (is "?L n = ?R n")

  (is "_= ?R n")

  (is "?P n" is "?L n = ?R n")

  (is "?P")

のように様々なスタイルが使えます．