では証明を説明しましょう． by (induct n, simp_all) まず，byコマンドの引数はイニシャルプルーフメソッド，ターミナルプルーフメソッドの２つであり，それぞれ証明の方法，いわゆるmethodを指定しますが，ターミナルはイニシャルが残した証明の目標サブゴ…

それでは解説です．まず最初の lemma lem01: はこれから lem01 という名前のレンマを証明するというコマンドで，後に参照しないなら lem01: は不要です．lemmaコマンドには少なくとも１つの引数が必要で，それが "(a::nat=>real) 0 = 0 & (ALL n. a (Suc n) …

例として a_{0}=0 かつ 任意の自然数nについてa_{n+1}=2 a_{n}+1 ならば a_{n}=2^n-1 が定理であることの「簡潔な証明」を示します． そのまえに対話型の証明作成はその名の通りシステムの出力を見ながら進めるもので，Outputパネルのタブを右クリックし，フ…

それでは使ってみましょう．前回同様にjeditを起動すると，デフォルトでユーザーホームディレクトリのScratch.thyというファイルが（なければ作成され）ロードされますので，まずは theory Scratch imports Complex_Main begin end と入力してください．１行…