Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 20 Sep 1993 12:32:32 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA15201;
          Mon, 20 Sep 93 04:24:12 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA15197; Mon, 20 Sep 93 04:24:06 -0700
Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk;
          Mon, 20 Sep 93 11:55:52 BST
From: David Shepherd <des@inmos.co.uk>
Message-Id: <13659.9309201123@frogland.inmos.co.uk>
Subject: Re: a little proof challenge
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Mon, 20 Sep 1993 12:23:18 +0100 (BST)
In-Reply-To: <7637*joyce@cs.ubc.ca> from "Jeffrey Joyce" at Sep 8, 93 05:15:00 pm
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 1228

Jeffrey Joyce has said:
> "!P Q R.
>   !x:*. ?v. ?w. !y. !z:**.
>     ((P x /\ Q y) ==> ((P v \/ R w)  /\ (R z ==> Q v)))"

belatedly (i've been away for 3 weeks) here's a hol90 proof.
took about 10 minutes or so.

    prove(--`!P Q R.
	     !(x:'a). ?v. ?w. !y. !(z:'b).
	     ((P x /\ Q y) ==> ((P v \/ R w)  /\ (R z ==> Q v)))`--,
	  CONV_TAC(DEPTH_CONV FORALL_IMP_CONV)
	  THEN CONV_TAC(DEPTH_CONV EXISTS_IMP_CONV)
	  THEN REPEAT GEN_TAC
	  THEN STRIP_TAC
	  THEN CONV_TAC(DEPTH_CONV FORALL_AND_CONV)
	  THEN CONV_TAC(DEPTH_CONV EXISTS_AND_CONV)
	  THEN CONV_TAC(DEPTH_CONV FORALL_IMP_CONV)
	  THEN ASM_CASES_TAC(--`?(z:'b) . R z`--)
	  THENL 
	  [
	    POP_ASSUM STRIP_ASSUME_TAC
	    THEN EXISTS_TAC(--`y:'a`--)
	    THEN ASM_REWRITE_TAC[]
	    THEN EXISTS_TAC(--`z:'b`--)
	    THEN ASM_REWRITE_TAC[]
	   ,
	    EXISTS_TAC(--`x:'a`--)
	    THEN ASM_REWRITE_TAC[]
	  ]);


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley