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

Lawrence Paulson lp15 at cam.ac.uk
Fri Mar 22 15:32:51 CET 2013

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.

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

More information about the isabelle-dev mailing list