Re: [isabelle] Length of Proofs



On Thu, 1 Nov 2012, Jeremy Dawson wrote:

In such a case it is advantageous not to have to write them all down repeatedly, but to reuse them. The Standard ML interface to Isabelle is ideally suited to this purpose. Unfortunately its use has become actively discouraged in recent years.

As far as I am concerned, I never discouraged the use of Isabelle/ML, it merely came out of use as proof scripting languages, because there are better ways these days. Christian Sternagel has already hinted at the fine art to combine structured Isar proof elements, and an assorted collection with proof tools.

If you still want to have hard-core quick script hacking, the community for that is centered around SSReflect, which is continuing traditions of APL for proof recording. The scripts then come out very tight and terse, by experts for experts.

I am still keen to seen such a quick-hacking approach turned into proper use for an advanced Prover IDE: instead of recording the gesticulation of the author in the script, it would produce a nice structured, readable, maintainable proof document.


	Makarius





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