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 15:49:54 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25941;
          Wed, 14 Apr 93 07:42:29 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA25936; Wed, 14 Apr 93 07:42:24 -0700
Received: from localhost by panther.cs.uidaho.edu with SMTP 
          id AA03935 (5.65c/IDA-1.4.4 for info-hol@cs.uidaho.edu);
          Wed, 14 Apr 1993 07:52:41 -0700
Message-Id: <199304141452.AA03935@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Problem writting INDIRECT_TAC
Date: Wed, 14 Apr 93 07:52:40 -0700
From: Phil Windley <windley@edu.uidaho.cs.panther>
X-Mts: smtp


The following message was sent to info-hol-request.  I presume it was meant
for forwarding to the list.  [PJW]

------- Forwarded Message

Date: Wed, 14 Apr 93 07:40:14 -0700
From: val@netcom.com (Dewey Val Schorre)
Message-Id: <9304141440.AA01237@netcom2.netcom.com>
To: info-hol-request@ted.cs.uidaho.edu
Subject: Problem writting INDIRECT_TAC



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 decided to creep upon the problem by modifying DISJ2_TAC,
which works
fine as follows:

     #let DISJ2_TAC(termList, term) =
     #   let (term1, term2) = dest_disj term
     #   in ([(termList, term2)],
     #      \thmList. DISJ2 term1 (hd thmList));;
     DISJ2_TAC = - : ((* # term) -> ((* # term) list #
     proof))
     
     #
     #g "(0=0) \/ (0=1)";;
     "(0 = 0) \/ (0 = 1)"
     
     () : void
     
     #
     #e DISJ2_TAC;;
     OK..
     "0 = 1"
     
     () : void
     
     #

A slight change makes it fail.

     #let DISJ2_TAC(termList, term) =
     #   let (term1, term2) = (term, term)
     #   in ([(termList, term2)],
     #      \thmList. DISJ2 term1 (hd thmList));;
     DISJ2_TAC = - : ((* # term) -> ((* # term) list #
     proof))
     
     #
     #g "(0=0) \/ (0=1)";;
     "(0 = 0) \/ (0 = 1)"
     
     () : void
     
     #
     #e DISJ2_TAC;;
     OK..
     evaluation failed     Invalid tactic
     
     #

What went wrong?

Val


------- End of Forwarded Message