Isabelle/Isar（その７）

　では，Isarらしい，読み易い証明をステップ毎に改行して書いて見ます．

lemma kudoi:
  fixes "a" :: "nat => real" and "n" :: "nat"
  assumes 1: "a 0 = 0" and 2: "ALL n. a (Suc n) = 2 * a n + 1"
  shows "a n = 2 ^ n - 1"
proof (induction n)
  show "a 0 = 2 ^ 0 - 1"
    proof simp
      show "a 0 = 0"
        proof (rule 1)
        qed
    qed
next
  fix n
  assume "a n = 2 ^ n - 1"
  from this and 2
  have "a (Suc n) = 2 * (2 ^ n - 1) + 1" 
    proof simp
    qed
  also
  have "... = 2 ^ (Suc n) - 1"
    proof simp
    qed
  finally
  show "a (Suc n) = 2 ^ (Suc n) - 1"
    proof this
    qed
qed

初見でも自然に読み下せるのではないでしょうか？これがIsarの可読性です．また，定理の参照や入れ子の証明もtacticのそれより簡単です．ただし，計算機による定理証明に可読性が必要か？　また，ご覧の通りくどく，書くのが面倒なので，Isarでも簡潔に書く為の様々なお約束を用いるのが普通であり，その究極がtacticですから，どの辺りで手を打つかはもはや好みの問題かも知れません．