Email Gateway (Aug 18 2022 at 10:09): Email Gateway (Aug 18 2022 at 10:09):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I am getting problems when trying to use the Sequents logic for
Isabelle. I'm using XEmacs from the Fink package downloader and
Isabelle2005, on a PowerPC mac. I've compiled the logic Sequents,
and once in Proof General switched to using this from the Isabelle --
Logics --> Sequents menu option.
Following the manual (.../doc/Logics.pdf) I type in "context LK.thy"
But then I get the following error messages
context LK.thy
***Outer syntax error : name declaration expected but long
identifier "LK.thy" was found
from typing
context "LK.thy"
*** Could not find theory file "LK.thy.thy" in dir(s) "/Users/pc/
Isabelle/Proof Files", "."
*** Theory loader: the error(s) above occurred while
examining theory "LK.thy"
*** At command "context"
but from typing
context "LK"
I get the message
theory LK = (LK)
Now, again following the example in the Logics manual, if I type the
following
consts A, B :: o;
I get an error of
*** Outer Syntax error: keyword "::" expected but keyword "," was found
Changing this to
consts A :: o
B :: o;
Allows it to work. However, now if I try to prove the simple sequent
" |- A /\ B --> A" via the line
Goal "|- A /\ B --> A";
I get the error
*** Outer syntax error: command expected, but identifier "Goal" was
found
Basically, I'm not sure what has gone wrong; I don't think Isabelle
is working properly at all. I also experienced a problem when trying
to prove automatically that the sum of the first n squares is (1/6)n(n
+1)(2n+1), in that Isabelle cannot do it by "auto" or any other
method (this was back in HOL). The proof of the sum of the first n
integers being (1/2)n(n+1) works fine by induction, and since by hand
the proofs follow the same pattern and are very similar, I assume
that the first n squares proof would be similarly easy. When I
turned on the simplifier trace for this problem to see what was
happening, it did not stop, and one time actually shut down XEmacs
and left me looking at a blank X-Term window.
Any insights anyone could give me would be greatly appreciated.
Many thanks
Peter Chapman
Email Gateway (Aug 18 2022 at 10:09):From: Makarius <makarius@sketis.net>
The above commands refer to the old ML toplevel of Isabelle, but the
ProofGeneral setup uses the Isar toplevel, which is described in the
isar-ref manual.
In order to see how this works for Sequents, just open one of the example
theories, e.g. Sequents/LK/Nat.thy and start stepping through the source.
In Isabelle2005 these theories still have an appendix in ML with the
actual proofs, but it is hard to use these with ProofGeneral. In recent
development snapshots of Isabelle (cf. http://isabelle.in.tum.de/devel/)
everything has been converted into proper theory sources already.
Makarius
Email Gateway (Aug 18 2022 at 10:09):From: Peter Chapman <pc@cs.st-and.ac.uk>
Thanks.
Another problem, though. Now I'm trying to implement the sequent
calculus G3ip. The whole file builds/loads until the last line,
which is
ML {* use_legacy_bindings (the_context ()) *}
which spits back the error
*** Error:
*** Can't unify bool with Thm.thm (Different type constructors) found
near
*** val false = thm("false")
*** Failure
*** At command "ML" .
I don't know which file it is looking at with the line val false
= thm("false") . I wrote a file called G3ip.ML similar to LK0.ML,
but still got the error (I don't know if that is where the error
comes from in the first place). I can't find anything in the
documentation, or a few hours worth of internet searching, to tell me
how to fix this error, or even what is causing it.
The top line for my file, if that is relevant, is
theory G3ip
imports Sequents
begin
.
.
.
Any help would be greatly appreciated.
Cheers
Peter Chapman
Email Gateway (Aug 18 2022 at 10:09):From: Makarius <makarius@sketis.net>
On Fri, 9 Feb 2007, Peter Chapman wrote:
Another problem, though. Now I'm trying to implement the sequent calculus
G3ip. The whole file builds/loads until the last line, which isML {* use_legacy_bindings (the_context ()) *}
which spits back the error
*** Error:
*** Can't unify bool with Thm.thm (Different type constructors) found near
*** val false = thm("false")
*** Failure
*** At command "ML" .
Here SML complains about an attempt to use an existing constructor (false)
in a thm value binding. This kind of incident explains why the above
function is called use_legacy_bindings -- you probably won't need these
bindings anyway.
I wrote a file called G3ip.ML similar to LK0.ML
This is another legacy feature. There is no need to use ML files, just
produce plain Isar sources. E.g. see the version of Sequents in recent
Isabelle development snapshots, which no longer feature these strange ML
things.
Makarius
Last updated: May 03 2024 at 08:18 UTC