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

*To*: pvs-help@csl.sri.com*Subject*: Defining a finite (super)type.*From*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Date*: Wed, 18 Apr 2001 23:37:35 +0300 (IDT)*cc*: Tamarah Arons <tamarah@narkis.wisdom.weizmann.ac.il>*Sender*: pvs-help-owner@csl.sri.com

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

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