[isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

Let's try to answer everyone again:

Alex:
I think I was wrong about the cases involving algebra. There may be something interesting going on. The prenormalisation phase calls clarify_tac, then full_atomize_tac, then some other stuff. With a Free variable x assumed to be even, the resulting goals with the old and new versions of hypsubst are of the form "ALL k. P (2 * k)" and "ALL k. x = 2 * k --> P (2 * k)". It's possible that the quantifier elimination process that follows doesn't know what to do with the additional implication, or maybe just its left hand side.

If the same problem occurs for more interesting examples, it could be fixed by following clarify_tac with Hypsubst.thin_triv_tac in groebner.ML.

Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen.

Makarius:
Indeed bounds, frees and consts can all be seen as the same kind of thing. At the moment the only real benefits of hyp_subst over asm_full_simp are robustness in the case of Vars and the capacity to reorient equations in order to rewrite bounds -> frees -> expressions. Adjusting this to rewrite bounds -> frees -> consts -> expressions would be easy - is this what you are asking for? I don't see this as widely useful, but perhaps you have an application in mind.

Finally, the full run of "isabelle make test" is indeed quite broken, including apparently going into a loop while defining a record in Hoare_Parallel. I'll look into it.

Yours,
    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.