[isabelle] yet another simplifier question

hi everybody.
I'm interested in what exactly happens in the following proof -

    theory tmp
    imports Complex_Main
        lemma "sin((x::real) + y + x) = sin(2*x + y)"
        using [[simp_trace=true]]
        by simp

the proof succeeds, and because of the sin() I guess it can't be due to
so I guess there is a true rewriting process here, but I failed to
from the output what exactly happens and how the following expression
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.