[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 #]), 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.)