# 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.*