*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] yet another simplifier question*From*: noam neer <noamneer at gmail.com>*Date*: Sat, 5 Nov 2016 03:47:19 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a0ba4baa-8d66-ce82-9092-e992ff31ea26@in.tum.de>*References*: <CAGOKs0_QVcuM1gVkD3kt3wnpSONdP-vFFzO+qcaA6MjDAH4Z9g@mail.gmail.com> <a0ba4baa-8d66-ce82-9092-e992ff31ea26@in.tum.de>

first I must admit I didn't know the simplifier can do things to sub expressions besides application of identities. good to know that. second, is there a documentation of what "field_combine_numerals" can and can't do? for example to my surprise the following fails (and this was the trigger to the original question) - lemma "sin((x::real) + y + x + y) = sin(2*x + 2*y)" using [[simp_trace=true]] by simp (* doesn't work *) also, I must say that the simplifier's output is very hard to read. it would have been much easier to understand it if there was some identation, and if there was some declaration where the output of a simproc begins (I assume much of the output before the produced rewrite rule also came from the simproc.) can we request this for the next Isabelle revision ? many thanks, Noam On Fri, Nov 4, 2016 at 8:48 AM, Tobias Nipkow <nipkow at in.tum.de> wrote: > 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 >> >> >

**Follow-Ups**:**Re: [isabelle] yet another simplifier question***From:*Lawrence Paulson

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

**Re: [isabelle] yet another simplifier question***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] cvc4 crashing
- Next by Date: Re: [isabelle] Isabelle2016-1-RC1: Printing of literal newline characters in Scala code is wrong
- Previous by Thread: Re: [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