Re: [isabelle] Odd failure to match local statement with pending goal.



Bertram Felgenhauer wrote:
> So do we know whether this is an obscure feature or possibly a bug?
> (If it's a feature I'd love to hear the underlying story.)

Hi,

this problem has now been fixed in the repository version of Isabelle (476a239d3e0e).
It was caused by some rather old code in Isabelle's theorem module that renamed
"all bound variables and some unknowns" in a rule during resolution, in order to preserve
as many of the variable names in the goal as possible. For example, when resolving the rule

  ?P ?x ==> \<exists>x. P x

with the proof state

  \<exists>foo. P foo

this will result in the new proof state

  ?P ?foo

because the schematic variable ?x in the rule has been renamed to match that of the
bound variable foo in the goal.
Unfortunately, such a renaming of schematic variables can cause two kinds of name clashes,
neither of which were detected by the old code:

1. If two bound variables in the goal happen to have the same name, this may cause
   two schematic variables in the rule to be mapped to the same variable:

   lemma R1: "P x ==> Q y ==> (\<exists>x. P x) \<and> (\<exists>y. Q y)"
     by auto

   lemma "(\<exists>z. P z) \<and> (\<exists>z. Q z)"
     apply (rule R1)
     oops

2. If a bound variable in the goal happens to have the same name as a schematic variable
   in the rule, it may clash with another schematic variable in the rule after the
   renaming.

   lemma R2: "P y ==> x = y ==> \<exists>x. P x"
     by auto

   lemma "\<exists>y. P y"
     apply (rule R2)
     oops

I have now introduced a check that filters out such problematic renamings.

Greetings,
Stefan






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.