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
    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)

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.

Tobias

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.