*To*: "Aaron W. Hsu" <arcfide at sacrideo.us>*Subject*: Re: [isabelle] Linear Ordering for nat list*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Wed, 2 May 2012 07:16:56 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <jnqire$ced$2@dough.gmane.org>*References*: <jnpkdv$e6u$1@dough.gmane.org> <84749AD1-8794-470E-873E-FF493841C4BF@cam.ac.uk> <jnpsp0$7d6$1@dough.gmane.org> <9FE0740D-C2E4-411E-AB24-2068DFA83D40@gmail.com> <jnqbd9$ced$1@dough.gmane.org> <D2CF3969-C3D8-4C07-B1A9-75DB00153AC0@gmail.com> <jnqire$ced$2@dough.gmane.org>*Sender*: ramana.kumar at gmail.com

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 sacrideo.us> 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 sacrideo.us | http://www.sacrideo.us > Programming is just another word for the lost art of thinking. > > >

**References**:**[isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**Re: [isabelle] Linear Ordering for nat list***From:*John Wickerson

**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**Re: [isabelle] Linear Ordering for nat list***From:*Peter Gammie

**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

**Re: [isabelle] Linear Ordering for nat list***From:*Peter Gammie

**Re: [isabelle] Linear Ordering for nat list***From:*Aaron W. Hsu

- Previous by Date: Re: [isabelle] Linear Ordering for nat list
- Next by Date: Re: [isabelle] Difference between "apply(auto)" and "apply(force)"
- Previous by Thread: Re: [isabelle] Linear Ordering for nat list
- Next by Thread: Re: [isabelle] Linear Ordering for nat list
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list