*To*: Johannes Hölzl <hoelzl at in.tum.de>, Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Vector of bools*From*: s.wong.731 at gmail.com*Date*: Tue, 29 Mar 2011 17:00:02 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1301411462.2260.1076.camel@macbroy12.informatik.tu-muenchen.de>

Great! That worked. Thanks. Steve On Mar 29, 2011 4:11pm, Johannes Hölzl <hoelzl at in.tum.de> wrote:

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

Am Dienstag, den 29.03.2011, 15:37 +0100 schrieb Steve W:

> I see. So if I want to try, say, "real ^ 'n", which libraries do I needto

> import? I'vetried "HOL/Multivariate_Analysis/Cartesian_Euclidean_Space",

> but it takes a very long time to load the import.

>

> Thanks

> Steve

>

> On Fri, Mar 25, 2011 at 9:30 PM, Brian Huffman brianh at cs.pdx.edu> wrote:

>

> > 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, eg,

> > > ?

> >

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

> >

**References**:**Re: [isabelle] Vector of bools***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Vector of bools
- Next by Date: [isabelle] Proving two real^3 spaces are the same
- Previous by Thread: Re: [isabelle] Vector of bools
- Next by Thread: [isabelle] HOL/Auth : extension to parts/analz/synth
- 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