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

Re: inst? and overloaded operators



     
     > (You
     > could have also checked the intval_adt.pvs file and applied the
     > axioms in there manually).
     
     I did, but I only found extensionality which goes the opposite
     direction. Am I overlooking something?

You can use intval_v_intval twice to prove injectiveness.  I.e., you
can prove:

intval_inj: lemma
    injective?(intval)

with:

(""
 (EXPAND "injective?")
 (REDUCE NIL)
 (LEMMA "intval_v_intval")
 (INST - "x1!1")
 (LEMMA "intval_v_intval")
 (INST - "x2!1")
 (REPLACE -5 *)
 (GROUND))