更に２つ目のサブゴールは，帰納法の変数nが1以上，つまり，Suc n_の形の場合なので，場合を設定するコマンドcase Suc を用いて簡素化出来ます．それは lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a…

Isarに負けないよう，くどく続けます． 仮に以上の計算過程を省略するなら，これまでの話から，次のように書けることが判るでしょう． lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a n + 1" shows "a…

では帰納法の２つ目のサブゴールの証明部分を解説しましょう． まず，１つ目の証明から２つ目に移ることをシステムに告げているのが next です．するとIsarは proof (state): step 14goal (1 subgoal): 1. ⋀nat. a nat = 2 ^ nat - 1 ⟹ a (Suc nat) = 2 ^ Su…