*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Fri, 22 Mar 2013 08:15:04 +0100*Sender*: c.diekmann at googlemail.com

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

**Follow-Ups**:**Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning***From:*Christian Sternagel

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

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

- Previous by Date: Re: [isabelle] union-find based unification
- Next by Date: Re: [isabelle] union-find based unification
- Previous by Thread: Re: [isabelle] union-find based unification
- Next by Thread: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list