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

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: Re: [isabelle] "and similarly..."
*From*: Makarius <makarius at sketis.net>
*Date*: Wed, 15 Feb 2012 12:19:35 +0100 (CET)
*In-reply-to*: <4F287341.70602@rsise.anu.edu.au>
*References*: <A49A52D0-C544-488B-8B82-A224DA214AD5@cam.ac.uk> <4F287341.70602@rsise.anu.edu.au>
*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.*