Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Tue, 7 Jan 92 07:51:38 -0800
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9201071551.AA29698@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted


Has anyone a rule (or conversion?) for the following?

I would like to remove all existentially quantified variables (xi)
in a theorem that appear free in a subterm "t = xi" of the body.
For example, from

  |-  ?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)

one should obtain

  |-  ?x z. f b ==> g z a x

I hope that this is an interesting problem and that I am not incorrect
in thinking that it is logically possible.  It may even be easy.
The following (inefficient) function may be of use:

%--------------------------------------------------------------%
%  Rotate the bound variables in an existential quantification %
%                                                              %
%  SIFT_EXISTS_CONV "?x1 x2 ... xn. t" =                       %
%    |- "(?x1 x2 ... xn. t) = ?xn x1 x2 ... xn-1. t"           %
%--------------------------------------------------------------%

let BINDER_CONV c = RAND_CONV (ABS_CONV c) ;;

letrec SIFT_EXISTS_CONV t =
  let bvars = length (fst (strip_exists t)) in
  if bvars < 2 then ALL_CONV t
  else if bvars = 2 then SWAP_EXISTS_CONV t
  else (BINDER_CONV SIFT_EXISTS_CONV THENC SWAP_EXISTS_CONV) t ;;


Gracias Spasibo Danke Tak Kiitos Dzi\c{e}kuj\c{e} {Dank U}
Obrigado Thanks Hvala Tack Merci Grazie Takk

Ray Toal
toal@cs.ucla.edu