Let's try to answer everyone again:

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.

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.


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.
Isabelle-dev mailing list

Reply via email to