Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: toal@edu.ucla.cs (Ray J. Toal)
Cc: info-hol@edu.uidaho.cs.ted
Subject: unwinding.
Date: Sat, 11 Jan 92 20:24:14 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.445:11.00.92.20.24.19"@cl.cam.ac.uk>

Regarding:

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

Attached is a special-purpose rule for doing this, extracted from
the latest version of the ind_defs library. It's pretty fast, and
HOL hackers may find it interesting to dissect.

Tom

=========================================================================

% --------------------------------------------------------------------- %
% INTERNAL FUNCTION : reduce                                            %
%                                                                       %
% A call to                                                             %
%                                                                       %
%   reduce [v1;...;vn] ths [] []                                        %
%                                                                       %
% reduces the list of theorems ths to an equivalent list by removing    %
% theorems of the form |- vi = ti where vi does not occur free in ti,   %
% first using this equation to substitute ti for vi in all the other    %
% theorems. The theorems in ths are processed sequentially, so for      %
% example:                                                              %
%                                                                       %
%   reduce [a;b] [|- a=1; |- b=a+2; |- c=a+b] [] []                     %
%                                                                       %
% is reduced in the following stages:                                   %
%                                                                       %
%   [|- a=1; |- b=a+2; |- c=a+b]                                        %
%                                                                       %
%   ===> [|- b=1+2; |- c=1+b]      (by the substitution [1/a])          %
%   ===> [|- c=1+(1+2)]            (by the substitution [1+2/b])        %
%                                                                       %
% The function returns the reduced list of theorems, paired with a list %
% of the substitutions that were made, in reverse order.  The result    %
% for the above example would be [|- c = 1+(1+2)],[("1+2",b);("1",a)].  %
% --------------------------------------------------------------------- %

letrec reduce vs ths res sub =
   if (null ths) then (rev res, sub) else
   (let l,r = dest_eq(concl(hd ths)) in
    let sth,pai = mem l vs => hd ths,(r,l) |
                  mem r vs => SYM(hd ths),(l,r) | fail in
    if free_in (snd pai) (fst pai) then fail else
    let sfn = map (SUBS [sth]) in
    let ssfn = map \(x,y). (subst [pai] x),y in
        reduce vs (sfn (tl ths)) (sfn res) (pai . ssfn sub)) ?
    (reduce vs (tl ths) (hd ths . res) sub);;

% --------------------------------------------------------------------- %
% REDUCE : simplify an existentially quantified conjuction by           %
% eliminating conjuncts of the form |- v=t, where v is among the        %
% quantified variables and v does not appear free in t. For example     %
% suppose:                                                              %
%                                                                       %
%   tm = "?vi. ?vs. C1 /\ ... /\ vi = ti /\ ... /\ Cn"                  %
%                                                                       %
% then the result is:                                                   %
%                                                                       %
%   |- (?vi. ?vs. C1 /\ ... /\ vi = ti /\ ... /\ Cn)                    %
%          =                                                            %
%      (?vs. C1[ti/vi] /\ ... /\ Cn[ti/vi])                             %
%                                                                       %
% The equations vi = ti can appear as ti = vi, and all eliminable       %
% equations are eliminated.  Fails unless there is at least one         %
% eliminable equation. Also flattens conjuncts. Reduces term to "T" if  %
% all variables eliminable.                                             %
% --------------------------------------------------------------------- %

let REDUCE =
    let chfn v (a,th) =
      let tm = mk_exists(v,a) in
      let th' =
          if (free_in v (concl th))
            then EXISTS (mk_exists(v,concl th),v) th else th in
         (tm,CHOOSE (v,ASSUME tm) th') in
    let efn ss v (pat,th) =
        let wit = fst(rev_assoc v ss) ? v in
        let epat = subst ss (mk_exists(v,pat)) in
            (mk_exists(v,pat),EXISTS(epat,wit) th) in
    letrec prove ths cs =
        (uncurry CONJ ((prove ths # prove ths) (dest_conj cs))) ?
        (find (\t. concl t = cs) ths) ?
        (REFL (rand cs)) in
    \tm. let vs,cs = strip_exists tm in
         let rem,ss = reduce vs (CONJUNCTS (ASSUME cs)) [] [] in
         if (null ss) then failwith `REDUCE` else
         let th1 = LIST_CONJ rem ? TRUTH in
         let th2 = (uncurry DISCH) (itlist chfn vs (cs,th1)) in
         let rvs,rcs = strip_exists(rand(concl th2)) in
         let eqt = subst ss cs in
         let th3 = prove (CONJUNCTS (ASSUME rcs)) eqt in
         let _,th4 = itlist (efn ss) vs (cs,th3) in
         let th5 = (uncurry DISCH) (itlist chfn rvs (rcs,th4)) in
             IMP_ANTISYM_RULE th2 th5;;