*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Trouble selecting maximum element of locally linear relation*From*: "Denis Bueno" <dbueno at gmail.com>*Date*: Tue, 18 Mar 2008 12:31:12 -0400

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

**Attachment:
Hyper.thy**

**Follow-Ups**:**Re: [isabelle] Trouble selecting maximum element of locally linear relation***From:*Stefan Friedrich

**Re: [isabelle] Trouble selecting maximum element of locally linear relation***From:*Tobias Nipkow

- Previous by Date: [isabelle] CSL 2008 - Last CfP - Deadline is March 28th
- Next by Date: [isabelle] IJCAR's ESHOL Workshop - CFP
- Previous by Thread: [isabelle] CSL 2008 - Last CfP - Deadline is March 28th
- 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