[isabelle-dev] [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning

Tjark Weber webertj at in.tum.de
Fri Mar 22 14:15:55 CET 2013

On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
> On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
> > "{(x, y). P}" is pretty syntax for
> > "Collect (prod_case (%x y. P))", so in your case, you get
> > "Collect (prod_case (%v v. v : {''a'', ''b''}))"
> > See how the second v in %v v. ... hides the former.
> >
> > There is no warning because it is perfectly normal to rebind a variable 
> > name in a lambda abstraction.
> I agree that it is perfectly normal, just like term "λx x x. x", and no 
> warning or error is to be expected.

Clearly, different people have different expectations. "{(v,v). P v}"
is not a lambda abstraction (regardless of how it is represented
internally). But it is similar to established mathematical notation, so
users might (and, as this thread again shows, do) expect it to denote
some subset of the identity relation. See also


More information about the isabelle-dev mailing list