Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 14 Oct 1993 05:16:48 +0100
Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA06618;
          Wed, 13 Oct 93 22:10:05 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.4/16.2) id AA06610; Wed, 13 Oct 93 22:10:03 -0600
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA15549; Wed, 13 Oct 93 21:09:57 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA13727;
          Wed, 13 Oct 93 21:07:40 -0700
Message-Id: <9310140407.AA13727@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: Inefficiency when processing big pairs
Date: Wed, 13 Oct 93 21:07:35 PDT
From: chou@cs.ucla.edu

I am verifying some distributed programs and need to deal with
big pairs (around 10 components).  I found that HOL can be very 

inefficient when processing big pairs, as the following session
shows.  The conversion PUSH_IN_CONV pushes the first of sequence
of existential quantifiers all the way in:
  

    val PBINDER_CONV = RAND_CONV o PABS_CONV ;
  

    fun PUSH_IN_CONV (tm) =
      ( (SWAP_PEXISTS_CONV THENC PBINDER_CONV PUSH_IN_CONV)
        ORELSEC ALL_CONV
      ) (tm) ;

Below the theorem counter is reset between each call to PUSH_IN_CONV:
  

  - PUSH_IN_CONV (--`?w:num#num#num#num#num. ?x y z. x + y + z = 10`--) ;
  val it = |- (?w x y z. x + y + z = 10) = (?x y z w. x + y + z = 10) : thm
  

  - thm_count();
  val it = (217,213) : int * int
  

  - PUSH_IN_CONV (--`?(w1,w2,w3,w4,w5):num#num#num#num#num. ?x y z. x + y +  
z = 10`--) ;
  val it =
    |- (?(w1,w2,w3,w4,w5). ?x y z. x + y + z = 10) = (?x y z.  
?(w1,w2,w3,w4,w5). x + y + z = 10) : thm
  

  - thm_count();
  val it = (1909,3771) : int * int
  

  - PUSH_IN_CONV (--`?w:num#num#num#num#num#num#num#num#num#num. ?x y z. x +  
y + z = 10`--) ;
  val it = |- (?w x y z. x + y + z = 10) = (?x y z w. x + y + z = 10) : thm
  

  - thm_count();
  val it = (217,213) : int * int
  

  - PUSH_IN_CONV  
(--`?(w1,w2,w3,w4,w5,w6,w7,w8,w9,w10):num#num#num#num#num#num#num#num#num#nu 
m. ?x y z. x + y + z = 10`--) ;
  val it =
    |- (?(w1,w2,w3,w4,w5,w6,w7,w8,w9,w10). ?x y z. x + y + z = 10) =
       (?x y z. ?(w1,w2,w3,w4,w5,w6,w7,w8,w9,w10). x + y + z = 10) : thm
  

  - thm_count();
  val it = (7039,14001) : int * int


What is the source of this inefficiency?  And how to get around it?
Any suggestions are appreciated!

- Ching Tsun