[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:

	("" 
	 (SKOSIMP*) 
	 (LEMMA "tree_left_pair") 
	 (LEMMA "tree_right_pair") 
	 (INST?)   
	 (INST?) 
	 (REPLACE*) 
	 (ASSERT)) 

- Darrell