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

Re: Defining a finite (super)type.



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