*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] How does one reason about the subset of a list?*From*: Martin Ellis <m.a.ellis at ncl.ac.uk>*Date*: Sun, 26 Feb 2006 04:28:20 +0000*In-reply-to*: <19FD5FDFDE9BF64EADBECBD4B444BDDD061612@mucse307.eu.infineon.com>*References*: <19FD5FDFDE9BF64EADBECBD4B444BDDD061612@mucse307.eu.infineon.com>*User-agent*: KMail/1.9.1

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

**Follow-Ups**:

**References**:**[isabelle] How does one reason about the subset of a list?***From:*Primrose.Mbanefo

- Previous by Date: [isabelle] found it
- Next by Date: Re: [isabelle] How does one reason about the subset of a list?
- Previous by Thread: [isabelle] How does one reason about the subset of a list?
- Next by Thread: Re: [isabelle] How does one reason about the subset of a list?
- Cl-isabelle-users February 2006 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