*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] yet another simplifier question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 4 Nov 2016 07:48:48 +0100*In-reply-to*: <CAGOKs0_QVcuM1gVkD3kt3wnpSONdP-vFFzO+qcaA6MjDAH4Z9g@mail.gmail.com>*References*: <CAGOKs0_QVcuM1gVkD3kt3wnpSONdP-vFFzO+qcaA6MjDAH4Z9g@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

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

**Follow-Ups**:**Re: [isabelle] yet another simplifier question***From:*noam neer

**References**:**[isabelle] yet another simplifier question***From:*noam neer

- Previous by Date: [isabelle] yet another simplifier question
- Next by Date: [isabelle] Method setup with arguments
- Previous by Thread: [isabelle] yet another simplifier question
- Next by Thread: Re: [isabelle] yet another simplifier question
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list