このように仮定に近いサブゴールの証明はsimp任せに出来ますが，多くの場合いきなりサブゴールをshowするのは難しく，そこに至るまでの中間のサブゴールを適宜設けてそれらを証明，統合してshowとなります． もし今回の仮定 "a 0 = 0" からサブゴール "a 0 =…

また，1と名付けた事実の参照は，usingを用いて show "a 0 = 2 ^ 0 - 1" using 1 by simp 更にstaementの前に，fromを用いて from 1 show "a 0 = 2 ^ 0 - 1" by simp とすることもできます．仮定に限らず一般の定理の参照も同様ですが，from，usingでは変数…

つまり１つ目のサブゴールの証明は show "a 0 = 2 ^ 0 - 1" proof simp show "a 0 = 0" proof (simp add: 1) qed qed のようにsimpのみで賄えるわけですから，内側のproofを外側に重ねられそうです．実際 show "a 0 = 2 ^ 0 - 1" proof (simp add: 1) qed の…

前回２つのproofコマンドの引数ととしたmethodは，simpとrule 1でした． simpは見ての通り計算も出来ますし lemma "A & B --> A" by simp のようにロジックも解し，かなり多才ですがあまり深いことは出来ません．例えば lemma "(0::real) <= x ^ 2 + 1" by s…

Isarのproofモードは，荒く言って 証明の目標の明言を要請するstateモードと，その証明の方法を要請するproveモードの対 の列であり，コマンドとしては，前者にはshow系のshowsやshow，後者にはproof系のproofやbyやapplyを用います．実際，（その８）と（そ…

前回の内容を入力し終わると，Outputは proof (prove): step 0 goal (1 subgoal): 1. a n = 2 ^ n - 1 となり，証明待ちモードに入ったことが判ります． ここからいよいよ証明です．最初の proof (induction n) はshowsで指定した結論を自由変数nについての…

では，くどく解説していきます．まず 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が「これから定義や定理，証明を書いてください」と言っている状態です．またシステムのパラメー…

では証明を説明しましょう． 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 と入力してください．１行…

Isabelle/HOLはHOLのラッパーですが，HOLにはない「推論規則による（危うげな部分も含む）マッチング」が特徴です．ただしかつてのapply-doneによるタクティック列挙の証明は，現在は構造化された言語Isar上でのエミュレーションとなっており，証明のスタイ…