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

Enumeration types


I have what I hope is a simple problem. In my theory, I have defined
an enumeration type UType as follows:

 	UType: TYPE = {emptyT, zeroT, succT}

Now, when proving theoreoms, I am finding that in a great number of
sub-goals, the prover is stating me the problem in the following form:

[1]   emptyT?(x)
[2]   zeroT?(x)

.. when, in fact, what I believe it really means, is as follows:

[-1]  succT?(x)

To turn the first into the second, am using the command
	(CASE "x = succT")
which splits it into 2 subgoals, one of which is trivially proven.

Is there any way of defining the type so this problem will not

Thanking you in advance,

Malcolm Dowse