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

Dear Cornelius,

you see already in the output of, e.g.,

    term "{(v, v). v : {''a'', ''b''}}"

that the non-linear pattern "(v, v)" is "not accepted" (or rather implicitly translated into a linear one).

Currently, for set-comprehension, a syntax translation is specified (in Set.thy), which is conceptually very simple and reuses the "pttrn" token category. "pttrn" is initially equivalent to plain identifiers and only later extended, e.g., in Product_Type.thy to allow pairs.

It might be possible to incorporate error messages in the setup in Product_Type.thy. But as you will see there, even the current "simple" setup is rather involved.



On 03/22/2013 04:15 PM, C. Diekmann wrote:

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.