Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu
Subject: "X_EXISTS_TAC"
Date: Thu, 20 Jan 1994 11:24:33 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.741:20.00.94.10.24.36"@ira.uka.de>


Phil Windley wrote:
|> Of course, a conversion that proves permuting the variables doesn't change
|> the meaning would be as good.

I have written the following conversion for permuting existentially 
quantified variables in HOL90.


(* ******************** LINE_ORDER_CONV *******************************	*)
(* Given two lists lines1 and lines2 which contain the same variables	*)
(* but possibly in another order and a formula P, this conversion 	*)
(* proves that  |- ? lines1.P = ? lines2.P				*)
(* ********************************************************************	*)

structure O = Old_syntax

val NOT_NOT  = prove(--`!a.(~~a) = a`--,REWRITE_TAC[])


fun LINE_ORDER_CONV lines1 lines2 P =
    let fun list_mk_fun2bool_type [] = (==`:bool`==) |
    	    list_mk_fun2bool_type (t::l) = O.mk_type("fun",[t,(list_mk_fun2bool_type l)])
	fun EVERY_RULE [] th = th |
	    EVERY_RULE (r::rtl) th = EVERY_RULE rtl (r th)
	fun NOTNOT_CONV t = SPEC (dest_neg(dest_neg t)) NOT_NOT
	val PVAR = genvar (list_mk_fun2bool_type (map type_of lines1))
	val P0 =mk_neg(list_mk_comb(PVAR,lines1))
	fun ORDER_IMP_CONV lines1 lines2 P0 = 
	    let val P1 = list_mk_forall(lines1,P0)
		val P2 = CONTRAPOS(DISCH P1 (EVERY_RULE (map GEN (rev lines2)) 
							(SPEC_ALL(ASSUME P1))))
		val P3 = CONV_RULE (TOP_DEPTH_CONV NOT_FORALL_CONV) P2
	     in CONV_RULE (ONCE_DEPTH_CONV NOTNOT_CONV) P3
	    end
	val line_order_lemma = (GEN PVAR (IMP_ANTISYM_RULE 
					(ORDER_IMP_CONV lines2 lines1 P0)
			 		(ORDER_IMP_CONV lines1 lines2 P0)))
     in
	BETA_RULE(SPEC (list_mk_abs(lines1,P)) line_order_lemma)
    end