Re: [isabelle] Length of Proofs

On Tue, 20 Nov 2012, Jeremy Dawson wrote:

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.

This is why I have never separated Isabelle/Isar and Isabelle/ML in that sense, they are just two different languages of the Isabelle user-space. My first command implemented on the Isar toplevel was 'ML'.

Isabelle/ML happens to be used much less in applications these days, though, and this is no problem, merely an indication that the abstractions of Isar do most of your work already without extra tinkering in ML.

Anyway, I've pointed to the Isar command 'method_setup' already. If you look it up in the isar-ref or implementation manual, and then look at 5-10 examples in the library, you should rather quickly get an idea how to define your own basic proof tools, like in the old ML-only times of Isabelle in the 1990-ies.

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.

Users just need to be told about AFP, to preserve things in the longer term. (AFP does not accept ancient 1900-style scripts.)

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

We will come back to this on-topic on the original thread. So far I've skimmed a little over these theories by Christoph Lange, and it looks mostly like a conventional "Isar deflation" job, not old-style ML tinkering.


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