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

Re: inst? and overloaded operators


   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)


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



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