Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu
In-Reply-To: John Harrison's message of Thu, 20 Jan 1994 13:59:22 +0100 <"swan.cl.cam.:053260:940120125930"@cl.cam.ac.uk>
Subject: X_EXISTS_TAC
Message-Id: <94Jan20.164108met.8085@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 20 Jan 1994 16:41:01 +0100


> 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.

It would be simple to write "S_..." versions of the "X_..." versions, as
John suggests. Whether one is in hol88 or hol90 doesn't matter. To go a
tiny bit further, there are other cases where types can be ascertained
by context. The most irritating is BOOL_CASES_TAC, where one often has
to annotate the argument with ":bool". I thought you could use
antiquotation to remedy this, but that solution didn't work in hol88. (It
seems to be because quotations are evaluated eagerly.) hol90 allows more
control over parsing, so one can write a non-irritating BOOL_CASES_TAC
(note, however, the obscure type).

hol88

    #let BCT tm = BOOL_CASES_TAC "^tm:bool";;
    BCT = - : (term -> tactic)

    #BCT "A";;
    Indeterminate types:  "A:?"
 
    evaluation failed     types indeterminate in quotation


hol90

    - fun BCT frag_list =
       Tactic.BOOL_CASES_TAC (Parse.term_parser
                               (QUOTE "("::frag_list@[QUOTE")"]@`:bool`));
    val BCT = fn : term frag list -> tactic

    - g `A \/ ~A`;
    val it =
      (--`A \/ ~A`--)
      ____________________________

     : goalstack

    - e (BCT `A`);
    OK..
    2 subgoals:
    val it =
     (--`F \/ ~F`--)
     ____________________________
   

     (--`T \/ ~T`--)
     ____________________________

    : goalstack