Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Attributes for unnamed facts in obtains

Email Gateway (Aug 18 2022 at 15:37):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,

the Isar command obtains works without "where" when only facts, but no
new variables are obtained, although I have not found a proper syntax
documentation for that in the Isabelle/Iar reference manual.

The following three examples work as expected:

from A & B obtain foo [intro]: "A" and bar [simp]: "B" by(rule conjE)
from A & B obtain foo: "A" and [simp]: "B" by(rule conjE)
from A & B obtain [intro]: "A" and "B" by(rule conjE)
from A & B obtain [intro]: "A" and [simp]: "B" by(rule conjE)
from A & B obtain "A" and "" [simp]: "B" by(rule conjE)

However, if the first fact is unnamed and without attributes, and only
an attribute is given for the second fact (like in the next example),
the parser produces a syntax error:

from A & B obtain "A" and [simp]: "B" by(rule conjE)

*** Outer syntax error: name declaration expected,
*** but keyword [ was found

Is there any specific reason for this?

Best regards,
Andreas

Last updated: Apr 26 2024 at 12:28 UTC