*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Vector of bools*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 29 Mar 2011 17:11:02 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTinUY0LS4rOmL=hxj=Rqdne-b9fjMNyvEz89CQCk@mail.gmail.com>*Organization*: Technische Universität München*References*: <AANLkTi=CxrGvO=fw6f+O63UHjqZuPAFLycgnbNPAEvQ2@mail.gmail.com> <AANLkTik6ZD=giEw1Q_b00AAy17RcY8u+YG_BS7iGCbYg@mail.gmail.com> <AANLkTinUY0LS4rOmL=hxj=Rqdne-b9fjMNyvEz89CQCk@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] Vector of bools***From:*s . wong . 731

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

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

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

- Previous by Date: Re: [isabelle] Vector of bools
- Next by Date: Re: [isabelle] Vector of bools
- 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