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, 27 Sep 1993 19:40:14 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03656;
          Mon, 27 Sep 93 11:24:27 -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 AA03650; Mon, 27 Sep 93 11:24:19 -0700
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <12475-0@iraun1.ira.uka.de>; Mon, 27 Sep 1993 19:23:47 +0100
Date: Mon, 27 Sep 93 19:26:18 MET
From: schneide <schneide@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: SELECT_TAC
Message-Id: <"iraun1.ira.479:27.08.93.18.23.59"@ira.uka.de>

Some time ago I suggested a tactic called SELECT_TAC
in order to eliminate arbitrary select operators.
However, I gave an implementation with a function which
I haven't described. So some people asked about the 
complete implementation. For this reason, I list the
entire implementation in HOL90 below:


(* *********************** MP2_TAC ****************************	*)
(*       A ?- t							*)
(*   ==============  MP2_TAC (A' |- s ==> t)			*)
(*    A ?- s 							*)
(*								*)
(* ************************************************************	*)

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

(* ******************* 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.	*)
(* Otherwise the tactic below should be used.			*)
(* ************************************************************	*)

fun SELECT_EXISTS_TAC t (asm,g) =
    let val SELECT_ELIM_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_ELIM_THM
	val lemma2 = BETA_RULE(SPECL[P,Q]lemma1)
     in
	(MP2_TAC lemma2 THEN CONJ_TAC)(asm,g)
    end



(* *********************** 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[RULE_ASSUM_TAC (REWRITE_RULE [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