Re: [isabelle] Pairs/tuples
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Pairs/tuples
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Fri, 01 Apr 2011 09:22:22 +0200
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:22.214.171.124) Gecko/20110303 Icedove/3.0.11
On 31.03.2011 17:50, s.wong.731 at gmail.com wrote:
> lst :: "nat*nat*nat"
> where ax : "lst = (1,2,3)"
> lemma "snd (snd lst) = 3"
apply (simp add: ax)
> 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and