*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] bug in strict_linear_order_on*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 30 Jun 2015 21:25:38 +0200*In-reply-to*: <5676D599-C2E1-4B8E-8B25-76E58428489C@cantab.net>*References*: <5676D599-C2E1-4B8E-8B25-76E58428489C@cantab.net>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Hi John,

This may take a little while. Tobias On 30/06/2015 18:03, John Wickerson wrote:

Dear Isabelle, I think the definition of "strict_linear_order_on" in HOL/Order_Relation.thy may be wrong, or at least, sub-optimal. Specifically, the definition does not state that the relation r must be contained within A*A. In contrast, the non-strict version, "linear_order_on", *does* make this restriction. In which case, can I propose that the definition be updated to (something like):definition "NEW_strict_linear_order_on A r â strict_linear_order_on A r â (r â A Ã A)"On another, slightly-related, matter -- I was hoping to find a lemma capturing the "order-extension principle". Something a bit like: "if p is a strict partial order on A, then there exists a strict linear order on A that is a superset of p". [I haven't formulated this very precisely, but can do.] This doesn't immediately appear to be in the HOL library, but seems an obvious candidate for inclusion. Did I miss it somewhere under a different name? Cheers, John

**Attachment:
smime.p7s**

**References**:**[isabelle] bug in strict_linear_order_on***From:*John Wickerson

- Previous by Date: [isabelle] bug in strict_linear_order_on
- Previous by Thread: [isabelle] bug in strict_linear_order_on
- Cl-isabelle-users June 2015 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