*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Vector of bools*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 28 Mar 2011 09:43:21 +1100*Accept-language*: en-US*Acceptlanguage*: en-US*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTik6ZD=giEw1Q_b00AAy17RcY8u+YG_BS7iGCbYg@mail.gmail.com>*References*: <AANLkTi=CxrGvO=fw6f+O63UHjqZuPAFLycgnbNPAEvQ2@mail.gmail.com>, <AANLkTik6ZD=giEw1Q_b00AAy17RcY8u+YG_BS7iGCbYg@mail.gmail.com>*Thread-index*: AcvrNWVgEg4EIc/dSkeb1+y8bLUGxwBmjW5e*Thread-topic*: [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.

**References**:**[isabelle] Vector of bools***From:*Steve W

**Re: [isabelle] Vector of bools***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Making records instances of classes
- Next by Date: [isabelle] HOL/Auth : extension to parts/analz/synth
- Previous by Thread: Re: [isabelle] Vector of bools
- Next by Thread: Re: [isabelle] Vector of bools
- Cl-isabelle-users March 2011 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