Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 10:22):

From: Peter Lammich <lammich@in.tum.de>
Hi list,

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?

If the latter is the case:
FEATURE REQUEST: Dummy patterns with "of" and "where"!

Best,
Peter

==============================================
Example:

theory Scratch
imports Main
begin
thm imp_refl[of "undefined _ _"] (* Duplicate fixed variable(s):
"uu_" *)
context begin
thm imp_refl[of "undefined _ _"] (* Duplicate fixed variable(s):
"uu_" *)
end

notepad begin
thm imp_refl[of "undefined _ _"] (* undefined ?uu5 ?uua5 ⟶
undefined ?uu5 ?uua5 *)
end

Email Gateway (Aug 22 2022 at 10:22):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 10:23):

From: Peter Lammich <lammich@in.tum.de>
Just for documentation: The (obvious) workaround is to write
thm imp_refl[of "undefined a b" for a b]

Last updated: Apr 20 2024 at 08:16 UTC