Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 15 Jun 1993 23:50:10 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12451; Tue, 15 Jun 93 15:39:25 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA12446; Tue, 15 Jun 93 15:39:19 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57659>; Wed, 16 Jun 1993 00:39:22 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8067>; Wed, 16 Jun 1993 00:39:15 +0200 From: Konrad Slind To: toal@cs.ucla.edu, info-hol@ted.cs.uidaho.edu In-Reply-To: Ray Toal's message of Tue, 15 Jun 1993 22:48:20 +0200 <9306152048.AA10755@makaha.cs.ucla.edu> Subject: A simple question Message-Id: <93Jun16.003915met_dst.8067@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 16 Jun 1993 00:39:02 +0200 Ray asks for a tactic meeting the following description; > ?x1 ... xn. t > ============================== NEW_EXISTS_TAC xi u > ?x1..x(i-1)x(i+1)..xn. t[u/xi] Off the top of my head, the following variant seems simple and NEW_EXISTS_TAC ought to be easy to build from it. It amounts to "bubbling" the desired bound variable to the front of the existential quantifier block then doing an EXISTS_TAC. The index of the bound variable is zero-based. > fun bring 0 = REFL > | bring n = funpow (n-1)(RAND_CONV o ABS_CONV) SWAP_EXISTS_CONV > THENC bring (n-1); > > fun EXISTS_NTH_TAC n tm = > CONV_TAC (bring n) THEN EXISTS_TAC tm; Examples. - top_goal(); (--`?x y z. x /\ y /\ z`--) ============================= - e (EXISTS_NTH_TAC 1 (--`F`--)); OK.. 1 subgoal: (--`?x z. x /\ F /\ z`--) ============================= - b(); (--`?x y z. x /\ y /\ z`--) ============================= - e (EXISTS_NTH_TAC 0 (--`F`--)); OK.. 1 subgoal: (--`?y z. F /\ y /\ z`--) ============================= - b(); (--`?x y z. x /\ y /\ z`--) ============================= - e (EXISTS_NTH_TAC 2 (--`F`--)); OK.. 1 subgoal: (--`?x y. x /\ y /\ F`--) =============================