Isabelle 2020 の HOL を使った「ケネディと天使の問題を…

Isabelle 2020 の HOL を使った「ケネディと天使の問題を Isabelle で証明」という記事を書いた。Isabelle の Tips とともに…。
JRF 2020年6月22日

前に Isabelle を使ったのが 2015 年。そのときの Tips は [cocolog:83987061] にある。

それにプラスしていくつかの Tips。

JRF 2020年6月22日

……。

特定の定理や定義を表示したいとき、THEN の結果を出力したいときは…

<pre>
thm trans [THEN sym]
</pre>

…などとすれば良い。

JRF 2020年6月22日

……。

jEdit の Plugins -> Plugin Options の Isabelle の General の中の "Completion Immediate" の項目のチェックボタンをオフにした上で…。

古い notation では、\<forall> は ALL、\<exists> は EX、\<in> は : (type に対しては ::)、\<lambda> は %、\<and> は &、\<or> は |。

JRF 2020年6月22日

\<open> \<close> は {* *} であったらしいのだが、そちらを使うと legacy だという警告が出る。

JRF 2020年6月22日

……。

jEdit の Utilities -> Global Options の中の Shortcuts に Choose keymap の項目があって、そこで Emacs を選んだ上で、まず、C-x C-s と C-s の設定をする。

あと、C-e を prefix に持っているものをすべて削除で C-e が(同じじゃないが)使えるようになる。

JRF 2020年6月22日

……。

……。

Tips はここまでにして今回の記事について。記事は↓。

《ケネディと天使の問題を Isabelle で証明 その１ うそつき天使問題 - JRF のソフトウェア Tips》  
http://jrf.cocolog-nifty.com/software/2020/06/post-ef863f.html

《ケネディと天使の問題を Isabelle で証明 その２ 気まぐれ天使問題 - JRF のソフトウェア Tips》  
http://jrf.cocolog-nifty.com/software/2020/06/post-d9cd87.html

JRF 2020年6月22日

《ケネディと天使の問題を Isabelle で証明 その３ 悪戦苦闘編 - JRF のソフトウェア Tips》  
http://jrf.cocolog-nifty.com/software/2020/06/post-33c483.html

JRF 2020年6月22日

……。

オブジェクト指向を PTS などの論理でどう表すかというのが、大学院時代の私のテーマとしてあった。その流れが今回につながっている。

大きな前進とまではいかないが、一つの大事な例にはなったかな…というのが感想。

JRF 2020年6月22日

……。

……。

追記。

ついでなので↓を Isabelle2020 に対応させておいた。

《The Proofs about Alpha-equivalences in Isabelle》  
http://jrf.cocolog-nifty.com/software/2016/01/post.html

isabelle_TheLambda のバージョンは 0.0.3。

JRF 2020年6月22日

ZF のモジュールについて例えば Finite は ZF.Finite に書き換える必要があり、一部シンボルを書き換える必要があった (le → \<le>、lepoll → \<lesssim> だけだったと思う。)

証明が止まったのは二ヶ所ほどで、あとはすんなりいけた。楽な作業だった。

JRF 2020年6月22日

……。

……。

追記。

kennedy_problem 更新。バージョン 0.0.2。

証明の最初、simp ではなく unfold を使うようにするなど微調整。

JRF 2020年6月23日