[isabelle] Problems with Sequents in Isabelle



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






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