Re: [isabelle] substitution



know*


On Wed, Sep 12, 2012 at 6:08 PM, Prathamesh <prathamesh.t at gmail.com> wrote:

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


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