さて，これまでは数列を定理の中で，言わば局所的に定義しましたが，セッション全体を通して大域的に定義すると，システムが証明に便利な定理を自動的に用意してくれます． まず，数列Xを次のように定義します． fun X :: "nat => real" where "X 0 = 0" | "…

次に帰納法の２つ目のサブゴールに移ります． next case (Suc m) と入力すると，Outputは proof (state): step 7this: 1 ≤ m ⟹ a m = 2 ^ m - 1 1 ≤ Suc mgoal (1 subgoal): 1. ⋀n. (1 ≤ n ⟹ a n = 2 ^ n - 1) ⟹ 1 ≤ Suc n ⟹ a (Suc n) = 2 ^ Suc n - 1 さら…

premsを参照する例として lemma fixes "a" :: "nat => real" and "n" :: "nat" assumes "a 1 = 1" and "!!n. 1 <= n ==> a (Suc n) = 2 * a n + 1" shows "1 <= n ==> a n = 2 ^ n - 1" の証明を考えます．これは自然数の成り立ちからすれば途中から始まる帰…