Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar
- To: Lars Hupel <hupel at in.tum.de>
- Subject: Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar
- From: Makarius <makarius at sketis.net>
- Date: Mon, 7 Sep 2015 19:25:08 +0200 (CEST)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <08eef16dcbda6bd2dd5759ca3065603a-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGXFNaSFtTXQgfirstname.lastname@example.org>
- References: <226c1ffc97e4c37b33d0cab699e31954-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGXFJcSVxSWwgemail@example.com> <e83a700a3763601eb43c8d6c86c2b221-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGXFNaSFlRWA4firstname.lastname@example.org> <08eef16dcbda6bd2dd5759ca3065603a-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGXFNaSFtTXQgemail@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Wed, 12 Aug 2015, Lars Hupel wrote:
It appears that there is some difference between dealing with a finished
theory and a non-finished theory. Makarius, maybe you could shed some
light on this. Is it generally not supported to modify finished theories
After some more investigation, I think I can answer that myself: Yes,
there is a difference. If I, instead of using a finished theory directly,
first call 'Theory.begin_theory', everything works as expected.
Theory updates always need to happen within a theory body, as defined by
Theory.begin_theory ... Theory.end_theory. Under normal circumstances,
the system does that for you, so there are not many words in the
implementation manual what happens outside. That behaviour is essentially
undefined (or arbitrary).
The underlying problem in the source file I attached wasn't that the
datatype wasn't being created, but rather that it was created without
qualification. (It was just called 'String0'.)
That is an accidental effect of continuing updates after end_theory (of
the existing theory Main), which is treated like a formal "extend"
operation. Thus the naming policy is reset to a global default, without
any theory prefix yet.
There could be more explicit checks and error messages. I used to have
that on my TODO list until approx. 15 years ago, and then removed it for
lack of practical relevance -- at least at that time in the past.
This archive was generated by a fusion of
Pipermail (Mailman edition) and