IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、setup Pure_Thy.old_appl_syntax_setupというコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされ…

空列はPureの項ではない。 任意の識別子は項になる。 型推論される。 勝手な識別子の型は型変数 'a とされる。型総称な変数ということだろう。 併置は適用演算のはず。 ラムダ抽象は %x. A 、ピリオドの直後の空白は必須。 η変換は自動で行う。 β変換も自動…

proof method, tactic, rule, proof script, proof command あたり。proof commandの定義はない。commandの分類に、theory command, proof commandとかあって、lemmaはproofコマンドに分類されてる。「lemmaはゴールコマンドだ」とかの記述もあった。コマン…

文書指向へと舵を切ったウェンツェルだが、まだまだ全然だし、先は長いし、苦難が予想される。 用語法、メンタルモデルがスクリプト指向のまま。 ウェンツェル自身もfact, goalを多用している。 論理の概念・用語法と、ソフトウェアとしての証明系の用語・文…

infix operatorの優先度の一覧が欲しいだけど、isabelle infix operator precedence とかでググッてもあんまり分からん。Coqだと、公開されているHTMLマニュアルが引っかかったけど、Isabelleは粒度がでかいPDFだからなーー。[追記] introの"4.1.1 Infix Ann…

ここにまとめることにする。追加情報は追記していく。配布に付いているPDF文書、同梱文書と呼ぶことにする。略称はファイルのベース名。 タイトル ページ数 略称 Programming and Proving in Isabelle/HOL 63 prog-prove A Proof Assistant for Higher-Order…