Re: [isabelle] "and similarly..."



On Wed, 1 Feb 2012, Jeremy Dawson wrote:

You have to be using the ML interface to Isabelle to do this - which, I understand, is what ML was originally designed for - and so is particularly well suited for.

Contemporary Isabelle does not really have anything that could be called "ML interface". There is Isabelle/ML and Isabelle/Isar, and both are intertwined in a certain way: ML is used for the implementation of Isar, and Isar embeds ML into its formal context later on in the bootstrapping.

The primary "interface" to the user is the Isar source language (by definition). It can refer to ML in better ways than ever before in the history of LCF-style theorem proving. The current Prover IDE (Isabelle/jEdit) even provides hyperlinks for ML entities and inferred types. The TTY loop is a bit more awkward here, and in fact close to being useless.


Taking Isabelle/Isar and Isabelle/ML together, it is possible to define your own proof methods, say to automate certain standard proof schemes. This transfers the old LCF idea of user-defined tactics into the world of Isabelle/Isar, but not much more.

What is conceptually missing is a systematic way to define proof patterns in a more structured language. Ltac of Coq marks some success in that respect: it allows users to define tactics quickly without embarking on details about ML.

Nonetheless, instead of adding a "proof programming language" to Isar, I conceptually prefer to keep the language as is, and instead empower the Prover IDE around it. With serious "proof refactoring", which is a non-trivial thing to provide, one could imaging certain "and similarly ..." operations on the source.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.