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 08:03:27 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02177;
          Tue, 24 Aug 93 23:55:37 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA02173; Tue, 24 Aug 93 23:55:25 -0700
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <17412-0@iraun1.ira.uka.de>; Wed, 25 Aug 1993 08:55:12 +0200
Date: Wed, 25 Aug 93 8:57:27 MET DST
From: schneide <schneide@ira.uka.de>
To: info-hol@dworshak.cs.uidaho.edu
Subject: SELECT_EXISTS_TAC
Message-Id: <"iraun1.ira.416:25.07.93.06.55.21"@ira.uka.de>

Hello all,
  recently I had some trouble with a goal which contained 
a term with the choice operator. The tactics available in
HOL only deal with terms of the form P(@x.P x), but I had
a goal of the form Q(@x.P x). I solved the problem with
the following tactic, which I think is quite useful:

(* ******************* SELECT_EXISTS_TAC **********************	*)
(*								*)
(* 			G |- Q(@x.P x)				*)
(*		===================================		*)
(* 		G |- ?x.P x	G |- !y.P y ==> Q y		*)
(*								*)
(* The term @x.P x has to be given as argument. The tactic will	*)
(* then eliminate this term in Q and the subgoals above are 	*)
(* obtained. This tactic only makes sense if G|-?x.P x holds.	*)
(* ************************************************************	*)

The hol90 code for this tactic is:


fun MP2_TAC th ((asm,g):goal) =
    let val {ant=s,conseq=t} = dest_imp(concl th)
     in ([(asm,s)],fn [t]=> MP th t)
    end


fun SELECT_EXISTS_TAC t (asm,g) =
    let val SELECT_EXISTS_THM = TAC_PROOF( 
	    ([],--`!P Q. (?x:'a. P x) /\ (!y. P y ==> Q y) ==> Q(@x.P x)`--),
	    REPEAT GEN_TAC 
	    THEN SUBST1_TAC(SYM(SELECT_CONV(--`P(@x:'a.P x)`--)))
	    THEN STRIP_TAC THEN RES_TAC)
	val {Bvar=x,Body=Px} = dest_select t
	val P = mk_abs{Bvar=x,Body=Px}
	val y = genvar(type_of x)
	val Q = mk_abs {Bvar=y,Body=subst[{redex=t,residue=y}]g}
	val lemma1 = INST_TYPE[{redex=(==`:'a`==),residue=(type_of x)}] 
							SELECT_EXISTS_THM
	val lemma2 = BETA_RULE(SPECL[P,Q]lemma1)
     in
	(MP2_TAC lemma2 THEN CONJ_TAC)(asm,g)
    end


If G|-?x.P x does not hold, the tactic makes no sense. In this case I would
suggest the following more general tactic :

(* *********************** SELECT_TAC *************************	*)
(*								*)
(*			G |- Q(@x.P x)				*)
(* 	   ==========================================		*)
(*	    G |-(?x.P x) => !y. P y ==> Q y | !y.Q y		*)
(*								*)
(* ************************************************************	*)



fun SELECT_TAC t (asm,g) =
    let val SELECT_THM = TAC_PROOF( 
	    ([],--`!P Q. ((?x:'a.P x) => !y. P y ==> Q y | !y.Q y) ==> Q(@x.P x) `--),
	    REPEAT GEN_TAC
	    THEN DISJ_CASES_TAC(SPEC(--`?x:'a.P x`--)BOOL_CASES_AX) 
	    THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
	    THENL[APPLY_ASM_TAC 1 (SUBST1_TAC(SYM(SELECT_CONV (--`P(@x:'a.P x)`--)))) 
		  THEN RES_TAC THEN ASM_REWRITE_TAC[],
		  ASM_REWRITE_TAC[]])
	val {Bvar=x,Body=Px} = dest_select t
	val P = mk_abs{Bvar=x,Body=Px}
	val y = genvar(type_of x)
	val Q = mk_abs {Bvar=y,Body=subst[{redex=t,residue=y}]g}
	val lemma1 = INST_TYPE[{redex=(==`:'a`==),residue=(type_of x)}] 
							SELECT_THM
	val lemma2 = BETA_RULE(SPECL[P,Q]lemma1)
     in
	(MP2_TAC lemma2 THEN COND_CASES_TAC)(asm,g)
    end


----------------------------------------------------------------------
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) 
----------------------------------------------------------------------

Cheers, 
	Klaus