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

[Lawrence Paulson]

We appear to be in danger of overlooking this problem, which could indicate a significant error somewhere. The names of bound variables should not be significant. Does anybody have any idea what could be causing this?
Larry

Begin forwarded message:

> From: Lars Noschinski <noschinl at in.tum.de>
> Date: 28 July 2011 14:36:19 GMT+01:00
> To: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Subject: Re: [isabelle] Odd failure to match local statement with pending goal.
> 
> Hello all,
> 
> As Larry stated, this is indeed a strange problem. I tried to find a minimal example; here is what I came up with:
> 
> -------------------
> lemma
>  shows  "⋀c d. d ∈ Z ⟹ x = c ⟹
>        ∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}"
>  apply (unfold mem_Collect_eq)
> proof -
>  fix s t
>  assume "x = s" and "t ∈ Z"
>  then show "∃s t. t ∈ Z ∧ y = t"
>    sorry
> qed
> -------------------
> 
> The show statement fails with
> 
> >    *** Local statement will fail to refine any pending goal
> >    *** Failed attempt to solve goal by exported rule:
> >    ...
> 
> Any of the following actions will make this example succeed:
> 
> - Rename any of the two existentially bound variables in the shows
>   statement
> - Rename any of the two existentially bound variables in the show
>   statement
> - Rename any of the variables mentioned by fix
> - Remove any one of the assume statements
> - Remove the "apply (unfold ...)" and state the unfolded goal directly
> 
> This was tested on a relatively current repository version of Isabelle (last week or so).
> 
>  -- Lars
>