# Re: [isabelle] Why can't auto prove that goal: f (x+(y+z)) = f ((x+y)+z)

On Tue, Aug 31, 2010 at 9:32 AM, Peter Lammich
<peter.lammich at uni-muenster.de> wrote:
> Recently, auto left me a goal of the form
> f (x+(y+z)) = f ((x+y)+z)
> x,y,z :: nat
>
> I always thought the simplifier would rewrite the right sum automatically.
> However, when searching for the corresponding theorem, I cannot find it:
>
> find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
>
> searched for:
>
> "_ + (_ + _) = _ + _ + _"
>
> nothing found in 0.111 secs
>
> What's going on here, how is associativity of + on nats implemented?
Hi Peter,
You didn't find the theorem "add_assoc" because it is oriented the other way:
"(x + y) + z = x + (y + z)"
As far as I know, all associativity theorems (for multiplication,
etc.) in the main libraries are oriented like this.
> btw: I now prove this goal by (rule arg_cong, simp) or by adding "intro:
> arg_cong" to auto's arguments,
> but I would have much more liked to write: "simp add: add_a" or something
Try "simp add: add_ac", which will rewrite additions to a normal form,
with terms in sorted order and additions grouped to the right.
- Brian

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