Isabelle/Isar（その３）

　例として

　a_{0}=0　かつ　任意の自然数nについてa_{n+1}=2 a_{n}+1　ならば　a_{n}=2^n-1

が定理であることの「簡潔な証明」を示します．

　そのまえに対話型の証明作成はその名の通りシステムの出力を見ながら進めるもので，Outputパネルのタブを右クリックし，フロートを選択，パネルのウインドを独立させ，全画面表示にしておきましょう．こうすればAlt+Tabでウインド間の行き来，Outputの確認も容易になります．

　では，statement，すなわち，これから証明しようとする内容を，次の通り入力してください．

lemma lem01:
  "(a::nat=>real) 0 = 0 & (ALL n. a (Suc n) = 2 * a n + 1) --> a n = 2 ^ n - 1"

　...2 ^ n - 1 までの入力中はウインド左のガターに警告マークが現れ，Outputにもエラーメッセージが出ますが，" まで入力すると，警告は消え，Outputも

proof (prove): step 0

goal (1 subgoal):
1. a 0 = 0 ∧ (∀n. a (Suc n) = 2 * a n + 1) ⟶ a n = 2 ^ n - 1

になり，proof (prove)，すなわち「証明待ちモード」に入ります．

　そこで証明の本体を次の通り入力してください．

  by (induct n, simp_all)

ここでも...simp_all) (の入力中はエラーとなりますが，)まで入力するとエラーメッセージが消え，証明が完了したことが確認できます．

　これで上記の定理はlem01としてシステムに登録されましたので，他の定理の証明で参照可能になり，証明の外いわゆるtheory modeでもthmコマンドにより表示できます．

> thm lem1;
?a 0 = 0 & (ALL n. ?a (Suc n) = 2 * ?a n + 1) --> ?a ?n = 2 ^ ?n - 1

また，この定理のstatementはprint_statementコマンドで呼び出せます．

> print_statement lem1;
theorem lem1:
  fixes a :: "nat => real" 
    and n :: "nat" 
  shows "a 0 = 0 & (ALL n. a (Suc n) = 2 * a n + 1) --> a n = 2 ^ n - 1"

これは上記の証明に先立って述べた "(a::nat=>real) 0 = 0...の省略のない形なので，これを用いて

lemma lem02:
  fixes a :: "nat => real" 
    and n :: "nat" 
  shows "a 0 = 0 & (ALL n. a (Suc n) = 2 * a n + 1) --> a n = 2 ^ n - 1";
  by (induct n,simp_all);

と入力するのが本来です（２度目の証明で名前を変えたのlem01では先のものとの衝突をさける為で，ttyではこの辺りが面倒ですが，jeditでは先の宣言部分からlem01:を消せばシステムからも名前が消えます）．