Pureの機能、分からない所
次は最初から使える。
- typedecl 型または型構成子を導入できる。型レベルでの定数（＝型名）と定関数（＝型構成子）のシグネチャ宣言のようなもの。
- class 型クラスは使える。「class 名前だけ」というのも特別にあって、これでユニバーサルな型クラスを定義できる。ユニバーサルな型クラスは、Coqで言えばTypeに相当するもの。typeというクラス定数（ソートか？）はある。
- locale 型クラスがあるんだから、localeもあるだろう。
- default_sort 「ソート」と「クラス」の使い分けがワカランけど、ともかく型変数が特定のクラスのインスタンスでないときは、デフォルトソートだとみなすようだ。ソート≒クラス≒カインドだと思う。
- axiomatization/where シグネチャと公理の登録。シグネチャだけ、公理だけでもいい。セオリーの素材を登録（＝生成）する基本的な道具。
- judgment 意味不明だったが、ポールソンの古い論文 foundation(https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf) でだいたい分かった。ユーザー定義論理の論理式を、Pureの論理式（なぜか命題と呼ぶ）にマップする関数とその構文を定義する。Truepropという名にするのが習慣だが、isTrueとかProvableとかでもいいと思う。ポールソン論文ではjudgmentにスコットブラケットを使っている。しかし、最近はスコットブラケットがPure内部で使っているからまずいだろう。
- definition, abbreviation 定義・略記の展開が出来る。unfoldメソッドを使うのだろう。axiomatization、definition, abbreviationの使い分けがイマイチわからない。
- assumes/shows形式の定理の記述（ステートメントというのか？）が出来る。よく分かってない。
- THENなどのタクティカルが使える。よく分かってない。
- ルール＝Pureの公理（ファクトか？）を使うapply以外だと、assumption, (unfold def) がapplyとして使える。
- OFというタクティカルもある。
- insertというメソッド
- カンマ、縦棒、プラスというタクティカル。
- nonterminal, syntax, translationはたぶん構文的な何かだろう。知らない。
- lemmaは、接続詞（and）なしで、複数慣れべてもよい。まとめて書ける。
- abbreviationには、where宣言部の前にシグネチャを書ける。
- mixfixにbinderというのがある。
- notationはけっこう複雑な指定が出来る。
ワケワカンナカッタのは、judgmentだが、ポールソンの言うメタ論理とオブジェクト論理の関係から分かった。メタ論理＝Pureについては、Pureの証明機構がどうなっているか、まだ理解できない。Pureにおける証明状態がどう保持されていて、証明メソッドでどう遷移するか、その操作的（operational）意味論がまだ不鮮明。
ウェンツェルはIsar証明マシン（Isar/VM）を（不十分に）定義しているが、Pure証明マシンの詳細な構造と操作方法が必要だ。
