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

[Makarius]

On Mon, 13 Jan 2014, 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.

> Here's what's changed:
>  1) the new behaviour is to keep hypotheses of the form "x = Suc a"
>     where x is free, and to reorient equalities of the form "Suc a = x"
>     (to "x = Suc a", which is kept). Equalities on bound variables are
>     still removed immediately.
>  2) when any action is taken (substitution or reorientation) and a
>     hypothesis kept, it is moved to last place amongst the hypotheses in
>     the goal. This is different to my previous proposed patch. I suspect
>     it might reduce the number of times the new hypotheses are picked by
>     erule or similar in old scripts. I do not yet have any empirical
>     evidence this helps.
>  3) the old behaviour is provided via new method hypsubst_thin and
>     Hypsubst.hyp_subst_tac_thin in ML. The setting [[ hypsubst_thin =
>     true ]] also restores the old behaviour, and can be used to repair
>     otherwise unrepairable proofs.Some of these features might need a
>     better name.

This sounds quite reasonable to me, although I am not a proven expert of 
hypsubst.  Whenever I had a question about it in the past, I would first 
consult Stefan Berghofer.

As I've already pointed out in the discussion some years ago, the "proof 
of correctness" of such a change works empirically, against the body of 
existing applications in the Isabelle repository and AFP.  You have also 
access to classified L4.verified material, and might take big external 
projects like IsaFoR into account.

The changes so far appear to be below the level of significance -- we've 
had much more substantial upheavals in the past.

With an easy escape, i.e. the alternate name of the proof method and a 
confifuration option to recover the old behaviour, users should manage to 
convert their old stuff reasonably well.


 	Makarius