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; Wed, 25 Aug 1993 11:00:29 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02217;
          Wed, 25 Aug 93 02:56:14 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA02213; Wed, 25 Aug 93 02:56:10 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 25 Aug 1993 10:55:12 +0100
To: schneide <schneide@ira.uka.de>
Cc: info-hol@dworshak.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: SELECT_EXISTS_TAC
In-Reply-To: Your message of "Wed, 25 Aug 93 08:57:27 +0700." <"iraun1.ira.416:25.07.93.06.55.21"@ira.uka.de>
Date: Wed, 25 Aug 93 10:55:01 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:153680:930825095529"@cl.cam.ac.uk>


Klaus asks:

> ----------------------------------------------------------------------
> However, I am not sure, if the subgoal of this tactic is equivalent
> to the original goal. 
> 
> Is there any proof for the theorem:
> 
> |- !P Q. Q(@x.P x) ==> ((?x:'a.P x) => !y. P y ==> Q y | !y.Q y) 
> ----------------------------------------------------------------------

The answer is `no'.  See the attached proof script.

Tom

=====================================================================

new_theory `bad`;;

let bad = 
    new_axiom 
     (`bad`, 
      "!P Q. Q(@x:*.P x) ==> 
             ((?x.P x) => (!y. P y ==> Q y) | !y.Q y)");;

let thm1 = REWRITE_RULE [] (BETA_RULE (SPEC "\x:*.F" bad));;

let thm2 = INST_TYPE [":bool", ":*"] thm1;;

let thm3 = SPEC "\y:bool. y = @x:bool.F" thm2;;

let thm4 = REWRITE_RULE [] (BETA_RULE thm3);;

let thm5 = SPEC "~ (@x.F)" thm4;;

let thm6 = PROVE ("~(~b = b)", BOOL_CASES_TAC "b:bool" THEN REWRITE_TAC[]);;

let fthm = MATCH_MP thm6 thm5;;   % this proves |- F %