Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Very counterintuitive set notation for tuples...

Email Gateway (Aug 19 2022 at 10:34):

From: "C. Diekmann" <diekmann@in.tum.de>
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

Last updated: Apr 19 2024 at 12:27 UTC