前回２つの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についての…