Re: [isabelle] yet another simplifier question



In such situations, you should try simplifying with

  apply (simp add: algebra_simps)

It works in your example. Sledgehammer also solves your problem.

There are many other useful packages of rules for such situations, including field_simps and divide_simps.

To be quite honest, I never try to trace the simplifier. The output is simply too massive. I just try something else.

Larry Paulson


> On 5 Nov 2016, at 01:47, noam neer <noamneer at gmail.com> wrote:
> 
> 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 ?
> 




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