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.)
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
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)"
lemma "(\<exists>z. P z) \<and> (\<exists>z. Q z)"
apply (rule R1)
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
lemma R2: "P y ==> x = y ==> \<exists>x. P x"
lemma "\<exists>y. P y"
apply (rule R2)
I have now introduced a check that filters out such problematic renamings.
This archive was generated by a fusion of
Pipermail (Mailman edition) and