Re: [isabelle] Pairs/tuples



On 31.03.2011 17:50, s.wong.731 at gmail.com wrote:
> axiomatization
> lst :: "nat*nat*nat"
> where ax : "lst = (1,2,3)"
>
> lemma "snd (snd lst) = 3"
apply (simp add: ax)

works

> 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?

When looking at the simplifier trace, i.e.

using ax
using [[simp_trace]]
apply simp

one can see that the simplifier tries to uses the rule "(1,2,3) = lst" instead of "lst = (1,2,3)" here, so it fails. The simplifier re-orients rules in certain cases to prevent looping, but it is not entirely clear to me why it reorients here.

  -- Lars





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