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
This archive was generated by a fusion of
Pipermail (Mailman edition) and