Re: [isabelle] Length of Proofs


I take your first point, that "everything is accessible from ML", but in a practical sense, I would say it's not because the code is so difficult to understand. (Much more difficult than either Isabelle as it was in 1997, or HOL, to give examples within my experience.)

In a way, my first contribution to this thread was to make it clear that both "development" and "ordinary reasoning" are intertwined - there was quite a lot of "development" involved in getting the right combination of compound tactics and proof steps to avoid a proof script which would have been 10000 lines long.

The bigger issue is that pen and paper proofs I do and publish in a journal will be available as long as people want to read them. The Isabelle proofs I do are in Isabelle 2005, and include theory and ML files from 1997, and so will in the future be inaccessible to anyone who doesn't (or can't) install Isabelle 2005 (which only seems to work with one particular version of PolyML). Given the philosophy of Isabelle developers, prospective users need to be warned that if they want to write proofs which will be accessible to future researchers, they need to be done in print.

Finally, it's worth pointing out that no one in this thread has actually come up with a suggestion about how to do the sort of proof which was the subject of my original post other than using Standard ML (which, I understand, was designed for exactly that purpose).


Lawrence Paulson wrote:
As I see it, there are advantages to both interfaces. And everything is accessible from ML simply because it is the implementation language, although of course this access may not be very convenient. I think it's generally accepted these days that the ML level really is more appropriate for development than for ordinary reasoning. It isn't realistic to support both Isar and the ML level as the day-to-day user interface; even with unlimited resources, such duplication wouldn't be very elegant.

Isabelle has undergone very rapid change over the years, and this has meant leaving a lot of old practices behind. I know that it has caused users difficulties in the past, and it's unfortunate, but maintaining upwards compatibility is also very difficult. As one of the earliest Isabelle users, you naturally feel this much more than others do.


On 17 Nov 2012, at 06:04, Jeremy Dawson <jeremy at> wrote:

My understanding has been that you - or someone - introduced new features in Isabelle which were accessible only from Isar, not from the Standard ML interface.

In my book this discourages the use of Standard ML, and also provides an explanation for it having "come out of use", regardless of its relative merits as a user interface language.

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