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



On Friday 24 February 2006 15:51, Primrose.Mbanefo at infineon.com wrote:
> I assume that the elements which come before the i-th element are all
> less than or equal to i.

That's a mouthful.  Call it 'P':
constdefs
"P (xs::nat list) == ALL i. i < length xs --> xs!i <= i"

(I'm using the ASCII notation here, see the tutorial appendix for the prettier 
representation)

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

You can start by defining 'exchange the elements'.  Might as well make it for 
any two elements, no need to limit ourselves to consecutive elements:

constdefs
"listswap xs i j == xs[i := xs ! j, j := xs ! i]"

The function "preserves the length of xs", in the sense that it's result is 
the same length.  You don't need this property, but it can tidy up the proof 
states you see later if you have these lemmas:

lemma listswap_length:
  "!! i j xs. i < length xs & j < length xs -->
              length (listswap xs i j) = length xs"
  apply(induct_tac i)
  by(auto simp add:listswap_def)

lemma listswap_length2:
  "[| i< length xs; j < length xs |] ==> length (listswap xs i j) = length xs"
  by(simp add: listswap_length)

(Is there an easier way to get the latter?)

> 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>
> xs[j:=xs!(j+1),(j+1):=xs!j]!k))

Firstly, the "\<forall>i < j. xs!j < xs!i" doesn't seem to correspond with 
anything in your English description.

You seem to be missing either the assumption that P already holds of the list 
in the first place, or it holds for some initial number of elements, 
depending on what you're trying to prove.  If it doesn't already hold, then 
your exchange wont fix that property.  

Not sure whether you want to assume P true of the whole list, or just up to a 
given element.  Assuming the former, you could write:

lemma "P xs --> 
              (ALL j. j < (length xs - 1) -->
                 xs!(j+1) <= xs!j -->
                    P (listswap xs j (j+1)) )"

You should see that that much more closely matches your English description 
above. ("P xs" is the first paragraph of yours I quoted, etc.)

Using the listswap_length lemma, the last line will expand to:
   ALL i < length xs. listswap xs j (j+1) ! i <= i

So there are three cases to consider:
 * where xs!i is the element at j (i.e. i = j)
 * where xs!i is the element at j+1 (i = j+1)
 * where i is an element unaffected by the exchange.
The proof of that falls out fairly straight-forwardly.

Is that the goal you're trying to prove?  If not, and you want P to be a 
property only of the first n elements, then redefine it to be a predicate
P (xs::nat list) (n::nat), rather than P (xs::nat list).

Hope that gives you a start.

Martin





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