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.firstname.lastname@example.org>
- References: <A49A52D0-C544-488B-8B82-A224DA214AD5@cam.ac.uk> <4F287341.email@example.com>
- 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and