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

[Makarius]

On Mon, 13 Jan 2014, Lawrence Paulson wrote:

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

Indeed.  The proposed change is basically some form of "localization" of 
hypsubst, in the sense that it does not make implicit assumptions how free 
variables got introduced, their scope etc.  In ancient times, a Free was 
fixed in the immediate scape of the goal state, but that is long past.


> the current treatment of contexts may make this information available 
> after all.

That is a very old topic, and there are various ideas in some drawer that 
have accumulated a lot of dust.  It could easily take a few more years to 
revisit that.  It somehow belongs to the national debts problem from 2006.

Since December 2013, I am again improving the situation concerning the 
formal proof context within proof tools, notably the Simplifier and its 
add-ons.  It is always surprising how long really tiny steps take, e.g. 
see current Isabelle/f26a7f06266d.


 	Makarius