[isabelle-dev] Safe approach to hypothesis substitution mark II

[Lawrence Paulson]

I think the problem is that the unsafe situations cannot be detected locally, i.e., there is no way for the tactic to know that a particular free variable is actually a locale constant. I could be wrong: the current treatment of contexts may make this information available after all. That would be the best solution.

But if this contextual information is not available, then I think that some sort of compatibility mode will unfortunately be necessary, given the number of instances where introducing the safe behaviour causes proofs to fail. I have to say, in most cases these are tricky proofs that refer to specific assumptions, but lots of these still exist.

Larry

On 13 Jan 2014, at 12:50, Tjark Weber <webertj at in.tum.de> wrote:

> I will freely admit my ignorance of the issues involved, but perhaps it
> would be desirable to identify these unsafe situations in the code and
> discard the hypothesis if (and only if) doing so is safe?