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

Re: ADT axioms

Matteo Vaccari writes:
 > I have a simple tree datatype:
 > tree[t:TYPE+] : DATATYPE
 >   BEGIN
 >     scalar (scalar: t): scalar?
 >     pair   (left: tree, right: tree): pair?
 >   END tree
 > but I'd like to be able to prove the reverse implication, for instance
 >   pair(a,b) = pair(c,d) IMPLIES a=c AND b=d

There may be a simpler solution, but this proof seems to work:

	 (LEMMA "tree_left_pair") 
	 (LEMMA "tree_right_pair") 

- Darrell