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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
