Re: [isabelle] substitution



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.

find_theorems "(_ @ _) ! _ = _"
find_theorems "drop _ _ ! _ = _"

Cheers,
René


-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck





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