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