Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <23308-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 15:33:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14856; Mon, 27 Jul 92 07:23:20 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA14851; Mon, 27 Jul 92 07:23:04 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <22923-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 15:20:50 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list) Subject: Re: How to prove this shortly? In-Reply-To: Your message of Fri, 24 Jul 92 16:43:18 +0700. <199207241443.AA21267@infix.cs.ruu.nl> Date: Mon, 27 Jul 92 15:20:40 +0100 From: John Harrison Message-Id: <"swan.cl.ca.930:27.06.92.14.21.03"@cl.cam.ac.uk> Wishnu Prasetya writes: I'm trying to prove the following goal: "!P:*->bool. !Q R (St:(*->bool)->(*->bool). (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)" I'm not satisfied with the proof I made since it is somewhat lengthy. The goal seems simple, there must be a cleverer way to prove it, so I thought. Perhaps anyone can suggest me a good one? Wai Wong and Victor Carreno suggest: REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC and Tom Melham suggests: REPEAT STRIP_TAC THEN REPEAT (FIRST_ASSUM MATCH_MP_TAC) THEN FIRST_ASSUM ACCEPT_TAC If you care about efficiency, you could try the following proof: REPEAT GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o GEN "s:*" o end_itlist IMP_TRANS o map (SPEC "s:*") o CONJUNCTS) although I wouldn't say it was very good style... essentially it's doing a forward proof thinly disguised as a backward one. John.