Re: [isabelle] Pairs/tuples



Thanks for the replies. After some more experiments, it seems that if one of
the elements in the tuple has a variable type, then it's not so trivial. For
example:

axiomatization
lst :: "'a*nat*nat"

axioms
ax : "lst = (1,2,3)"

lemma "snd (snd lst) = 3"
apply (simp add: ax)

doesn't find a proof. How come changing the type of an element could make
such a difference?

TIA

Steve

On Fri, Apr 1, 2011 at 8:22 AM, Lars Noschinski <noschinl at in.tum.de> wrote:

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