[isabelle-dev] Safe approach to hypothesis substitution
schropp at in.tum.de
Wed Aug 25 13:28:42 CEST 2010
On 08/25/2010 07:57 AM, Thomas Sewell wrote:
> It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines.
Sorry for that. ^^
> I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem.
Well as you said
There's no truly safe way to delete an equality on a Free variable without inspecting the whole context.
> To answer Andreas' question about blast_hyp_subst_tac:
> I made some attempts, but it seemed that making blast_hyp_subst_tac share behaviour or even code with the other versions led to incompatibilities I didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly in compatibility mode with previous behaviour.
> I think you've outlined why there was a problem - blast is guessing incorrectly what the tactic will do. Perhaps in the future the Hypsubst ML structure could export its eq_var and triv_asm term inspection functions so blast would have a better idea what it would do (assuming blast can construct accurately what the subgoal passed would be).
Blast has a different term structure with Skolems replacing
Goal-Parameters etc. In the current architecture
there seems to be no easy way to get a subgoal of the search back as an
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev