[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Subject*: Re: Defining a finite (super)type.*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Wed, 18 Apr 2001 18:34:21 -0700*CC*: pvs-help@csl.sri.com, Tamarah Arons <tamarah@narkis.wisdom.weizmann.ac.il>*References*: <Pine.GSO.3.96-heb-2.07.1010418233221.19287A-100000@summer.wisdom.weizmann.ac.il>*Sender*: pvs-help-owner@csl.sri.com

Tamarah Arons wrote: > > Hello, > > I would like to define "FINITE_TYPE" as any type with a finite > number of elements (i.e. a 1-1 mapping from these elements to upto[N] > for some N). That is, I would like any finite type, > (for example, a finite set, or a data structure with finite fields > e.g. [# b : bool, u : upto[10] #]), to be called a FINITE_TYPE. > > My motivation is that I have a number of theories with parameter > [DOMAIN : NONEMPTY_TYPE] where DOMAIN in instantiated with various > types when the theorem is imported. I would like to derive similar > theorems for [DOMAIN : FINITE_TYPE]. How can I define such a property > over types? (I realise that a possible workaround may be to add as theory > parameters a mapping from the type to natural numbers and a maximum, > but I am hoping for a more elegant solution.) > > Thanks, > Tamarah You can use the boolean constant "is_finite_type" of finite_set_def in the prelude. It's defined so that is_finite_type[T] is true whenever T is a finite type. To specify that a parameter must be a finite type, you can use theory assumptions, for example: th [T: TYPE] : THEORY BEGIN ASSUMING T_is_finite: ASSUMPTION is_finite_type[T] ENDASSUMING ... That's equivalent to writing th [T: TYPE] : THEORY BEGIN ASSUMING T_is_finite: ASSUMPTION EXISTS (N:nat), (g:[T -> below[N]]): injective?(g) ENDASSUMING ... Bruno -- Bruno Dutertre | bruno@sdl.sri.com SDL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

**References**:**Defining a finite (super)type.***From:*Tamarah Arons <tamarah@wisdom.weizmann.ac.il>

- Prev by Date:
**Defining a finite (super)type.** - Next by Date:
**Substitution** - Prev by thread:
**Defining a finite (super)type.** - Next by thread:
**formalizing integration** - Index(es):