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

[Lawrence Paulson]

Some sort of visual indication that the same variable is being bound twice might be useful, though that sort of thing is easy to overlook.
Larry

On 22 Mar 2013, at 13:15, Tjark Weber <webertj at in.tum.de> wrote:

> 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
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev