Isabelle/Isar（その８）

　では，くどく解説していきます．まず

lemma kudoi:
  fixes a :: "nat => real" and n :: "nat"
  assumes 1: "a 0 = 0" and 2: "ALL n. a (Suc n) = 2 * a n + 1"
  shows "a n = 2 ^ n - 1"

がコマンドlemmaとその引数です（ttyインターフェイスではここで改行できます）．kudoi:はこの補題の名前，fixesは証明内で固定される対象とそのタイプ，assumesは仮定，showsは結論を指定しています．詳しく見ていくと．．．

　fixesに続く，a :: "nat => real" は，a が自然数全体の集合natから実数全体realの集合への写像であることを表し，n :: "nat" は n が自然数であることを表しています．項目が複数あるときはandで結びます．なお，aとnは本来は "a"と"n"と書くべきところ，一文字なので""が略せるというお約束を用いています．このfixesおよびproofで用いるfixは，Isabelle（メタロジック）レベルでの全称量化記号!!に対応しており，証明の外から見ればa,nは任意，証明内では固定されたもので，証明が完了すると量化が解かれ，代入やパターンマッチングが可能な自由変数（Isabelleでいうスキーマティック変数）になります．

　assumesに続く，1: "a 0 = 0" and 2: "ALL n. a (Suc n) = 2 * a n + 1"は，1，2という名前の論理式を仮定とするということです．仮定が複数あるときはandで結びます．Isabelleレベルでの"[|a 0 = 0; ALL n. a (Suc n) = 2 * a n + 1|]" あるいは "a 0 = 0 ==> (ALL n. a (Suc n) = 2 * a n + 1) (==>)" に対応していますが，名指しで参照できる点，および，証明途中のOutputには表示されない点などが特徴です．なお，assumesの第k項目はassms(k)で参照でき，多数あれば，assms(1,2,4-6,9)といった書式も使えます．

　showsに続く，"a n = 2 ^ n - 1" が結論です．この論理式は証明中は "?thesis" として参照できます．また，今回のように自由変数を含むなら "a n = 2 ^ n - 1" ( is "?P n") とすれば，例えば，"a 0 = 2 ^ 0 - 1" は "?P 0" で，"a (Suc n) = 2 ^ (Suc n) - 1" は "?P (Suc n)" で代替できます．