Re: [isabelle] yet another simplifier question

On 04/11/2016 04:53, noam neer wrote:
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)

This is a step in the process that rewrites x+y+x to 2*x+y. As it says in the trace:

Procedure "Numeral_Simprocs.field_combine_numerals" produced rewrite rule:
x + y + x â 2 * x + y

In the next step in the trace, the goal is solved by reflexivity.

Numeral1 is introduced locally by the proof method that combines summands.


where did all the numerals come from? I expect a rewriting process to
remove things
like Numerla1, not add them.

thanx, Noam

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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