定理の表示

lemmas（複数形！）というコマンドがある。lemmas G = A B C のように書いて、複数の定理をグルーピングできる。lemmas X = A なら、定理Aに別名Xを与えることが出来る。

これを使うと、特定の名前Aの定理の内容を目視できる。ダミーの名前 X を使って、lemmas X= A とする。

TrueIは、論理式（論理定数も論理式）Trueの導入規則に対応する定理（＝Pureの証明できる命題）。（Pureの論理式はなぜか命題と呼ぶ。）

lemma TrueI: True
  unfolding True_def by (rule impI)

lemmas X_1 = impI (* (?P ==> ?Q) ==> ?P --> ?Q *)
lemmas X_2 = True_def (* True ≡ False --> False *)

lemma MyTrueI: True
(* ==> True *)
apply (unfold True_def) (* False --> False *)
(* ==> False --> False *)
apply (rule impI) (* (?P ==> ?Q) ==> ?P --> ?Q *)
(* False ==> False *)
apply (assumption)
done