Isabelle/Isar（その９）
前回の内容を入力し終わると，Outputは
proof (prove): step 0 goal (1 subgoal): 1. a n = 2 ^ n - 1
となり，証明待ちモードに入ったことが判ります．
ここからいよいよ証明です．最初の
proof (induction n)
はshowsで指定した結論を自由変数nについての数学的帰納法の結論とするようなmethodを用いるということで，入力後のOutputは
proof (state): step 1
goal (2 subgoals):
1. a 0 = 2 ^ 0 - 1
2. ⋀n. a n = 2 ^ n - 1 ⟹ a (Suc n) = 2 ^ Suc n - 1
となり２つのサブゴールが出来たことが判ります．proofコマンドはこのように証明の最初に適用するmethodを指定するもので，引数を略すると，結論の形に応じたmethodが適用されます．例えば
lemma shows "A <-> B" proof
に対するOutputは
proof (state): step 1
goal (2 subgoals):
1. A ⟹ B
2. B ⟹ A
となります．なお，何もして欲しくない場合には
lemma shows "A <-> B" proof -
のように「何もしない」methodを指定すれば
proof (state): step 1
goal (1 subgoal):
1. A = B
のままです．また，システムが適当なmethodを見つけられない場合にはエラーになりますので，そのときも proof - としておきます．
上のOutputにある通り，proofコマンドの実行が完了すると「次に証明したい事柄を書いてください」状態，すなわち，proof (state)モードに入ります．
