Re: [isabelle] Curious failure of simp when goal equation is reoriented



On Tuesday 04 February, 2014 at 12:56 pm, Tobias Nipkow wrote:
> > I've been playing with the list theory from the Isabelle tutorial and
> > bumped into something odd. After defining rev and app, and giving a
> > couple of simplification rules, I can prove the following lemma with
> > induct and simp:
> >    lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
> > But not this one:
> >    lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
> > 
> > This seems rather strange to me, because all I've done is flipped the
> > equation around. I can understand that reorienting a simplification
> > rule will affect the behaviour of simp, but why does reorienting the
> > goal make a difference?
> 
> Because you are doing an induction, and the IH is your original goal, and the IH
> is used as a rewrite rule in your proof.

Thanks for the replies, all. That makes perfect sense now - it's the
orientation of the induction hypothesis that makes the difference.

Nick




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