[isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken
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"
This is ultimately a problem of the class target in conjunction with the
unnamed local context. See now
date: Fri Jun 01 22:01:43 2018 +0200
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:
date: Sun May 20 22:37:00 2018 +0200
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