Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
To: Phil Windley <windley@leopard.cs.byu.edu>
Cc: info-hol@cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk
Subject: Re: X_EXISTS_TAC
In-Reply-To: Your message of "Wed, 19 Jan 94 20:41:43 MST." <"swan.cl.cam.:119310:940120035950"@cl.cam.ac.uk>
Date: Thu, 20 Jan 94 09:26:13 +0000
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:230770:940120092627"@cl.cam.ac.uk>

Hi, Phil,

	I have a tactic, namely EXISTS_PERM_TAC, which does the
following

	?- ? x1 ... xn. t[x1 ... xn]
       ================================ EXISTS_PERM_TAC[xi...xj]
        ?- ?xi ... xj ... . t[x1 ... xn]

It changes an existentially quantified goal to a new goal whose
quantified variables are a permutation of the old goal.

	You can define X_EXISTS_TAC in term this and EXISTS_TAC.
For example,

let X_EXISTS_TAC v wit = EXISTS_PERM_TAC [v] THEN EXISTS_TAC wit;;

I'm including the file which contains the source codes of
EXISTS_PERM_TAC, together with some other useful rules, conversions
and tactics performing permutation of variables at the end of this
message. Hope this will help you.

	By the way, when will you be able to release the source of
the WWW HOL documents so we can install a copy here to serve this
side of the atlantic.

Wai

------------------included file ----------------
%<----------------------------------------------------------------
  Permutaion of universal quatifications

   FORALL_PERM_RULE : term list -> thm -> thm
      |- ! x0 ... xn. t[x0,...,xn]
   ---------------------------------- FORALL_PERM_RULE [xi;...;xj]
    |- ! xi ... xj .... t[x0,...,xn]
  The resulting theorem has the same universal quatifications as
  the input theorem but in the order specified by the argument
  term list. The terms in the list must all be variables and they
  must appear in the input theorem.

   FORALL_PERM_CONV : term list -> conv
   FORALL_PERM_CONV [xi;...;xj] !x0 ... xn. t[x0,...,xn] ---> 
    |- ! xi ... xj .... t[x0,...,xn]
   This conversion is similar to the above inference rule.

   FORALL_PERM_TAC : term list -> tactic
      ?- !x0 ... xn. t[x0,...,xn]
   ================================== FORALL_PERM_TAC [xi;...;xj]
    ?- ! xi ... xj .... t[x0,...,xn]
   This tactic is similar to the above inference rule.
---------------------------------------------------------------->%

begin_section `Q_PERM`;;

let chk_var vl v = (is_var v & (mem v vl)) ;;

let FORALL_PERM_RULE = 
  \tms thm.
    let vs = (fst o strip_forall) (concl thm) in
    if (forall (chk_var vs) tms) then
        let vs' = subtract vs tms in (GENL (tms @ vs')(SPEC_ALL thm))
    else failwith `not all variables are quantified`
 ?\s failwith (`FORALL_PERM_RULE: `^s);;

let FORALL_PERM_CONV = 
    let forall_perm_rule = \tms thm. GENL tms (SPEC_ALL thm) in
  \tms tm.
    let (vs,body) =  strip_forall tm in
    if (forall (chk_var vs) tms) then
        let vs' = tms @ (subtract vs tms) in 
    	let th1 = DISCH_ALL (forall_perm_rule vs' (ASSUME tm)) in
    	let th2 = DISCH_ALL (forall_perm_rule vs
    	     (ASSUME(list_mk_forall(vs',body)))) in
    	(IMP_ANTISYM_RULE th1 th2)
    else failwith `not all variables are quantified`
     ?\s failwith (`FORALL_PERM_CONV: `^s);;

let FORALL_PERM_TAC = 
  \tms (asm,gl).
    CONV_TAC (FORALL_PERM_CONV tms) (asm,gl);;


%<----------------------------------------------------------------
  Permutaion of existential quatifications

   EXISTS_PERM_RULE : term list -> thm -> thm
      |- ? x0 ... xn. t[x0,...,xn]
   ---------------------------------- EXISTS_PERM_RULE [xi;...;xj]
    |- ? xi ... xj .... t[x0,...,xn]
  The resulting theorem has the same existential quatifications as
  the input theorem but in the order specified by the argument
  term list. The terms in the list must all be variables and they
  must appear in the input theorem.

   EXISTS_PERM_CONV : term list -> conv
   EXISTS_PERM_CONV [xi;...;xj] ?x0 ... xn. t[x0,...,xn] ---> 
    |- ? xi ... xj .... t[x0,...,xn]
   This conversion is similar to the above inference rule.

   EXISTS_PERM_TAC : term list -> tactic
      ?- ?x0 ... xn. t[x0,...,xn]
   ================================== EXISTS_PERM_TAC [xi;...;xj]
    ?- ? xi ... xj .... t[x0,...,xn]
   This tactic is similar to the above inference rule.

    The code was originally written by I.S.Dhingra, and forward
    to me by Brian Graham. I added the variable checking to make
    sure the variables suppied by the user all occur in the input
    theorem.
---------------------------------------------------------------->%
let EXISTS_PERM_RULE tms th =
    let old_l,tm = strip_exists (concl th) in
    if (forall (chk_var old_l) tms) then
      let new_l = tms @ (subtract old_l tms) in
      letrec build_exists l thm =      % note: builds exists in rev order%
        (null l) => thm
                  | build_exists
                      (tl l)
                      (EXISTS ("?^(hd l). ^(concl thm)", (hd l)) thm) in
      let new_thm = build_exists (rev new_l) (ASSUME tm) in
      letrec build_result l old_tm old_thm new_thm =
        (length l=0)=>MP (DISCH (concl old_thm) new_thm) old_thm |
        (length l=1)=>CHOOSE ((hd l), old_thm) new_thm    |
                      let tm' = mk_exists ((hd l), old_tm)
                      in
                      build_result (tl l)
                                   tm'
                                   old_thm 
                                   (CHOOSE ((hd l),(ASSUME tm')) new_thm)
      in
      build_result (rev old_l) tm th new_thm
    else failwith `not all variables are quantified`
     ?\s failwith (`EXISTS_PERM_RULE: `^s);;

let EXISTS_PERM_CONV tms t =
   let (vs,body) = strip_exists t in
   if (forall (chk_var vs) tms) then
     let new_l = tms @ (subtract vs tms) in
     let th1 = EXISTS_PERM_RULE new_l (ASSUME t) in
     let t' = concl th1 in
     let th2 = EXISTS_PERM_RULE vs (ASSUME t') in
     (IMP_ANTISYM_RULE (DISCH t th1) (DISCH t' th2))
   else failwith `not all variables are quantified`
   ?\s failwith (`EXISTS_PERM_CONV: `^s);;

let EXISTS_PERM_TAC = 
  \tms (asm,gl).
    CONV_TAC (EXISTS_PERM_CONV tms) (asm,gl);;

(FORALL_PERM_RULE,FORALL_PERM_CONV,FORALL_PERM_TAC,
EXISTS_PERM_RULE,EXISTS_PERM_CONV,EXISTS_PERM_TAC);;
end_section `Q_PERM`;;

let (FORALL_PERM_RULE,FORALL_PERM_CONV,FORALL_PERM_TAC,
  EXISTS_PERM_RULE,EXISTS_PERM_CONV,EXISTS_PERM_TAC) = it;;

----------------------end of included file ----------------