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

[Makarius]

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);


> @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.


	Makarius