Isabelle/Isar（その10） - ATPとCASのこと

　Isarのproofモードは，荒く言って

証明の目標の明言を要請するstateモードと，その証明の方法を要請するproveモードの対

の列であり，コマンドとしては，前者にはshow系のshowsやshow，後者にはproof系のproofやbyやapplyを用います．実際，（その８）と（その９）が最も外側の証明のstate/proveモードの対であり，（その９）の結果得られたOutputにある２つのサブゴールの１つ目を次の目標にすることをIsarに伝えているのが

show "a 0 = 2 ^ 0 - 1"

であり，入力後は

proof (prove): step 2

goal (1 subgoal):
 1. a 0 = 2 ^ 0 - 1

のようにproof (prove)すなわち，その証明待ちモードになり，内側の対が出来ます．

　そしてここでも外側と同じくproofコマンドを用いてmethodを適用するわけですが，今回は 2 ^ 0 - 1 を簡約するために simp を引数にして

proof simp

としています．これで右辺が簡約され

proof (state): step 3

goal (1 subgoal):
 1. a 0 = 0

というサブゴールに変わり，次に証明する目標を聞いてきますので，３度show-proofの対を作るべく

show "a 0 = 0"

と伝えてやると，その証明を

proof (prove): step 4

goal (1 subgoal):
 1. a 0 = 0

のように要求してきます．きりがないようですが，今回の目標は仮定の1そのものですから，次のproofコマンドは，1の結論（ここでは1自体）をサブゴールの結論（ここではサブゴール自体）とマッチングさせるmethodであるrule 1を引数にして

proof (rule 1)

としています．Outputは

proof (state): step 5

goal:
No subgoals!

なので，proof (rule 1)に対応するqedを入力すれば，最も内側の証明が完了して

show a 0 = 0 
 Successful attempt to solve goal by exported rule:
  a 0 = 0 
 proof (state): step 6

this:
  a 0 = 0

goal:
No subgoals!

さらにproof simpに対応するqedを入力すると，中間の，つまり帰納法の１つ目のサブゴールa 0 = 2 ^ 0 - 1の証明が完了して，

show a 0 = 2 ^ 0 - 1
Successful attempt to solve goal by exported rule:
a 0 = 2 ^ 0 - 1
proof (state): step 7
this:
a 0 = 2 ^ 0 - 1
goal (1 subgoal):
1. ⋀n. a n = 2 ^ n - 1 ⟹ a (Suc n) = 2 ^ Suc n - 1

のように２つ目のサブゴールが繰り上がってきたことが判ります．なお，thisというのは処理し終えた最新の事実の一時的な名前で，これをAとして同じ証明内で後に参照するには，例えば

note A = this

とします（ただ，今回のように証明の最後に記録しても参照の余地はありませんので，証明の途中で得た事実にの参照に用いるのが普通です）．