# [isabelle] yet another simplifier question

hi everybody.
I'm interested in what exactly happens in the following proof -
theory tmp
imports Complex_Main
begin
lemma "sin((x::real) + y + x) = sin(2*x + y)"
using [[simp_trace=true]]
by simp
end
the proof succeeds, and because of the sin() I guess it can't be due to
linarith.
so I guess there is a true rewriting process here, but I failed to
understand
from the output what exactly happens and how the following expression
appeared
in the process -
(Numeral1 / Numeral1 + Numeral1 / Numeral1) * (x / 1) + y = 2 /
Numeral1 * (x / 1) + (y + 0)
where did all the numerals come from? I expect a rewriting process to
remove things
like Numerla1, not add them.
thanx, Noam

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