[isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Dmitriy Traytel]

Hi Makarius,

> On 1 Jun 2018, at 23:32, Makarius <makarius at sketis.net> wrote:
> 
> On 01/06/18 10:35, Dmitriy Traytel wrote:
>> Hi all,
>> 
>> thanks for pointing this out, Lars. And thanks for looking at the sources, Jasmin.
>> 
>> The problem seems to only show up when the declaration in question is inside of a class context. Here is a reduced version that does not involve primrec at all.
>> 
>> context linorder begin
>> 
>> context fixes b :: nat begin
>> 
>> definition c where "c = b"
>> 
>> end
>> 
>> end
> 
> This is ultimately a problem of the class target in conjunction with the
> unnamed local context. See now
> 
> changeset:   68351:bcdc4c21ab1d
> tag:         tip
> user:        wenzelm
> date:        Fri Jun 01 22:01:43 2018 +0200
> files:       src/Pure/Isar/class.ML
> description:
> varify frees, notably dangling_params (see also e0cd57aeb60c);

Happy to see that this was not a problem in our codebase.


>> @Makarius: What is the rationale behind disallowing the definition of c?
> 
> The changeset explains it as follows:
> 
> changeset:   68239:e0cd57aeb60c
> user:        wenzelm
> date:        Sun May 20 22:37:00 2018 +0200
> files:       src/Pure/global_theory.ML
> description:
> more checks for global facts: disallow undeclared frees (as in
> Export_Theory.export_fact);
> 
> 
> At first I did not want to expose odd mixtures of free vs. schematic
> variables to the world out there, and for global items we have a clear
> understanding that fixed vs. schematic can always be flipped via
> Logic.varify_global/unvarify_global and related operations.
> 
> Moreover, the check was meant to tighten existing tools and local theory
> targets, as we have seen here. In the process, I had to give up the full
> rigour, though: a3bd410db5b2 allows mixed variable indexes.
> 
> 
> Looking even more closely at global facts, there might be further
> problems that are still undetected. In the next round I will experiment
> with Thm.plain_prop_of to see if we can disallow hyps, shyps, tpairs.

Thanks for the explanation. The context handling in the BNF packages has quite improved over the years thanks to the additional checks you introduce every now and then. Do not hesitate to tell us should you encounter further problems.

Dmitriy



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180602/966800a3/attachment-0002.html>