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, 13 Jul 1995 12:36:48 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA164003618;
          Thu, 13 Jul 1995 05:06:58 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from relay.cs.ruu.nl (infix.cs.ruu.nl) by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA163973614;
          Thu, 13 Jul 1995 05:06:54 -0600
Received: from muddy.cs.ruu.nl (wishnu@muddy.cs.ruu.nl [131.211.80.113]) 
          by relay.cs.ruu.nl (8.6.12/8.6.12/ehk) with ESMTP id NAA29648 
          for <info-hol@leopard.cs.byu.edu>; Thu, 13 Jul 1995 13:07:57 +0200
Received: (wishnu@localhost) by muddy.cs.ruu.nl (8.6.9/8.6.9) id NAA07267;
          Thu, 13 Jul 1995 13:07:53 +0200
Date: Thu, 13 Jul 1995 13:07:51 +0200 (METDST)
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
To: hol mailing list <info-hol@leopard.cs.byu.edu>
Subject: [Q] pattern matching for existential quatification
Message-Id: <Pine.HPP.3.91.950713123638.270O-100000@muddy.cs.ruu.nl>
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII

Hi,

I want to have a tactic that can prove the following automatically:

    A1; "P x"   ?-  "?z. P z"

This is the code I wrote using unifier 'match':

     let MATCH_ASM_EXISTS_TAC (asml,g) =
        (FIRST_ASSUM (\thm. (EXISTS_TAC o fst o hd o fst)
                                (match (snd (dest_exists g)) (concl thm)))
        THEN FIRST_ASSUM ACCEPT_TAC) (asml,g) ;;

Questions:

      1. I'm not sure if the above is the best way to do it.
      2. Is there perhaps a standard tactic I don't know that ought to
         do the same thing?

--Wishnu--