Re: [isabelle] yet another simplifier question
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)"
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 ?
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
>> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and