宣伝: 『「シミュレーション仏教」の試み』(JRF 著)。Amazon Kindle で販売中!
技術系電子本。Python による仏教社会シミュレーション( https://github.com/JRF-2018/simbd )の哲学的解説です。令和4年3月11日発売。

« 前のひとこと | トップページ | 次のひとこと »

cocolog:91995523

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

JRF 2020年6月22日 (月)

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

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

JRF2020/6/226115

……。

特定の定理や定義を表示したいとき、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 で証明 その1 うそつき天使問題 - JRF のソフトウェア Tips》
http://jrf.cocolog-nifty.com/software/2020/06/post-ef863f.html

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

JRF2020/6/224758

《ケネディと天使の問題を Isabelle で証明 その3 悪戦苦闘編 - 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

« 前のひとこと | トップページ | 次のひとこと »