Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Wed, 14 Apr 1993 17:08:34 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26133;
          Wed, 14 Apr 93 09:01:35 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26128;
          Wed, 14 Apr 93 09:01:25 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 14 Apr 1993 16:59:55 +0100
To: val@com.netcom (Dewey Val Schorre)
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Problem writting INDIRECT_TAC
In-Reply-To: Your message of Wed, 14 Apr 93 07:52:40 -0700. <199304141452.AA03935@panther.cs.uidaho.edu>
Date: Wed, 14 Apr 93 16:59:42 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.151:14.04.93.16.00.00"@cl.cam.ac.uk>


Val writes:

> I have written INDIRECT_TAC but get the following error when
> it is run:
>
>      #let INDIRECT_TAC (termList, term) =
>      #  ( [termList, (mk_imp ((mk_neg term), "F"))],
>      #    \thmList. CCONTR term (hd thmList));;
>      INDIRECT_TAC = - : ((* # term) -> ((* # term) list #
>      proof))
>
>      #
>      #g "(0=0) \/ (0=1)";;
>      "(0 = 0) \/ (0 = 1)"
>
>      () : void
>
>      #
>      #e INDIRECT_TAC;;
>      OK..
>      evaluation failed     check_valid -- CCONTR

I think you need the negated goal as an assumption rather than the antecedant
of an implication to make it fit the spec of |CCONTR|:

       A |- F
   ---------------  CCONTR "t"
    A - {~t} |- t

So the following should work, depending on whether you want to actually push
the negated goal into the assumptions, or leave it as the antecedant of an
implication:

  let INDIRECT_TAC (termList, term) =
    ( [union [mk_neg term] termList, "F"],
      \thmList. CCONTR term (hd thmList));;

or

  let INDIRECT_TAC (termList, term) =
    ( [termList, (mk_imp ((mk_neg term), "F"))],
      \thmList. CCONTR term (UNDISCH_ALL(hd thmList)));;

This seems to be an exception to the rule that there is usually a trivial way
of combining existing tactics, rather than actually writing ML. When I was
learning HOL and tried writing my own tactics in ML, I was repeatedly told I
was mad.

John.