Re: [isabelle] [symmetric]-attribute changes variable names



On Mon, Nov 26, 2012 at 1:51 AM, Peter Lammich <lammich at in.tum.de> wrote:
> I recently stumbled over the following quite confusing behaviour:
>
> definition "foo x \<equiv> x"
> thm foo_def[symmetric]
>   > Outputs ?y = foo ?y

It looks like this only happens for definitions whose right-hand side
is just a variable. Also, note that this behavior is not due to the
"symmetric" attribute per se; it really starts with Thm.biresolution.
"thm foo_def [THEN symmetric]" yields the same result.

Here's what I think is happening: When you resolve two theorems like
"rule1 [THEN rule2]", and two variable patterns are unified, the
result takes the variable name from rule2.

This seems like a sensible design for Thm.biresolution, because it is
used most often to apply rules during a proof; here rule2 corresponds
to the goal state, and rule1 is the applied rule. It makes sense to
preserve the names of schematic variables during a proof.

- Brian





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