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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev