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

[Makarius]

On Fri, 22 Mar 2013, Tjark Weber wrote:

>> 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).

So how about "λ(v. v). v" then?

Anyway, when I've got exposed to this slightly sugared lambda-calculus in 
Isabelle for the first time in 1993, I found its simplicity and uniformity 
a great relieve, compared to all these adhoc explanations about binders in 
informal mathematics. You merely need to learn very few priniciples, and 
then you know how it works.  Of course, you need to develop a sense what a 
binding occurrence of a variable is.

Color schemes in the editor can help to teach people what these principles 
of binding and scoping are.  In the 1990-ies, black, blue, green variables 
were a big thing.  Today, it is just a tiny little step to visualize scope 
groups in Isabelle/jEdit in a similar way you ee in Netbeans etc. for 
Java. (You can already following the implicit hyperlinks in Isabelle2013.)


> 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

So I won't have to recycle the old jokes again -- its all there on the 
thread from 1 year ago.


 	Makarius