[isabelle-dev] Odd failure to match local statement with pending goal.
krauss at in.tum.de
Wed Aug 3 23:12:26 CEST 2011
On 08/03/2011 12:34 PM, Lawrence Paulson wrote:
> Many thanks for your analysis. It looks like an interaction involving "fix" and bound variables.
Not too fast :-)
We must now peel off the various layers of Isar (recall that "show" is
just a normal refinement step), to get closer to the problem. The
attached theory exposes the same issue in a bare-bones HOL, using plain
rule application. Note that after the "apply (rule R)", the two
arguments of P have been "over-unified", which makes the following
assumption step fail. Using the alpha-equivalent rule R2, the same works
The same can be done in low-level ML, using just "rtac", which suggests
that the error is somewhere in the underlying Thm.biresolution etc. So
far, I have not looked any further...
I could reproduce the same behaviour in Isabelle 2005, so the issue has
been around for a while... possibly much longer.
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev