Re: [isabelle] newbie questions: theory for sums and Isar syntax



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




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