Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning



Dear Cornelius,

You want "{(v, v) | v. v : {''a'', ''b''}}". The syntax for set comprehension is such that you should explicitly mention bound variables between "|" and ".", i.e., v in this case. In some simple cases, this can be avoided, and you ran into one of them:

"{(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.

Best,
Andreas


On 22/03/13 08:15, C. Diekmann wrote:
Hi,

I found a very counterintuitive problem with tuples in set notation.

I want to define some sort of reflexive closure.
When I write {(v, v). v ∈ {''a'', ''b''}} I hope to get {(''a'',
''a''), (''b'', ''b'')}. However, I found that
lemma "(''a'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)
and even
lemma "(''xyz'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)

With `declare[[show_types]]`, I traced the problem and found:
lemma "{(v, v). v ∈ {''a'', ''b''}} = {(x, y). y∈{''a'', ''b''}}" by simp
My set is actually translated into {(va∷'a, v∷char list). v ∈ {''a'', ''b''}}

Why does this happen?
Why wasn't there even some warning that a new variable `va` was introduced?


Regards
   Cornelius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.