[isabelle] How does one reason about the subset of a list?


I have a list (a "nat list") with N elements.

I assume that the elements which come before the i-th element are all
less than or equal to i.

I would like to say that if the i+1th element is also less than or equal
to the i-th element, 
then if I exchange the elements in the ith and i+1th positions 
then all elements upto i+1 are less than or equal to the i+1-th element.

I thought this should look like this:
\<forall> j. (j + 1) < length xs \<and> xs!j < ((xs!(j+1))::nat)
\<longrightarrow> (\<forall>i < j. xs!j < xs!i \<longrightarrow>
(\<forall>k \<le> j+1. xs[j:=xs!(j+1),(j+1) := xs!j]!(j+1) \<le>

I thought the best thing to do would be to prove a slightly simpler
version first which states that if all the elements in positions less
than i are less than/equal to the ith element and also that the i+1st
element is less than/equal to the ith element then all the elements upto
i+1 should be less than/equal to the ith element.

I have tried to formulate this in different ways but the formulation I
believe comes close to what I am looking for is:
\<forall> j. (j + 1) < length xs \<and> xs!j < ((xs!(j+1))::nat)
\<longrightarrow> (\<forall>i < j. xs!j < xs!i \<longrightarrow>
(\<forall>k \<le> j+1. xs!j \<le> xs!k) ) )

But I am not capable of proving anything about this statement. I tried
doing the induction on xs or on j (after removing its quantification)
but I didn't go very far.

Trying to reason about the sets involved didn't bring much. Notably, I
am wondering why I couldn't prove the below using an induction on the
list xs.:
 \<forall>n j . n < j \<longrightarrow> (\<forall>(i::nat) \<in> set xs.
n < i \<longrightarrow> ( \<forall>k \<in> set xs \<union> {j}. n < k) )

I do not believe I understand what quantification actually is...

Could anyone tell me what is wrong with these formulations and how I can
start reasoning about these?

Thanks in advance!


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