Re: [isabelle] My unforgivable soundness issue with a locale



I was wrong, Isar‑Ref disallows it. Printed page 89 it says:

    “Note that "(is p 1 . . . p n )" patterns given in the syntax of
     assumes and defines above are illegal in locale definitions.”


Le Mon, 23 Dec 2013 23:09:57 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:

Le Mon, 23 Dec 2013 12:19:43 +0100, Johannes Hölzl <hoelzl at in.tum.de> a écrit:

Am Sonntag, den 22.12.2013, 18:51 +0100 schrieb Yannick Duchêne
(Hibou57):
By the way, a question aside: is there a way to refer to a proposition
from another proposition? I mean so that I would not have to copy/paste
the premiss of “(text of B) ⟹ (text of A)” and just refer to B, as “B ⟹
(text of A)” instead of the latter.

I'm not sure for the locale syntax, but when writing lemmas you an
use ?X patterns:

lemma assumes "B" (is ?B) shows "?B ==> A"
  ...

 - Johannes

Hello Johannes,

I already tried this one. It seems to be allowed by Isar‑Ref, but Isabelle reject it with this message: “Illegal term bindings in context element”.



--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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