[isabelle-dev] Odd failure to match local statement with pending goal.

[Alexander Krauss]

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 
nicely.

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.

Alex
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Odd_Failure.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110803/c83350a9/attachment-0002.ksh>