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

Enumeration types



Hello,

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
occur?

Thanking you in advance,

Malcolm Dowse