[isabelle] substitution



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



-- 
"Men make their own history, but they do not make it as they please; they
do not make it under self-selected circumstances, but under circumstances
existing already, given and transmitted from the past. The tradition of all
dead generations weighs like a nightmare on the brains of the living."


The Eighteenth Brumaire of Louis Bonaparte, Karl Marx




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