Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar



On Mon, 3 Aug 2015, Lars Hupel wrote:

I'm currently working on some Isabelle/ML code which produces a bunch of
datatype specifications, ultimately calling
'BNF_FP_Def_Sugar.co_datatypes' for all of them. This generally works
fine, but there appears to be some corner case. I've attached a minimal
failing example. Loading this with Isabelle2015 gives the following error
message related to the declaration of the second data type:

 Undeclared hyps:
   size_String0 ≡ size_String0
 The error(s) above occurred for the goal statement⌂:
 map_pre_Rational0 id = id

(and some more along the same lines)

If I put a call to 'Local_Theory.restore' in between, the error
disappears. (Not that I have any idea why.)

Local_Theory.restore essentially introduces a command-transaction boundary, so the two invocations in ML behave like two Isar commands within a theory file. I can't explain the deeper reason of the problem seen here -- there might be something wrong with the context-discipline of the BNF implementation, which is rather complex.

Dmitriy Traytel has recently updated that for the coming release, see http://isabelle.in.tum.de/repos/isabelle/rev/7b915ca69af1

The motivation for that change was to allow the name space management of Isabelle2015 via "context begin private/qualified ... end" work for (co)datatype definitions as well, although a few more changes in the repository were required to get it into proper shape (e.g. 2618e7e3b5ea).

As it happens, these changes also make the problems exposed in the example disappear. This might be an accident, though, and the true reasons for the breakdown still lingering in the dark.


For now I recommend to keep the Local_Theory.restore workaround and try again when the first release candidates for Isabelle2016 emerge, presumably at the start of the year 2016.


	Makarius





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