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

Defining a finite (super)type.


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