Isabelle/Isar（その14）

　このように仮定に近いサブゴールの証明はsimp任せに出来ますが，多くの場合いきなりサブゴールをshowするのは難しく，そこに至るまでの中間のサブゴールを適宜設けてそれらを証明，統合してshowとなります．

　もし今回の仮定 "a 0 = 0" からサブゴール "a 0 = 2 ^ 0 - 1" に至る中間のサブゴールを設定するなら，それは当然 "2 ^ 0 - 1 = 0" でしょう．こうした中間サブゴールのstateに用いるのがhaveコマンドです．従って１つ目のサブゴールの証明は

  have "2 ^ 0 - 1 = (0::real)"
    by simp
  from this and 1 show "a 0 = 2 ^ 0 - 1"
    by simp

のようにも出来ます．ここで注意したいのは (0::real) としてタイプを指定している点です．つまり，"2 ^ 0 - 1 = 0" としただけではそれが何についての等式なのかがIsarには判らず，サブゴールや仮定とマッチさせられない訳です．実際， have "2 ^ 0 - 1 = 0" に対するOutputは

proof (prove): step 2

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

となってしまい，by simpでもFailed to finish proofとなります．ならば，"a 0 = 2 ^ 0 - 1" にタイプの指定は要らないのか？と思われるかも知れませんが，左辺がa 0であり，冒頭のfixesでaはnatからrealへの写像としていますので，Isarはa 0のタイプはrealと知ってるわけです．

　ということで，一つ目のby simpを入力するとIsarは

have 2 ^ 0 - 1 = 0
proof (state): step 3

this:
2 ^ 0 - 1 = 0

goal (2 subgoals):
1. a 0 = 2 ^ 0 - 1
2. ⋀n. a n = 2 ^ n - 1 ⟹ a (Suc n) = 2 ^ Suc n - 1

と言って来ます．このthisは直前の処理結果の名前なので，これを仮定1をandで繋いだものをfromで参照すれば，show出来るという流れです．

　なお，参照する事実の間のandは省略でき

  from this 1 show "a 0 = 2 ^ 0 - 1"

更に from this f1 は with f1 と略せます．

  with 1 show "a 0 = 2 ^ 0 - 1"

　また，事実の参照時に，その名前ではなく，式そのものをバッククォートで囲んだものを用いることも出来ます．つまり

  have "2 ^ 0 - 1 = (0::real)"
    by simp
  with `a 0 = 0` show "a 0 = 2 ^ 0 - 1"
    by simp

のような読み手が「仮定1はどれかな？」と探す必要のない証明が書ける訳です（読み手が居ればですが）．