Re: [PVS-Help] using TCCs in proofs

["Cesar A. Munoz" <munoz@nianet.org>]

Dave,
My mistake. Try the following revisited script:

(defstep try-tccs (fname &optional theory )
  (let ((ftcc (format nil "~A_TCC" fname))
        (th   (if theory (get-typechecked-theory theory)
*current-theory*))
        (l    (length ftcc))
        (decls (remove-if-not
                #'(lambda(d)
                    (and (subtype-tcc? d)
                         (let* ((idstr (format nil "~A" (id d)))
                                (idx   (mismatch ftcc idstr)))
                           (and idx (= idx l)))))
                (all-decls th))))
    (one-tcc decls))
  "Tries all the TCCs that match fname from theory (default is current
theory)"
  "~%Trying all the TCCs that match fname")

By default, it looks at the current theory. If you want definitions in
other theory try the option :theory, as in (try-tccs "f" :theory "foo").

I have tried the script in the following example:
                        
foo : THEORY
BEGIN
 
  x,y : VAR real
 
  f(x,y):real = IF y > 0 THEN 1/x ELSE 1/y ENDIF;
 
  l1: LEMMA FORALL (x: real, y: real): y > 0 IMPLIES x /= 0
%|- l1 : PROOF (try-tccs "f") QED
 
  l2: LEMMA FORALL (y: real): NOT y > 0 IMPLIES y /= 0
%|- l2 : PROOF (try-tccs "f") QED
 
END foo
 
faa : THEORY
BEGIN
 
  IMPORTING foo
 
  x,y : VAR real
 
  l1: LEMMA FORALL (x: real, y: real): y > 0 IMPLIES x /= 0
%|- l1 : PROOF (try-tccs "f" :theory "foo") QED
 
  l2: LEMMA FORALL (y: real): NOT y > 0 IMPLIES y /= 0
%|- l2 : PROOF (try-tccs "f" :theory "foo") QED
 
END faa

Hope that it helps,
Cesar

On Tue, 2004-02-10 at 23:26, David Naumann wrote:
> Dear Cesar Munoz,
> 
> Thanks very much for your help.
> 
> I added your strategies to pvs-strategies and tried it on several sequents
> in a proof.  Each time I get an error (see transcript below).
> 
> I'm not familiar with the strategy facility, but I noticed a reference to
> *current-theory* in your code.  The formula I'm proving is in a different
> theory, which imports the theory containing the declaration (named
> "fieldUpdateS") from which I want to use TCCs.  Could this be the problem?
> If so, can the strategy be changed to access all theories in the import
> chain?
> 
> It's possible that the error has nothing to do with your strategy.
> My theories involve slightly complicated use of dependent types and
> sometimes I get an error about "No methods applicable".  There's an
> outstanding bug report or two about it.
> 
> thanks,
> dave
> 
> *****************
> 
> Rule?
> (try-tccs "fieldUpdateS")
> Error: No methods applicable for generic function
>        #<standard-generic-function id> with args
>        (#<IMPORTING indistinguishable>) of classes (importing)
>   [condition type: program-error]
> 
> Restart actions (select using :continue):
> ...
> 
> *****************

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855