Re: [isabelle] Linear Ordering for nat list

Warning: HOL functions are total, there is no notion of a domain. That is, the
domain is always the whole type. If you want to express that the function is
partial, you need to do so explicitly. Peter already suggested carrying the
domain around explicitly or using HOLCF. Making it a function to type "option"
is another option ;-)


Am 02/05/2012 05:58, schrieb Aaron W. Hsu:
> 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. 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?

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