Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 28 May 1993 11:53:50 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02637;
          Fri, 28 May 93 03:40:20 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02632;
          Fri, 28 May 93 03:40:00 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 28 May 1993 11:38:59 +0100
To: reetz <reetz@ira.uka.de>
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: Elemination of @-terms
In-Reply-To: Your message of "Fri, 28 May 93 09:42:55 +0700." <9305280943.AA02616@ted.cs.uidaho.edu>
Date: Fri, 28 May 93 11:38:53 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:253430:930528103912"@cl.cam.ac.uk>


Ralf Reetz writes:

> I would like to proof the following goal:
> 
> ([],--`(@m. ?vn. (m = F) /\ (vn = vn1)) = F`--);
> 
> I was already able to proof the following three
> goals:
> 
> TAC_PROOF (([],--`?m.?vn.(m=F) /\ (vn=vn1)`--),

You can derive the appropriate implication using SELECT_RULE as follows:

  - val THM = prove
  =   (--`(?m.?vn.(m=F) /\ (vn=vn1)) ==>
  =             ((@m. ?vn:'a. (m = F) /\ (vn = vn1)) = F)`--,
  =    DISCH_THEN(CHOOSE_TAC o SELECT_RULE) THEN 
  =    ASM_REWRITE_TAC[]);
  val THM =
    |- (?m vn. (m = F) /\ (vn = vn1)) ==> ((@m. ?vn. (m = F) /\ (vn = vn1)) = F)
    : thm

You could also use SELECT_CONV for this sort of thing, but you'd have to 
strengthen the goal (e.g. using SUBGOAL_THEN) so that it has the right 
form. In HOL88 version 2.02 I added the following two theorems, which 
I find quite useful for getting rid of @-terms:

  let SELECT_REFL = prove_thm(`SELECT_REFL`,
    "!x:*. (@y. y = x) = x",
    let th = BETA_RULE(SPEC "\y:*. y = x" SELECT_AX) in
    GEN_TAC THEN MATCH_MP_TAC th THEN EXISTS_TAC "x:*" THEN REFL_TAC);;

  let SELECT_UNIQUE = prove_thm(`SELECT_UNIQUE`,
    "!P x. (!y:*. P y = (y = x)) ==> ($@ P = x)",
    REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o HALF_MK_ABS) THEN
    MATCH_ACCEPT_TAC SELECT_REFL);;

Note that sometimes (maybe after using ETA_CONV first), you can just MATCH_MP_TAC 
with the characterizing theorem SELECT_AX.

John.