[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)) = _ + _ + _"
"_ + (_ + _) = _ + _ + _"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and