*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] newbie questions: theory for sums and Isar syntax*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Sat, 19 Jul 2014 08:41:28 +0200*In-reply-to*: <E2B46200-81B7-4106-9CC8-405E6BACB193@fbreuer.de>*References*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de> <53C64CE6.1020402@in.tum.de> <E2B46200-81B7-4106-9CC8-405E6BACB193@fbreuer.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.6.0

On 18.07.2014 20:54, Felix Breuer wrote: > Hi Lars and Larry, > > > thank you for your help! Just knowing that the right name to search for was “setsum” helped a lot. Just searching for theorems containing “sum” (in the JEdit Query Panel) - as I had done before - finds nothing. In such cases, it might help searching for theorems with a certain name, e.g. "name: set". Also, you can search for constants of a certain type. > After some more work, I am now thoroughly stuck again, though: I want to prove: > > lemma "( ∑ k∈{0..m}. ((f (Suc k)) * (recip f (n - (Suc k)))) ) = ( ∑ k∈{(Suc 0)..(Suc m)}. ((f k) * (recip f (n - k))) )" > > Whatever f and recip are, this should follow simply from setsum_shift_bounds_cl_Suc_ivl, which reads: > > corollary setsum_shift_bounds_cl_Suc_ivl: > "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}” > > However, I cannot figure out how to get Isabelle to instantiate the corollary in the right way. When I try to prove the lemma using > > by (simp add: setsum_shift_bounds_cl_Suc_ivl) There is "subst" which applies only a single rule at a single position. You can also instruct simp to use only the given set of rules. by (subst setsum_shift_bounds_cl_Suc_ivl) .. (* where ".." equals "rule" for most purposes *) or by (simp only: setsum_shift_bounds_cl_Suc_ivl) Last but not least, you can also identify the wrong rule by using the simplifier trace: using [[simp_trace]] apply simp (* Look in the tracing output to identify the wrong rule, then replace apply simp by: *) by (simp del: foo) Best regards, Lars

**References**:**[isabelle] newbie questions: theory for sums and Isar syntax***From:*Felix Breuer

**Re: [isabelle] newbie questions: theory for sums and Isar syntax***From:*Lars Hupel

**Re: [isabelle] newbie questions: theory for sums and Isar syntax***From:*Felix Breuer

- Previous by Date: [isabelle] new in the AFP: CISC-Kernel
- Next by Date: Re: [isabelle] Addition to List?: rev_nonempty_induct
- Previous by Thread: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Thread: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Cl-isabelle-users July 2014 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