Re: [isabelle] Isabelle 2005 request



Dear Anonymous Reviewer,

please see the files at the URL
http://users.cecs.anu.edu.au/~jeremy/tmp/

Issue (1) - use of an old version of Isabelle.  This was a new version
once, when I first did proofs in this area.  Unfortunately new
versions are highly incompatible, like a different prover with the
same name, so I'm stuck with the old one.  As the reviewer has
discovered, the developers have also at some time stopped making the
2005 version and installation instructions available on their archive.

However I have just installed it on a borrowed computer in London,
running Linux, with the following details:

Linux robotpc3-temp.cs.ucl.ac.uk 3.6.11-4.fc16.i686.PAE #1 SMP Tue Jan 8 21:18:14 UTC 2013 i686 i686 i386 GNU/Linux

So here are instructions for what I did (from memory, unfortunately,
as the computer I've borrowed erases user files on reboot(!)).  

That computer does have 32-bit libraries installed!

Doing (from the directory where you unpack polyml-4.1.4.tar) cd
polyml-4.1.4/x86-linux ldd poly may make it clear whether you need to
install them

Go to 
http://users.cecs.anu.edu.au/~jeremy/isabelle/
Download Isabelle2005.tar and polyml-4.1.4.tar	

Choose a directory to work (it's /home/users/jeremy in my own case)

Put the tar files into that directory and unpack them (tar xvf filename.tar)

In Isabelle2005/etc/settings you need to edit it by changing
/home/users/jeremy to whatever directory you have chosen to use

Then type 
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).
which should start Isabelle 2005

If this works you can type 
[sym, refl, trans] ;
and it will display the text of those three theorems.

For the specific work of the paper you need to download a lot of files from
http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/

Easiest to download just gen.tar and unpack it, to create a whole lot of files
in your directory (which you need to create) isabelle/2005/gen/
(or choose another directory if you like)

Get into this directory and start Isabelle as above by 
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).

Then
use_thy "tripartite" ;
should run a lot of preliminary proofs then the results of the paper
(of which the last is wf_rearr_n)

Issue (2) - the url in the paper had not been updated.  Mea culpa.
What can I say, except that it's my fault, not my co-authors'. 
And to compliment the referee(s) - I think most don't try to check on the
proof files.  Of course it's just Murphy's Law that this happens when I'm 
not able to fix it right away.  And I'm sorry if the half-baked attempts to 
fix it by email led to wasting more of their time.

Issue (3) - this theorem is the last in tripartite.ML, and the last 
to show when 



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