Re: inst? and overloaded operators

[Hendrik Tews <tews@tcs.inf.tu-dresden.de>]

Hi,

   First the simple question: is there a direct way to
   say in the datatype declaration that I want intval(X)=intval(Y)
   to imply X=Y? It does not appear to be the case now.
   
I prove 

    inj : Lemma injective?(intval)

with 

    ;;; Proof inj-1 for formula intval_test.inj
    ;;; developed with shostak decision procedures
    ("" (grind) (decompose-equality -3))

so it looks like data type constructors are injective :-; (You
could have also checked the intval_adt.pvs file and applied the
axioms in there manually).

   My longer question concerns instantiation.

Can you send the prove script that leads to this subgoal?

Bye,

Hendrik

-----------------------------------------------------------------
Hendrik Tews     Department of Theoretical Computer Science
                 Dresden University of Technology, Germany

Telefon:   	 +49 351 463 38351
e-mail:    	 tews@tcs.inf.tu-dresden.de
www:       	 http://home.pages.de/~tews/
pgp key:         http://home.pages.de/~tews/pgpkey.asc
-----------------------------------------------------------------