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