Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 11:34:49 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24853; Thu, 9 Sep 93 03:29:32 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA24849; Thu, 9 Sep 93 03:29:30 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA19076; Thu, 9 Sep 93 03:29:31 -0700 Message-Id: <9309091029.AA19076@maui.cs.ucla.edu> To: info-hol@cs.uidaho.edu Subject: Re: a little proof challenge Cc: borm@cs.ubc.ca Date: Thu, 09 Sep 93 03:29:30 PDT From: chou@cs.ucla.edu The following tactic solves Jeff's challenge in HOL90: REPEAT GEN_TAC THEN CONV_TAC SWAP_EXISTS_CONV THEN ASM_CASES_TAC (--`(?t:'b. R t)`--) THENL [ ASSUME_TAC (SELECT_RULE (ASSUME (--`(?t:'b. R t)`--))) THEN EXISTS_TAC (--`(@t:'b. R t)`--) THEN ASM_REWRITE_TAC [] THEN ASM_CASES_TAC (--`(?s:'a. Q s)`--) THENL [ ASSUME_TAC (SELECT_RULE (ASSUME (--`(?s:'a. Q s)`--))) THEN EXISTS_TAC (--`(@s:'a. Q s)`--) THEN ASM_REWRITE_TAC [] , RULE_ASSUM_TAC (CONV_RULE (TRY_CONV NOT_EXISTS_CONV)) THEN ASM_REWRITE_TAC [] ] , RULE_ASSUM_TAC (CONV_RULE (TRY_CONV NOT_EXISTS_CONV)) THEN ASM_REWRITE_TAC [] THEN ASM_CASES_TAC (--`(?r:'a. P r)`--) THENL [ ASSUME_TAC (SELECT_RULE (ASSUME (--`(?r:'a. P r)`--))) THEN EXISTS_TAC (--`(@r:'a. P r)`--) THEN ASM_REWRITE_TAC [] , RULE_ASSUM_TAC (CONV_RULE (TRY_CONV NOT_EXISTS_CONV)) THEN ASM_REWRITE_TAC [] ] ] At first I tried FAUST_TAC. It did not come back after 15 min. So I killed it, looked at the goal for 15 min, and then spent 20 min with the subgoal package to solve the goal. Too bad there's no automatic tool that could help me. - Ching Tsun