*To*: "Aaron W. Hsu" <arcfide at sacrideo.us>*Subject*: Re: [isabelle] Linear Ordering for nat list*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Wed, 2 May 2012 14:59:36 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <jnqbd9$ced$1@dough.gmane.org>*References*: <jnpkdv$e6u$1@dough.gmane.org> <84749AD1-8794-470E-873E-FF493841C4BF@cam.ac.uk> <jnpsp0$7d6$1@dough.gmane.org> <9FE0740D-C2E4-411E-AB24-2068DFA83D40@gmail.com> <jnqbd9$ced$1@dough.gmane.org>

On 02/05/2012, at 1:58 PM, Aaron W. Hsu wrote: > On Wed, 02 May 2012 11:14:33 +1000, Peter Gammie wrote: > >> Before you do, have a poke around the Isabelle sources. There are a few >> theories about list orders already in there (e.g. "Length Lexicographic >> Ordering" in src/HOL/List.thy and probably a prefix order somewhere). > > Maybe I am going about this the wrong way. What I really want to do is > to be able to talk about the greatest element in the domain of a function > whose domain is finite. The greatest element of a finite set? Take a look at the Finite_Set theory - max is commutative so you can use the fold combinator for finite sets. > I want this for two reasons, but one of them is > because I want to state that a property that defines a subset of these > functions that map their domains completely. The way I was thinking of > doing this was getting the Max element of the domain and then saying > something like "domain f = {x. low domain f <= x < max domain f}" or some > such. > > Am I completely off base here? I don't know. One approach is simply to carry around a predicate that indicates where the function is defined. You can see another approach in HOLCF, where the "('a, 'b) cfun" type constructor identifies the subset of HOL functions that are continuous. Coarsely put all lemmas that require continuity then have it as a side condition, e.g. beta_cfun. See also Alex Krauss's descriptions of his fun package, which has some treatment of partially-defined functions. It depends on how your domains and functions are parameterised. Perhaps you can give us more information on what you're trying to do. cheers peter -- http://peteg.org/

**Follow-Ups**:**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**References**:**[isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**Re: [isabelle] Linear Ordering for nat list***From:*John Wickerson

**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**Re: [isabelle] Linear Ordering for nat list***From:*Peter Gammie

**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

- Previous by Date: [isabelle] Browsing Main?
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] Linear Ordering for nat list
- Next by Thread: Re: [isabelle] Linear Ordering for nat list
- Cl-isabelle-users May 2012 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