[isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

As previously discussed in the thread "Safe for boolean equality", the 
current strategy for using equality hypotheses 'x = expr', in which 
substitution for x is done and then the hypothesis is discarded, is 
unsafe. The conclusion of that discussion was that the problem was 
annoying but fairly rare, that there is some concern it may become more 
common as local are used more extensively, and that fixing it would 
probably require a painful change to the behaviour of auto.

The problem is that by forgetting what x equates to in our goal, we lose 
the connection from the goal to the context outside our goal. There may 
be other facts available that name x. There may also be schematic 
variables which could be instantiated to "hd x" but not the bound 
variable replacing it.

The simple solution in my mind is to keep the equality in the goal, and 
since noone else seemed interested I thought I'd attempt to do this 
myself and see how difficult it was. I attach the resulting patch. After 
several rounds of bugfixes and compatibility improvements, it requires 
23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.

The code change in Provers/hypsubst.ML adds code for counting the free 
and bound variables in a goal, and checking whether either side of an 
equality hypothesis is a unique variable, occuring nowhere else. The 
main substitution algorithms avoid using such equalities and also 
preserve rather than delete the hypothesis they select. There is a new 
tactic for discarding these equalities, which is added as an unsafe 
wrapper in Context_Rules, allowing all unsafe tactics to behave roughly 
as before. The version of hypsubst called by blast is left unchanged, as 
blast proofs seem to be highly sensitive to changes. There is plenty of 
room for optimisation, I tried to keep the diff readable.

Three kinds of proofs seem to need fixing:
   1. proofs where subgoal_tac or similar now needs to refer to xa 
rather than x.
   2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to 
be further specialised.
   3. proofs where variables are eliminated and then induction is 
performed, i.e. the word library. Explicitly adding "apply 
hypsubst_thin" seems the best solution.

At this stage I'm not sure how to proceed. I would be very happy to see 
safe get safer, but I'm not sure how acceptable this level of 
incompatibility is in an Isabelle change. There's an alternative 
approach I thought of recently but haven't tried yet - replacing used 
equalities with meta-equalities - which might reduce the 
incompatibilities of type 2.

I haven't checked whether there are any performance implications.

I'd be keen to hear what other Isabelle developers think.

Yours,
     Thomas.


-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: hypsubst-diff
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100823/95a58b30/attachment-0002.ksh>