Re: [isabelle] substitution



I happened to send this query a day back, can I knot if it filtered out?
Prathamesh

On Tue, Sep 11, 2012 at 5:42 PM, Prathamesh <prathamesh.t at gmail.com> wrote:

> 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
>
>


-- 
"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.