では，くどく解説していきます．まず 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" がコマンドlemmaとその引数です（ttyインターフェイスではここで改行で…

では，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 …

Isabelle/Isarのセッションは，theoryモード，proofモードからなっています． まず，theory-beginまで入力すると，theoryモードに入ります．theoryモードはIsarが「これから定義や定理，証明を書いてください」と言っている状態です．またシステムのパラメー…