Isabelle/Isar（その16）

　では帰納法の２つ目のサブゴールの証明部分を解説しましょう．

　まず，１つ目の証明から２つ目に移ることをシステムに告げているのが

next

です．するとIsarは

proof (state): step 14

goal (1 subgoal):
1. ⋀nat. a nat = 2 ^ nat - 1 ⟹ a (Suc nat) = 2 ^ Suc nat - 1

のようにメタレベルの表示で答えますので，これに対応するstatementをfix，assume，showを用いて入力します．

　まず，⋀nat. に対するのが

fix n

です（natというのはシステムが設けた束縛変数なので，入力時はnで構いません）．次のa nat = 2 ^ nat - 1に対するのが

assume "a n = 2 ^ n - 1"

であり，nや1のタイプを明示しなくて良いのは，aがnatからrealへの写像と固定しているからです．これで「任意に固定した自然数nについて，a n = 2 ^ n - 1と仮定すると」という帰納法のお約束が出来ました．

　後はa (Suc n) = 2 ^ (Suc n) - 1をshowするだけなのですが，いきなりでは寂しいので，ステップを設け，結果をalso-finallyで結んでいます．

　まず今仮定したthisとassmsの２つ目を

from this and 2

のように参照して，a (Suc n) を n で表わすことを目標にしているのが

have "a (Suc n) = 2 * (2 ^ n - 1) + 1"

です．証明はただ代入だけなので

proof simp
qed

勿論

by simp

でOKです．

　そしてこの結果をcalculationとして記憶させているのが

also

で，その右辺がSuc nの形になることを次の目標にしているのが

have "... = 2 ^ (Suc n) - 1"

です．これも簡単な計算なので上と同じくsimpで処理できます．

　これで帰納法の結論の形になりましたのでfinallyでcalculationをthisにして参照させれば

show "a (Suc n) = 2 ^ (Suc n) - 1"

というstatementが可能となり，そのままなので

proof this
qed

もしくは

by this

その省略形である

.

で，２つ目サブゴールが

show a (Suc n) = 2 ^ Suc n - 1
Successful attempt to solve goal by exported rule:
(a ?na2 = 2 ^ ?na2 - 1) ⟹ a (Suc ?na2) = 2 ^ Suc ?na2 - 1
proof (state): step 27

this:
a (Suc n) = 2 ^ Suc n - 1

goal:
No subgoals!

のようになくなります．

　最後に，一番外のproofに対するqedを入力，証明が完成します．