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

[Tjark Weber]

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
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html

Best,
Tjark