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 <[email protected]> > Date: 28 July 2011 14:36:19 GMT+01:00 > To: Bertram Felgenhauer <[email protected]> > Cc: [email protected] > 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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
