*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] substitution*From*: Prathamesh <prathamesh.t at gmail.com>*Date*: Wed, 12 Sep 2012 18:08:24 +0530*In-reply-to*: <CADCED3qn9rL9jwW3XODG=mfZFgNErHtaEr=rV20-LG28R6+WTQ@mail.gmail.com>*References*: <CADCED3qn9rL9jwW3XODG=mfZFgNErHtaEr=rV20-LG28R6+WTQ@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] substitution***From:*Prathamesh

**References**:**[isabelle] substitution***From:*Prathamesh

- Previous by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Date: Re: [isabelle] substitution
- Previous by Thread: [isabelle] substitution
- Next by Thread: Re: [isabelle] substitution
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list