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

[Tjark Weber]

On Mon, 2014-01-13 at 12:38 +0000, Thomas Sewell wrote:
> Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a
> free (blue) variable, hypsubst will substitute "Suc a" for x throughout
> the goal, and then discard the hypothesis. The substitution is almost
> always wanted. Discarding the hypothesis may, however, be unsafe, since
> there may be facts about x at the proof or locale level that now cannot
> be used. It may also be unsafe in the subtle case where a schematic
> variable in the goal can be instantiated to functions of x but not of
> "Suc a". This unsafeness is undesirable because hypsubst is called from
> tactics that are meant to be safe.

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?

Best,
Tjark