Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Wed, 7 Apr 1993 00:22:55 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29821;
          Tue, 6 Apr 93 16:00:43 -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 AA29816;
          Tue, 6 Apr 93 16:00:28 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 7 Apr 1993 00:00:10 +0100
To: Wishnu Prasetya <wishnu@nl.ruu.cs>
Cc: info-hol@edu.uidaho.cs.ted (hol mailing list)
Subject: Re: How to STRIP/GEN forall with paired dummy??
In-Reply-To: Your message of Tue, 06 Apr 93 18:49:40 +0100. <199304061649.AA02305@infix.cs.ruu.nl>
Date: Wed, 07 Apr 93 00:00:05 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.237:06.04.93.23.00.13"@cl.cam.ac.uk>


Hi,

> Can anyone help me as to how to strip or generalize the following goal:
>
>    "!(p,q,r). p ==> (q==>p)"

The easy way is to use the pair library, if you have it. Alternatively I give
below a crude way to convert the goal into a separately quantified one. (I
assume you meant r in the inner implication, but that's not really germane.)

let WISHNU = PROVE
 ("!(p,q,r). p ==> (q ==> r)",
  SUBGOAL_THEN "!p q r. p ==> (q ==> r)" (\th. REWRITE_TAC[th]) THENL
   [ALL_TAC;
    ONCE_REWRITE_TAC[(SYM o RAND_CONV ETA_CONV) "!x:*. P x"] THEN GEN_TAC THEN
    GEN_REWRITE_TAC (\c. RAND_CONV c THENC (funpow 2 RAND_CONV) c) []
     [GSYM PAIR] THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV)] THEN
  .....

John.