*To*: "C. Diekmann" <diekmann at in.tum.de>*Subject*: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 22 Mar 2013 08:39:47 +0100*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAGbqCMwbsBO6Gd6rp2nXe8S1i1mraZ8AjHC=38Cn-j_FufH-hA@mail.gmail.com>*References*: <CAGbqCMwbsBO6Gd6rp2nXe8S1i1mraZ8AjHC=38Cn-j_FufH-hA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130308 Thunderbird/17.0.4

Dear Cornelius,

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

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

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- Next by Date: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- Previous by Thread: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- 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