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

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?

`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 like this
`
Best, Peter

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