セミナーの内容

定理証明支援ツール Isabelle では、証明を記述する方法が2つあります。1つは apply スタイル、もう1つは Isar スタイルと呼ばれているものです。

Isar スタイルは数学のテキストに書かれている証明のように読めることが特徴です。apply スタイルで記述された証明は、Isabelle の中でコマンドを実行して途中の状態（残されているサブゴール）確認しながらでなければ読めません。これに対して Isar スタイルでは、ある時点までに得られた補題とこれから証明しようとしている命題を証明中に記述することができるので、テキストとして読むことができます。以下に例を示すので雰囲気を味わってみてください。

apply スタイルで書いた証明：

theorem
  "∀x. P ⟶ Q x ⟹ P ⟶ (∀x. Q x)"
apply(rule impI)
apply(rule allI)
apply(drule_tac x="x" in spec)
apply(drule mp)
apply(assumption)
apply(assumption)
done

Isar スタイルで書いた証明：

theorem
  assumes "∀x. P ⟶ Q x"
  shows "P ⟶ (∀x. Q x)"
proof
  assume "P"
  show "∀x. Q x"
  proof
    fix a
    from assms have "P ⟶ Q a" ..
    from this and ‹P› show "Q a" ..
  qed
qed

解説する内容はすべて Isabelle の公式文書に書いてあることです。つまり読めば得られる知識です。それでも、半日集中して習得できるほうがよいという人のためのチュートリアルです。よかったらどうぞ。

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

• apply スタイルの知識（Isabelle チュートリアル第1回と第2回程度の知識）

必要なもの

• Isabelle

配布物と Zoom Meeting の URL

セミナー開始時刻までに CONNPASS のメッセージにてお知らせします。 同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。
• 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
• 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。