# Re: [isabelle] Pairs/tuples

```Hi,

Thanks for that. But if I have

axiomatization
lst :: "nat*nat*nat"
where ax : "lst = (1,2,3)"

lemma "snd (snd lst) = 3"
using ax
apply simp

```
doesn't seem to prove it. I guess I need some form of a substitution so that (1,2,3) is substituted into lst?
```
Thanks
Steve

On Mar 31, 2011 4:20pm, Christian Sternagel <c.sternagel at gmail.com> wrote:
```
```Hi,
```
```

```
there are only pairs in Isabelle and the pair constructor * is right-associative. Hence when you write
```

```
```nat * nat * nat
```
```

```
```it really is
```
```

```
```nat * (nat * nat)
```
```

```
and a corresponding value would be (1, (2, 3)) (again you can save parentheses by writing (1, 2, 3) instead). Thus getting the third element is done by nested calls to snd, eg,
```

```
```lemma "snd (snd (1, (2, 3))) = 3" by simp
```
```

```
You see that I do not need a sledgehammer to prove the fact ;). Mere rewriting is enough. The same is true for your initial lemma
```

```
```lemma "snd (snd ([(1, 2, 3)] ! 0)) = 3" by simp
```
```

```
```hope this helps
```
```

```
```chris
```
```

```
```On 03/31/2011 04:42 PM, Steve W wrote:
```
```

```
```Greetings,
```
```

```
```I'm currently experimenting with pairs/tuples, like the following:
```
```

```
```axiomatization
```
```
```
```lst :: "((nat*nat)*nat) list"
```
```
```
```where ax : "lst = [((1,2),3)]"
```
```

```
```lemma "snd (lst ! 0) = (3::nat)"
```
```
```
```using ax
```
```
```
```sledgehammer
```
```

```
Does anyone know how I can prove that lemma since sledgehammer can't seem to
```
```
```find a proof?
```
```

```
```Also, if lst was of type "(nat * nat * nat) list", then how do I read the
```
```
```
```3rd element from a tuple?
```
```

```
```TIA
```
```

```
```Steve
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.