# Re: [isabelle] Pairs/tuples

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, e.g.,
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.*