[isabelle-dev] Safe approach to hypothesis substitution mark II
makarius at sketis.net
Mon Jan 13 16:55:49 CET 2014
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.
More information about the isabelle-dev