*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Fri, 22 Mar 2013 16:38:28 +0900*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/20130311 Thunderbird/17.0.4

Dear Cornelius, you see already in the output of, e.g., term "{(v, v). v : {''a'', ''b''}}"

cheers chris On 03/22/2013 04:15 PM, 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

**References**:

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