*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] How does one reason about the subset of a list?*From*: <Primrose.Mbanefo at Infineon.com>*Date*: Fri, 24 Feb 2006 16:51:13 +0100*Thread-index*: AcY5WiOf+VDc2983Toy8JBf0qgWzGA==*Thread-topic*: How does one reason about the subset of a list?

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

**Follow-Ups**:**Re: [isabelle] How does one reason about the subset of a list?***From:*Martin Ellis

- Previous by Date: Re: [isabelle] typecheck a term
- Next by Date: [isabelle] saving state
- Previous by Thread: [isabelle] HOR 2006: call for abstracts
- 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