ファクト、ステートメント

thm 定理名 というコマンドで定理＝ルールを表示できるが、存在しない定理名を指定すると、Undefined fact と出る。ということは、実装上は、既存の定理をfactと呼んでいるようだ。

print_statement 定理名 というコマンドで表示されるのは、定理名（ラベル）とその命題。だが、命題は、Isar statement formatで表示される。Isar statement formatは、fixes/assumes/shows が基本の形。

ということは、ステートメントとは、単一命題というよりは、パラメータ変数、仮定、結論という構造を持つ。実際、isar-refの2.2.2のタイトルは"Structured statements"だ。単一の命題は、結論のみのステートメントとみなすのだろう。