[isabelle] Problems with Sequents in Isabelle
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
***Outer syntax error : name declaration expected but long
identifier "LK.thy" was found
*** 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
I get the message
theory LK = (LK)
Now, again following the example in the Logics manual, if I type the
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and