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


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?


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