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.
Ahh, ok.
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 isabelle subgoal.
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
