cocolog:91995523
Isabelle 2020 の HOL を使った「ケネディと天使の問題を Isabelle で証明」という記事を書いた。Isabelle の Tips とともに…。 (JRF 4196)
JRF 2020年6月22日 (月)
……。
特定の定理や定義を表示したいとき、THEN の結果を出力したいときは…
<pre>
thm trans [THEN sym]
</pre>
…などとすれば良い。
JRF2020/6/226616
……。
jEdit の Plugins -> Plugin Options の Isabelle の General の中の "Completion Immediate" の項目のチェックボタンをオフにした上で…。
古い notation では、\<forall> は ALL、\<exists> は EX、\<in> は : (type に対しては ::)、\<lambda> は %、\<and> は &、\<or> は |。
JRF2020/6/229935
\<open> \<close> は {* *} であったらしいのだが、そちらを使うと legacy だという警告が出る。
JRF2020/6/224437
……。
jEdit の Utilities -> Global Options の中の Shortcuts に Choose keymap の項目があって、そこで Emacs を選んだ上で、まず、C-x C-s と C-s の設定をする。
あと、C-e を prefix に持っているものをすべて削除で C-e が(同じじゃないが)使えるようになる。
JRF2020/6/222195
……。
……。
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
JRF2020/6/224758
《ケネディと天使の問題を Isabelle で証明 その３ 悪戦苦闘編 - JRF のソフトウェア Tips》
http://jrf.cocolog-nifty.com/software/2020/06/post-33c483.html
JRF2020/6/221915
……。
オブジェクト指向を PTS などの論理でどう表すかというのが、大学院時代の私のテーマとしてあった。その流れが今回につながっている。
大きな前進とまではいかないが、一つの大事な例にはなったかな…というのが感想。
JRF2020/6/228971
……。
……。
追記。
ついでなので↓を Isabelle2020 に対応させておいた。
《The Proofs about Alpha-equivalences in Isabelle》
http://jrf.cocolog-nifty.com/software/2016/01/post.html
isabelle_TheLambda のバージョンは 0.0.3。
JRF2020/6/223271
ZF のモジュールについて例えば Finite は ZF.Finite に書き換える必要があり、一部シンボルを書き換える必要があった (le → \<le>、lepoll → \<lesssim> だけだったと思う。)
証明が止まったのは二ヶ所ほどで、あとはすんなりいけた。楽な作業だった。
JRF2020/6/226054
……。
……。
追記。
kennedy_problem 更新。バージョン 0.0.2。
証明の最初、simp ではなく unfold を使うようにするなど微調整。
JRF2020/6/233990
前に Isabelle を使ったのが 2015 年。そのときの Tips は [cocolog:83987061] にある。
それにプラスしていくつかの Tips。
JRF2020/6/226115