# Re: [isabelle] substitution

Am 12.09.2012 um 15:20 schrieb René Thiemann <rene.thiemann at uibk.ac.at>:
> Hi,
>
>> Hello,
>> I had this problem when proving a result. I was trying to prove a result of
>> the form
>> [i+1< list.length l; (i+k+2) < list.length l) ===> ((take i l)@drop (i+2)
>> l)!(k+i) = l!(i+2+k)"
>>
>> when I try to prove the same result in the next step subtituting n for i+k,
>> as in the following, it does not seem to work. Using [of ...] does not seem
>> to help either. Any suggestions?
>
> Try this:
>
> lemma assumes il: "i+1< length l" and ikl: "(i+k+2) < length l"
> shows "((take i l)@drop (i+2) l)!(k+i) = l!(i+2+k)"
> proof -
> have lt: "length (take i l) = i" using il by auto
> have "((take i l)@drop (i+2) l)!(k+i) = drop (i+2) l ! k"
> unfolding nth_append using il lt by simp
> also have "... = l!(i + 2 + k)"
> by (rule nth_drop, insert ikl, simp)
> finally show ?thesis by simp
> qed
>
> for finding the useful lemmas I usually recommend find_theorems which will give
> you pointers to the essential lemmas nth_append and nth_drop.
I forgot to mention. In your case the direct instantiation with [of ...] is not
required. Here, "simp", "unfolding" and "rule" instantiate the lemmas appropriately.
René

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