Re: [isabelle] Linear Ordering for nat list

On Wed, 02 May 2012 14:59:36 +1000, Peter Gammie wrote:

> Perhaps you can give us more information on what you're trying to do.

I am trying to come up with a basic notion of multi-dimensional arrays 
that I can use to model some things. Specifically, these arrays should 
map indices to specific values, be finite, and should be dense. The most 
basic thing I want to do with them is to get the shape. This, I want to 
have functions with the following type:

  f :: "'a array => 'a array" 

And similar. The property of density is the one I am having trouble with 
right now.  I want to state that for an array of a given shape, all of 
the indices of the given shape from [0,...,0] to [n_1-1,...,n_r-1] are 
defined, but no others, assuming that the array is of rank r, where n_i 
is the size of the array in dimension i, with 1 <= i <= r.

Any suggestions on the best way to model this would be appreciated.  
Right now I am using Map.

Aaron W. Hsu | arcfide at |
Programming is just another word for the lost art of thinking.

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