Re: [isabelle] Vector of bools



A third variant that should be mentioned is to use the word library, which provides a formalisation of machine-word. The 32-bit word type used in your CPU is equivalent to a vector of 32 bools. The word library allows you to construct such a vector for any fixed width.

>From memory you need to build the HOL-Word image and then import Word to get easy access to the word operations.

Given "x :: 32 word" you can query positions in the word with "x !! 1", "x !! 2" etc and also do the same kind of 32-bit arithmetic your CPU does with "(x + 17) * 22" etc. This includes the "x AND 1", "x OR 12", "x XOR 13" operators which translate into logical operations at every point in the vector.

Yours,
     Thomas.
________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Brian Huffman [brianh at cs.pdx.edu]
Sent: Saturday, March 26, 2011 8:30 AM
To: Steve W
Cc: isabelle-users
Subject: Re: [isabelle] Vector of bools

On Fri, Mar 25, 2011 at 10:46 AM, Steve W <s.wong.731 at gmail.com> wrote:
> I see that one can use real_vector to construct a vector of reals,

First of all, remember that real_vector is a *type class*, not a *type
constructor*. The real_vector class merely classifies types that
support scalar multiplication by real numbers.

To actually "construct a vector of reals", you will need to use some
specific type constructor that is an *instance* of the real_vector
class. For example, tuples like "real * real" or finite cartesian
products like "real ^ 'n".

> but is
> there a way to construct a vector of boolean values, e.g.,
> <true,false,false...>?

That depends. What kinds of operations on vectors of booleans do you require?

You could use the finite cartesian product "bool ^ 'n" from
Multivariate_Analysis, but that library doesn't provide many
operations that work with element types besides "real", "complex",
etc.

Another possibility is to use "bool list". The library provides lots
of list operations, but unlike type "bool ^ 'n", lists are not
guaranteed to all have the same length.

A third possibility, if you want vectors of a small constant size, is
to use ordinary tuples like "bool * bool * bool".

I might be able to help more if you tell me more about what you are
trying to do.

- Brian


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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