Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 1 Sep 1992 22:25:54 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08553;
          Tue, 1 Sep 92 12:16:11 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA08547;
          Tue, 1 Sep 92 12:15:59 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA00647;
          Tue, 1 Sep 92 15:16:55 -0400
Message-Id: <9209011916.AA00647@air52.larc.nasa.gov>
Date: Tue, 1 Sep 92 15:16:55 -0400
From: Victor "A." Carreno <vac@gov.nasa.larc.air16>
To: info-hol@edu.uidaho.cs.ted
Subject: IMP_RES_TAC


Hi all,

Resently I tried to prove a goal of the form "a/\b/\c ... /\m ==> R3". 
I had 3 lemmas of the form "a/\b/\c ... ==> Lx"
Since the antecedents of the lemmas are a conjunctive subset of the antecedent
of the goal, this can be solved easily by STRIP_TAC followed by IMP_RES_TAC
with lemmas 1-3.

The problem is that IMP_RES_TAC uses RES_CANON on the implicative theorem.
That results in an explosion of the list of theorems produced by RES_CANON,
growing exponentially with the number of conjuncts. 

In my case IMP_RES_TAC ran overnight (14 hours) without terminating. The
problem can be solved by selectively discharging and undischarging the
assumtions and using MP or by using:

% ----------------------------------------------------------------------- %
%   IMP_RES_W_THEN - : thm_tactical                                       %
%                                                                         %
%   Attempts to resolve an implicative theorem with the                   %
%   assumtions of a goal by using rewriting.                              %
%                                                  [VAC 31-8-92]          %

let IMP_RES_W_THEN ttac impth = 
     ASSUM_LIST  
     \asl. let l = map EQT_INTRO asl in
           let th = ((is_imp (concl impth)) => impth | failwith 
                           `IMP_RES_W_THEN:theorem not an implication`) in
           let res = REWRITE_RULE l th in
           ttac res;;

In the following example, with 5 conjuncts, the difference in speed is very
large. With more than 6 conjuncts IMP_RES_TAC is impractical.

let th1 = mk_thm ([],"(!a:*.A)/\(!b:*2.B)/\(!c:*3.C)/\(!d:*4.D)/\(!e:*5.E) ==> (!h.0<=h)");;

e (IMP_RES_TAC th1);;
Run time: 1198.2s
Garbage collection time: 972.2s
Intermediate theorems generated: 119754

e (IMP_RES_W_THEN ASSUME_TAC th1);;
Run time: 0.6s
Intermediate theorems generated: 34

(IMP_RES_W_THEN can probably be made fancier by checking for assumtion and
antecedents matching and failing if none is found etc.)

Cheers,

Victor.