Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Thu, 15 Apr 1993 17:08:34 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00202; Thu, 15 Apr 93 08:50:32 -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 AA00195; Thu, 15 Apr 93 08:50:21 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Thu, 15 Apr 1993 16:49:27 +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 Thu, 15 Apr 93 07:35:45 -0700. <9304151435.AA10581@netcom2.netcom.com> Date: Thu, 15 Apr 93 16:49:23 +0100 From: John Harrison Message-Id: <"swan.cl.ca.991:15.04.93.15.49.31"@cl.cam.ac.uk> The following is an explanation of the effect observed by Val, which I'm also posting to info-hol in the hope that it will be useful for others. > INDIRECT_TAC is constructing a function containing a call on CCONTR. > When the theorem is proven, this function will be called and CCONTR > will have an incorrect argument. But HOL produced the error message > when the function was constructed, long before it was ever called. What's happening here is not that |INDIRECT_TAC| is failing, as you can see by applying it directly rather than via the subgoal package: #INDIRECT_TAC([],"(0=0) \/ (0=1)");; ([([], "~((0 = 0) \/ (0 = 1)) ==> F")], -) : ((* list # term) list # proof) The |e| function actually "cheats" by applying |mk_thm| to the subgoals, in order to check that the proof function applied to them as theorems does work. (See for example the documentation for |VALID|, |check_valid| and |chktac|.) This is the effect you are encountering. There is an alternative to |e| called |expandf| which omits this check. Hence: #expandf INDIRECT_TAC;; OK.. "~((0 = 0) \/ (0 = 1)) ==> F" However if we then solve the goal #e(REWRITE_TAC[]);; OK.. goal proved |- ~((0 = 0) \/ (0 = 1)) ==> F then applying the proof function fails: #top_thm();; evaluation failed top_thm -- apply_proof -- CCONTR Hope this clarifies things. John.