Isabelle/Isar（その15）

　さらに１つ目のサブゴールの証明は

  from 1
  have "a 0 = 0"
    by simp
  also
  have "... = 1 - 1"
    by simp
  also
  have "... = 2 ^ 0 - 1"
    by simp
  finally
  show "a 0 = 2 ^ 0 - 1"
    by this

のように，calculationを生成するコマンドalsoと，その結果をthisとして参照するコマンドfinallyを用いて，推移律を活かした形にも書けます．

　一般の書式は

  have "X = (A::real)" sorry
  also
  have "... = B" sorry
  also
  have "... < C" sorry
  also
  have "... = Y" sorry
  finally
  have "X < Y" by this

であり，勿論haveの前にfromを入れることも出来，最後が結論ならshowとなります（利用できる推移律には等号のほか，print_trans_rules で表示されるものあります）．なお，sorryはproveモードのコマンドで「証明出来たことにします」というやや危険な代物です．

　また，証明の最後をby thisとしているのは，finally（fromと同じくstateの前にchainモードに入るコマンド）により，thisが1 - 1 = 2 ^ 0 - 1から最初と最後とを結んだcalculationのa 0 = 2 ^ 0 - 1になった為で，by thisは . と略すことも出来ます．