Email Gateway (Aug 18 2022 at 17:26): Email Gateway (Aug 18 2022 at 17:26):From: Steve W <s.wong.731@gmail.com>
Hi,
I see that one can use real_vector to construct a vector of reals, but is
there a way to construct a vector of boolean values, e.g.,
<true,false,false...>?
Thanks a lot.
Steve
Email Gateway (Aug 18 2022 at 17:26):From: Brian Huffman <brianh@cs.pdx.edu>
On Fri, Mar 25, 2011 at 10:46 AM, Steve W <s.wong.731@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.
Email Gateway (Aug 18 2022 at 17:26):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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@lists.cam.ac.uk [cl-isabelle-users-bounces@lists.cam.ac.uk] On Behalf Of Brian Huffman [brianh@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@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.
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.
Email Gateway (Aug 18 2022 at 17:27):From: Steve W <s.wong.731@gmail.com>
I see. So if I want to try, say, "real ^ 'n", which libraries do I need to
import? I've tried "HOL/Multivariate_Analysis/Cartesian_Euclidean_Space",
but it takes a very long time to load the import.
Thanks
Steve
Email Gateway (Aug 18 2022 at 17:27):From: Johannes Hölzl <hoelzl@in.tum.de>
The intended use is to build the HOL-Multivariate_Analysis image:
cd ..../isabelle/src/HOL
isabelle make HOL-Multivariate_Analysis
and then select it in ProofGeneral with the Emacs menu:
Isabelle / Logics / Multivariate_Analysis
the building of multivariate analysis takes a couple of minutes but it
is just needed once. Then you just need to import Multivariate_Analysis.
Greetings,
Johannes
Email Gateway (Aug 18 2022 at 17:27):From: s.wong.731@gmail.com
Great! That worked. Thanks.
Steve
Last updated: Apr 19 2024 at 01:05 UTC