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