Isar概要

1. 証明は、複合証明 proof ... qed か、自動証明 by ... のどちらか。
2. 自動証明の根拠と複合証明のヘッダ部には証明メソッドが書かれる。
3. 複合証明の本体（ボディ）部は、文（ステートメント）の列。
4. 文（ステートメント）は次の種類：
   1. fix文 自由変数の宣言
   2. assume文 仮定（assumption）の宣言
   3. have文 中間段階で得られた命題の記述
   4. show文 最終的に得られた命題の記述
5. have文の命題は中間結果と呼ぶ。
6. show文の命題は結論（conclusion）、または最終結果と呼ぶ。
7. have文またはshow文には、入れ子になった証明が後置される。
8. 証明全体で、assumeで入れた仮定から、showで示した結論を導く。assum ⇒ concl。
9. showが結論を示すので、Mizarのthusに近いか。

"A Tutorial Introduction to Structured Isar Proofs" by Tobias Nipkow

Thus the proof text is only suitable for the machine; for a human, the proof only comes alive when he can see the state changes caused by the stepwise execution of the commands. Such proofs are like uncommented assembly language programs.

Isabelleのネイティブスタイル

1. T:A⇒B と U:A に対して、TをUにアプライすることを T[OF U] と書く。関数が f (of x) であるのと一緒。結果はBとなる。
2. Isabelleの自由変数は ?名前 の構文を持つ。変数はインスタンス化される。
3. 証明メソッドは、推論規則以外に、simp単純化とblastソルバーがある。

注意：

1. 複合証明のヘッド部の証明メソッドは丸括弧に入れる。(rule impI) など。
2. Isabelleの命題（論理式）はすべてストリング形式で書かれる。ストリングの直前にラベルが許される。
3. Isabelleでは公理や仮定のこともruleと呼ぶ。←バカヤロー
4. show 結論 proof ... qed の形になるので、showがtargetのように使われて、ちっともshowの感じがしない。むしろ、showは次の証明の開始だと思ったほうがいいくらい。
5. ?thesisはカレントゴール（target）を示すパターン変数。
6. 直前の命題はthisで指す。
7. fromはラベルを後置して、show, haveの前提を明示する。p:P ... from p show Q は、assume P show Q と同じ。