Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar



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
in Isabelle/ML?

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.


	Makarius




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