*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] Trouble selecting maximum element of locally linear relation*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 20 Mar 2008 07:45:04 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000803180931k8f9dd61k4af0010e7b5e1603@mail.gmail.com>*References*: <6dbd4d000803180931k8f9dd61k4af0010e7b5e1603@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Regards Tobias Denis Bueno schrieb:

Hi all, In a proof I am working on, I need to formalise the statement "let x be the largest member of X". There is the Max operator in Finite_Set which provides this, but it requires the elements in the set X to be ordered by a linear order. My elements are *linearly ordered* but they are not ordered by a linear order. That is, my order is locally linear in the context I care about, but it is not linear in general. Is there a way to express this fact to Isabelle so I can use the Max function? Second, since I couldn't figure out how to express this to Isabelle (if it is indeed possible), I tried to prove that there is always a max for my set. Mathematically, this is achieved via a simple induction on the cardinality of the set X, and indeed in the Finite_Set library there is the induction rule "Finite_Set.finite_ne_induct" for an induction whose base case is a non-empty set, which is exactly what I want. However, Isabelle rejects my attempt to perform this induction ("empty result sequence"). Concretely, I am using a sequence-prefix ordering from the library LList2 [0]: x <= y if the sequence x is a prefix of y. In my proof, every element of the set X is a prefix of a fixed sequence, t. Thus, the elements in X are linearly ordered, since any two elements x and y are prefixes of t, and thus x <= y or y <= x. If you can help me, please try out the proof script, which I've attached: the relevant induction is for the theorem on line 152. Thank you. [0] http://afp.sourceforge.net/browser_info/current/HOL/Lazy-Lists-II/LList2.html

**Follow-Ups**:

**References**:**[isabelle] Trouble selecting maximum element of locally linear relation***From:*Denis Bueno

- Previous by Date: [isabelle] 转发 :the inductive approach analyze the NS protocol
- Next by Date: Re: [isabelle] term abbreviations?
- Previous by Thread: Re: [isabelle] Trouble selecting maximum element of locally linear relation
- Next by Thread: Re: [isabelle] Trouble selecting maximum element of locally linear relation
- Cl-isabelle-users March 2008 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