Re: [isabelle] Linear Ordering for nat list



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?


-- 
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.






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