[isabelle-dev] Global constant names in inductive
makarius at sketis.net
Thu Apr 6 16:32:42 CEST 2017
On 06/04/17 13:08, Lars Hupel wrote:
>> Did you encounter an actual problem from that situation?
>> Formally, a comment is not a problem. "Fixing" such things prematurely
>> is likely to break it.
> Yes, there is an actual problem. I define a function via
> "Function.add_function" and inspect the resulting info. As per usual
> discipline this looks as follows:
> That is, I inspect the relation as generated by the function package.
> The termination proof needs to get some information about that relation
> from the inductive package. However, "#R" is a term, not a const name
> string. Before I close the target, it will be a free variable.
OK, that is a better motivation.
Your proposed change
My old comment from 10-years ago stems from:
date: Sat Nov 10 18:36:08 2007 +0100
put_inductives: be permissive about multiple versions
(target names are not necessarily unique);
add_inductive: store info under global (!) name -- very rough
approximation of the real thing;
That historical context is important. Isabelle development means to
study sources + history carefully and to make empiric explorations
against current applications (notably AFP).
The date above reminds me of chaotic times in 2006/2007 when far too
many things were changed without clear principles.
More information about the isabelle-dev