Re: [isabelle] Lifting variables in theorem



On Mon, 3 Feb 2014, Jeremy Dawson wrote:

On 02/03/2014 09:11 PM, Makarius wrote:
 On Mon, 3 Feb 2014, Jeremy Dawson wrote:

> My whole point is that it should NOT be difficult for anyone to run > proofs today which were written in 2005 (or, indeed, much earlier).

 That problem is de-facto solved since 2004: Isabelle/AFP http://afp.sf.net

 You merely need to put your material into shape (according to minimal
 standards that are routine today) and submit it to the editors of the
 archive.  Afterwards it is usually maintained "automagically" to work with
 current Isabelle versions, but in extreme cases the editors might ask for
 you for assistance.
Hi Makarius,

I've been told similar things on occasions before, and it turns out not to be true. Unless (in this case), your "minimal standards" means rewriting everything in Isar. Which, as my previous email pointed out, is not on, since I'm guessing my latest effort involves three to four hundred thousand tactic applications.

If I'm wrong about this, please clarify

What you call "Isar" above is merely the tactic script emulation, which is also called "apply-style" occasionally. This is a minimal standard from around 2002, but your ML scripts follow the one of 1998. Proper Isar proofs are something else.

In old versions of Isabelle there is even some perl script to help in the semi-automatic conversion, cf. "isabelle convert" in Isabelle2005, but it was deleted later since it is long obsolete.

This thread is now once again where it gets since 10 years or so: after 15 years of introducing a new Isabelle theory format, to replace the old Foo.thy/Foo.ML pair, someone is still using something that hardly anybody else remembers or cares about.


	Makarius




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