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

Makarius makarius at sketis.net
Fri Jun 1 23:32:12 CEST 2018

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
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
more checks for global facts: disallow undeclared frees (as in

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.


More information about the isabelle-dev mailing list