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.