[isabelle] Pairs/tuples



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.