Re: [isabelle] of/where with dummy-patterns



On Fri, 26 Jun 2015, Peter Lammich wrote:

more or less intuitively, I used the of-attribute with dummy-patterns,
e.g.
 thm imp_refl[of "undefined _ _"]

inside a proof, this works fine. However, outside a proof, I get the
error message
 Duplicate fixed variable(s): "uu_"

The same behaviour for "where".

Is the of-attribute supposed to work with dummy-patterns or
do they only work by accident within proofs?

It is official since Isabelle2015, see NEWS:

* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.


The breakdown above indicates that I've got the context policy wrong for the "eigen context" of dummy variables. I need to revisit the whole complex again for the next release anyway: the main point is to have instantiations work properly in Eisbach, and we are only half-way through with that.

Right now it works outside a proof body for at most one dummy variable. In any case the result will be a bit ugly: some derivative of "uu".


	Makarius




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