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; Tue, 2 Mar 1993 11:12:49 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06207; Tue, 2 Mar 93 02:58:02 -0800 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 AA06202; Tue, 2 Mar 93 02:57:54 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 2 Mar 1993 10:57:10 +0000 To: blok@nl.utwente.cs (Rintcius Blok) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: pair proof In-Reply-To: Your message of Tue, 02 Mar 93 11:14:23 +0100. <9303021014.AA00306@apollo.cs.utwente.nl> Date: Tue, 02 Mar 93 10:57:02 +0000 From: John Harrison Message-Id: <"swan.cl.ca.273:02.03.93.10.57.17"@cl.cam.ac.uk> Rintcius Blok asks: > I have a problem with proving the following goal: > > g "!P.(!(x:*) (y:**).x IN X /\ y IN Y==>P(x,y))= > (!z.(FST z) IN X /\ (SND z) IN Y ==>P z)";; > > I think the proof is not difficult and can be very short, > but I cannot find/derive an appropriate theorem to "jump" from > the first pair repr. to the second. > > Is there anyone who can help? I think the following proof works (there may be neater ways): load_library `sets`;; let th = PROVE ("!P.(!(x:*) (y:**).x IN X /\ y IN Y==>P(x,y))= (!z.(FST z) IN X /\ (SND z) IN Y ==>P z)", GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN GEN_TAC THEN SUBST1_TAC(SYM(SPEC "z:*#**" PAIR)) THEN PURE_ASM_REWRITE_TAC[FST; SND]; REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);; John.