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

Tjark Weber webertj at in.tum.de
Mon Jan 13 13:50:01 CET 2014

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?


More information about the isabelle-dev mailing list