Email Gateway (Aug 18 2022 at 12:27): Email Gateway (Aug 18 2022 at 12:27):From: Devrim Ünal <devrimunal@gmail.com>
Hello,
I'm new to the list so this is probably a well known fact but I could
not find any information...
I want to run Isabelle over some theories developed by another
researcher. I downloaded
the theories but can not run them in Isabelle 2008.
They are of the form
theory Basic_Op_Rules = Basic_Inf_Rules :
section {* Basic properies *}
lemmas kbox = K_BOX[THEN temp_mp];
lemmas kpbox = K_PBOX[THEN temp_mp];
theorem box1 : " H |- BOX(NEXTA A) -> BOX(A -> NEXTA A) "
apply(rule kbox);
apply(rule MWeak);
apply(rule Nec1);
apply(rule t);
done
...
Any comments on how I can run/convert them so that they work in Isabelle 2008?
Thanks a lot.
Devrim
Email Gateway (Aug 18 2022 at 12:27):From: Tjark Weber <tjark.weber@gmx.de>
Devrim,
converting theories can be a daunting task (especially if they are very
old or very large). You can try running "isatool fixheaders", but if
you still get error messages afterward that you cannot fix easily, I
have another suggestion: how about installing the version of Isabelle
that these theories were originally developed for? Old Isabelle
releases are available from
http://www.cl.cam.ac.uk/research/hvg/Isabelle/download_past.html
Best,
Tjark
Email Gateway (Aug 18 2022 at 12:27):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Tjark Weber wrote:
This is, at best, only a partial solution. I've done a mass of work
recently in Isabelle2005 because it's built on other stuff which works
on Isabelle2005. But what happens when I want to combine it with
someone else's theories which are written in Isabelle2007? This looks
like being a serious problem for me.
On a similar theme, I have been recently helping a colleague who wants
to get some familiarity with Isabelle. He found some tutorial material
on the web somewhere, but it didn't work. Why? Because it was written
before the changes made in Isabelle2007. We had to revert to
Isabelle2005 to run it.
Yesterday, he was trying to run a different lot of tutorial material
which he had found somewhere. It didn't work either, because it used a
form of syntax I've never seen before. I would guess it's Isabelle2008
(which I've never used). (It's primrec statement is totally different
from anything I've seen in the last 10 years).
These issues seem to be capable of causing massive and unnecessary
difficulties.
Jeremy
Email Gateway (Aug 18 2022 at 12:27):From: Amine Chaieb <ac638@cam.ac.uk>
Isabelle's documentation, including tutorials, is tested in every
release and even in every development snapshot. The documentation files
are generated from Isabelle, and they actually go through the Isabelle
Kernel to check the proved theorems and the syntax etc...
Amine.
Jeremy Dawson wrote:
Email Gateway (Aug 18 2022 at 12:28):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Amine Chaieb wrote:
Dear Amine,
I'm not sure precisely what your point is, but let me assure I'm not
denying that for each theory file my colleague found on the web, there
is a version of Isabelle in which it runs successfully.
Nor was I asserting that either or both the theory files he found was
taken out of an Isabelle release.
Regards,
Jeremy Dawson
PS. Anyway, what aspects of the documentation are actually tested? I
notice that the Isabelle2008 documentation refers to a significant
number of functions which don't seem to exist in the actual Isabelle2008
(eg, context, update_thy, byev, findI, get_thm, brs), unless they're
hidden in some structure - but if that is so, the documentation should
say so.
Last updated: Nov 21 2024 at 12:39 UTC