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, 6 Oct 1992 16:34:36 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22957;
          Tue, 6 Oct 92 08:18:06 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA22952;
          Tue, 6 Oct 92 08:17:53 -0700
Received: by infix.cs.ruu.nl id AA01254 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Tue, 6 Oct 1992 16:16:49 +0100
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199210061516.AA01254@infix.cs.ruu.nl>
Subject: Re: about the speed of tactical THEN
To: wishnu@nl.ruu.cs (Wishnu Prasetya)
Date: Tue, 6 Oct 92 16:16:48 MET
Cc: info-hol@edu.uidaho.cs.ted (hol mailing list)
In-Reply-To: <199210051215.AA21527@infix.cs.ruu.nl>; from "Wishnu Prasetya" at Oct 5, 92 1:15 pm
X-Mailer: ELM [version 2.3 PL11]

  > Supposing you want to prove the goal 
  > 
  >    ([],T)
  > 
  > by applying series of tactics T1... TN, you can do this by:
  > 
  >    # prove(T, T1 THEN ... THEN TN)
  > 
  > or by using the subgoal package, ie:
  > 
  >    # set_goal([],T) ;;
  >    # e T1 ;;
  >      ...
  >    # e TN ;;
  > 
  > However, when N is something about 20 and involves stuff like
  > resolution or tautology proving, the first method using 'prove' tend
  > to be long, or too long that my stack over flows. Using the subgoal
  > package gives no problem.
  > 
  > The question is, why can't people just implement THEN just like a
  > consecutive application of 'expand' s? Will this speed up the 'prove'
  > style?

Sorry, it turned out that I misunderstood THEN as I naively assumed that

   T1 THEN T2

and

   e T1 ;; e T2

are sort of equivalent, which is not the case since THEN applies T2 to
ALL subgoals generated by T1, not only the top most subgoal.

-Wishnu-



--