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

[Thomas Sewell]

Veterans of this list will recall that some years ago we had a discussion about the "hypsubst" mechanism implemented in "~~/src/Provers/hypsubst.ML" and included by default in many Isabelle tools (safe, clarify, clarsimp, auto, etc).

A number of people have reported to me recently that they're interested in resolving this issue, so I'm going to restart the discussion. I'm currently posting to isabelle-dev, though at some point it might make sense to ask all users whether they're willing to deal with the fallout from the change.

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 proposed a change to hypsubst.ML a couple of years ago. I've reimplemented it recently, this time making an effort to keep the code readable.

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.

I include the patch to hypsubst and to core HOL, as of 2013-1. I also include a patch that fixes most of the sessions built by "isabelle build -a" within HOL.

The change requires, for instance, about a dozen lines of changes to the files in HOL/Library, which contain about 50K lines of proof, or 3 lines of changes to HOL/Bali, with 30K. The change to the Nominal examples (30K), however, is a bit longer (100 changes) and a bit more unpleasant. I've also checked the change against one chunk of L4.verified, with 70K lines in it, and have around 60 lines of changes to make. From my perspective, this level of impact seems to be annoying but not too annoying. I'm interested in what others think.

I'm still only two thirds of the way through my changes, I think, and currently these sessions still fail:
HOL-MicroJava FAILED
HOL-Old_Number_Theory FAILED
HOL-Probability FAILED
HOL-Quotient_Examples FAILED
HOL-SET_Protocol FAILED
HOL-UNITY FAILED
HOLCF-FOCUS FAILED
HOLCF-Library FAILED
HOLCF-ex FAILED
ZF-Coind FAILED
ZF-Induct FAILED
ZF-UNITY FAILED
ZF-ex FAILED

If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though.

All comments welcome,
     Thomas.


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hypsubst.diff
Type: text/x-patch
Size: 11035 bytes
Desc: hypsubst.diff
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140113/30e40766/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hypsubst-HOL-sessions.diff
Type: text/x-patch
Size: 38184 bytes
Desc: hypsubst-HOL-sessions.diff
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140113/30e40766/attachment-0003.bin>