Email Gateway (Aug 19 2022 at 08:47): Email Gateway (Aug 19 2022 at 08:47):From: Prathamesh <prathamesh.t@gmail.com>
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?
have preexp24: "\<lbrakk> 1+i < List.length l; (i+k+2)\<le>(List.length l)
\<rbrakk> \<Longrightarrow> ((take i l)@drop (i+2) l)!(k+i) = l!(i+2+k)"
by (simp add: linorder_not_le nat_add_commute nth_append_length_plus
preexp22 prerednbasic2 trans_le_add1)
have preexp25: "\<lbrakk> i \<le> n ; (n+2)\<le>(List.length l) \<rbrakk>
\<Longrightarrow> i+1<(List.length l)" by auto
have preexp26 "\<lbrakk> i \<le> n ; (n+2)\<le>(List.length l) \<rbrakk>
\<Longrightarrow> ((take i l)@drop (i+2) l)!n = l!(n+2)" using preexp24
preexp25 by auto
(unable to prove)
Prathamesh
Email Gateway (Aug 19 2022 at 08:47):From: Prathamesh <prathamesh.t@gmail.com>
I happened to send this query a day back, can I knot if it filtered out?
Prathamesh
Email Gateway (Aug 19 2022 at 08:47):From: Prathamesh <prathamesh.t@gmail.com>
know*
Email Gateway (Aug 19 2022 at 08:47):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi,
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é
Email Gateway (Aug 19 2022 at 08:47):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Last updated: Nov 21 2024 at 12:39 UTC