Re: [isabelle] Difficulties with "setsum"



> lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"
> 
> if both sides can be evaluated to the same value, you can discharge the
> goal by "eval".

Note that 'eval' does not go through the kernel and is generally
considered bad style (except for maybe exploratory purposes).

Fortunately, there's an alternative:

  lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"
  by code_simp

This sets uses the same code equations as 'eval' (as far as I know), but
goes through the kernel (by invoking the simplifier).

Cheers
Lars




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