Re: [isabelle] Linear Ordering for nat list



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/






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.