Qiyuan Xu (Nov 24 2022 at 13:26): Qiyuan Xu (Nov 24 2022 at 13:26):Sorry for the interruption... Guys, I solved this problem.
It is about the 'sort' of keywords. I quote-marked the sort because I don't know the formal name of those "prf_open % proof". I didn't find any documentation about this...
In my work,
Wrong:
theory Thy
keywords "❴" "❵" :: prf_decl % "proof"
Correct:
theory Thy
keywords "❴" :: prf_open % "proof"
and "❵" :: prf_goal % "proof"
The place where my code goes wrong:
lemma "...."
❴
...
❵
. (* here it goes wrong! *)
Command "❵" is some magic defined by myself, and I didn't know what the keyword sort does. So I mimicked other commands and wrote "prf_decl % proof". It works in the interactive mode, but it seems the batch mode checks more about the outer syntax of Isar. The thing is the command "❵" generates some proof obligations and the usage in my theory is like ❵ by methods. ❵ changes from the proof mode (forward) to the backward mode. Keyword sort "prf_decl % proof" is not for appending a proof scripts like this, so it fails in the syntax check and Isar tells me the command "." (corresponding to "by methods" here) is at the wrong place. After I corrected the sort to be prf_goal % "proof" which is expected to be followed by a proof script. The syntax check is passed and then everything works.
Again... I really hope for more documentation about the system. Isabelle/Isar is really great art and a complicated video game... I really enjoy it! again!
Notification Bot (Nov 24 2022 at 13:26):Qiyuan Xu has marked this topic as resolved.
Last updated: Dec 30 2024 at 16:22 UTC