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, 20 Jan 1994 13:12:13 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14998;
          Thu, 20 Jan 1994 06:02:26 -0700
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.8/16.2) id AA14994;
          Thu, 20 Jan 1994 06:02:15 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA18837;
          Thu, 20 Jan 1994 04:59:34 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 20 Jan 1994 12:59:27 +0000
To: info-hol@cs.uidaho.edu
Subject: Re: X_EXISTS_TAC
In-Reply-To: Your message of "Wed, 19 Jan 94 20:41:43 MST." <"swan.cl.cam.:141450:940120044614"@cl.cam.ac.uk>
Date: Thu, 20 Jan 94 12:59:22 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:053260:940120125930"@cl.cam.ac.uk>


Many people have given an implementation of something approaching X_EXISTS_TAC.

I'd just like to make a general suggestion concerning functions of the X_...
variety (X_GEN_TAC, X_SKOLEM_CONV etc.) These all take a term argument
indicating the variable name. Why not just take a string? The term is always a
variable, and the type is determined by context. Hence this would save the user
the effort of entering type information at each invocation.

Perhaps this is too much of an incompatible change in HOL88, but if done in
hol90, it could be absorbed in the wider trauma of changing over. Besides, the
appeal of avoiding term quotation is greater in hol90.

John.

P.S. For example (to give yet another implementation, and not a very good one):

#let X_EXISTS_TAC v witness (asl,tm) =          
#  let var = mk_var(v,type_of witness) in 
#  let evs,bod = strip_exists tm in
#  let svs = uncurry append (partition(curry$=var) evs) in
#  let th = PROVE(mk_imp(list_mk_exists(svs,bod),tm),
#    STRIP_TAC THEN MAP_EVERY EXISTS_TAC evs THEN POP_ASSUM ACCEPT_TAC) in
#  (MATCH_MP_TAC th THEN EXISTS_TAC witness)(asl,tm);;
X_EXISTS_TAC = - : (string -> term -> tactic)

#g "?w x y z. w + x + y + z = 5";;
"?w x y z. w + (x + (y + z)) = 5"

() : void

#X_EXISTS_TAC `y` "2";;
- : tactic

#e it;;
OK..
"?w x z. w + (x + (2 + z)) = 5"