Email Gateway (Aug 18 2022 at 11:57): Email Gateway (Aug 18 2022 at 11:57):From: Beta Ziliani <beta.ziliani@gmail.com>
Dear Isabelle User Group:
I've this problem using X-Isabelle. I've just downloaded Isabelle, with
Emacs 21.4.20 in a Kubuntu 7.10. Looking at the tutorial I put this simple
excercise
theory ToyList
imports PreList
begin
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
consts app :: "'a list => 'a list => 'a list" (infixr "@" 65)
rev :: "'a list => 'a list"
primrec
"[] @ ys = ys"
"(x # xs) @ ys = x # (xs @ ys)"
primrec
"rev [] = []"
"rev (x # xs) = (rev xs) @ (x # [])"
end
But whenever I want to do something useful , like use the command (by
pressing the Command button in the Proof General Toolbar)
value "rev (True # False # [])"
Isabelle respond with a
*** Illegal application of command "value" at top level
*** At command "value".
I'm making things wrong, or my installation is wrong?
Thanks in advance,
Beta
Email Gateway (Aug 18 2022 at 11:58):From: Makarius <makarius@sketis.net>
If you have come that far then the installation is fine. You are merely
experiencing a logical problem, trying to refer to formal entities without
a theory context: the 'value' command needs to be issued while the theory
is still open, before the final 'end'.
Makarius
Email Gateway (Aug 18 2022 at 11:58):From: Makarius <makarius@sketis.net>
This means you cannot issue it in the mini buffer command line of Proof
General, but have to put it into the true theory text.
Makarius
Email Gateway (Aug 18 2022 at 11:58):From: Makarius <makarius@sketis.net>
At that point you do not have the datatype, only the content of the
PreList theory.
Makarius
Email Gateway (Aug 18 2022 at 11:59):From: Beta Ziliani <beta.ziliani@gmail.com>
Thank you Makarious and Florian, but I'm still getting the same message with
the theory opened. What else could it be?
Just to give more information, whenever I try
normal form "rev (a # b # c # [])"
It says that "Command is not state preserving, I won't execute it!"
Thanks,
Beta
Email Gateway (Aug 18 2022 at 11:59):From: Beta Ziliani <beta.ziliani@gmail.com>
I think I know what the problem is: I have to specify Isabelle which buffer
to use. That was not on the tutorial...
Now I have another problem: When I use the buffer with the ToyList, it
complains saying that
*** Outer syntax error: keyword "=" expected,
*** but identifier a was found
And the text
theory ToyList
imports PreList
begin
is marked. But now mi context IS theory ToyList. And still nothing works:
value "rev (True # False # [])"
throws
*** Inner lexical error at: "# False # [])"
*** At command "value".
like it didn't parse the theory.
What I'm doing wrong???? :'(
Thanks again,
Beta
Email Gateway (Aug 18 2022 at 11:59):From: Beta Ziliani <beta.ziliani@gmail.com>
Quick response! Thank you very much!
The thing is, I have in the buffer the hole theory, not only the part i put
in the mail. What I show was the part of the text marked by the error thrown
by Isabelle.
I think Proof General is driving me crazy, I will try to understand a little
bit more on what's happening, and use the command line. I don't understand
how to execute or see the result of nothing. I give up! Or the tutorial is
incomplete, or it assume some knowledge (and dough is not a tutorial), or
I'm a complete idiot, which is not something we can discard...
Beta
Last updated: May 03 2024 at 12:27 UTC