Re: [isabelle] Linear Ordering for nat list

One simplistic approach to modelling those arrays would be to represent an
array as a triple (or, better, a record) of a size (of type nat) a
dimension (of type nat) and a function (of type nat list => 'a option).
Then define a predicate isArray :: 'a array_record => bool, which is
something along the lines of
isArray a = forall ls. (length ls = a.dimension) and (forall x. member x ls
==> x < a.size) <=> not (a.f ls = NONE)
which says that the function is equal to some value exactly when the index
list is valid.
(sorry I don't know the exact Isabelle syntax for that statement above - I
usually use a different theorem prover. hopefully my pseudocode is clear.)

You could then either carry that isArray predicate as a precondition on
most everything you prove (you could use locales to make that easier, i.e.
you wouldn't have to keep typing it out), or you could use isArray to
actually define a new array type, where all of those arrays would be valid,
but that may make it harder to reason about them, depending on what kind of
reasoning you need to do.

On Wed, May 2, 2012 at 7:05 AM, Aaron W. Hsu <arcfide at> wrote:

> 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.