Isabelle Tutorial その2

1.4 Variables

もちろんIsabelleは自由変数と束縛変数を区別しますし、束縛変数は名前の衝突が起こらないよう自動で改名されます。この2つに加えて、?で始まる変数があります。これをスキーマ変数(schematic variable)またはアンノウン(unknown)といいます。スキーマ変数は論理的には自由変数と同じですが、Isabelleの証明では自由変数とは異なり他の項に置き換えることができます。

証明を終えるとその定理に含まれる自由変数がスキーマ変数に置き換えられることがわかります。これにより、新たな定理を他の定理の証明に使うことができるのです。実際に証明をしてみると、なんとなくわかってくるかと思います。ただし、スキーマ変数を意識する必要はあまりないでしょう。

1.5 Interaction and Interfaces

Isabelleとshellで直接対話することもできますが、(X)EmacsとProof Generalを使った方が圧倒的に便利です。X-Symbolを使うと更に見やすくなります(私は使っていませんが)。

1.6 Getting Started

Isabelleを起動すると、デフォルトでHOLになります。他の論理を使いたい場合はメニューから選択しましょう。