Message-Id: <8809022359.AA00633@cheetah.ucdavis.edu>
Pointers: (916) 752-7324/3168
To: info-hol@clover.ucdavis.edu
Cc: lcp%computer-lab.cambridge.ac.uk@NSS.Cs.Ucl.AC.UK
Subject: ADD_NORMALIZE_TAC
Date: Fri, 02 Sep 88 16:59:28 -0800
From: windley@cheetah.ucdavis.edu (Phil Windley)

A couple of days ago, I mailed a request for help on associativity and
commutivity in proofs.  Mike Gordon responded with a tactic that worked for
things like this:

   (a + (b + c) + (d + e) + f) + g = (b + d) + (a + c) + ((f + g) + e)

However it only worked when a, b, etc were single letter variables.  What
I really wanted was to do things like:

   "((bv_to_nat w a) + ((bv_to_nat w b) + (bv cin))) +
            (((2 EXP (SUC w)) * (bv(a(SUC w)))) +
              ((2 EXP (SUC w)) * (bv(b(SUC w))))) =
         ((bv_to_nat w a) + ((2 EXP (SUC w)) * (bv(a(SUC w))))) +
      (((bv_to_nat w b) + ((2 EXP (SUC w)) * (bv(b(SUC w))))) + (bv cin))"

I modified his work to allow a, b, etc to be terms, rather than single
letter variables.  I have included it here.  Please excuse the ML, I'm
afraid I'm still a little clumsy, but I've tested it on some rather
complicated stuff and it seems to work.

A MULT_NORMALIZE_TAC would follow easily from this, but it be nicer to
write a tactic that is given a function and then determines if commutivity
and associativity hold for that function and forms an appropriate
conversion.

Anyway, thanks to Mike Gordon for the shove in the right direction.  I'd
appreciate hearing of any problems/ improvements to this.
________________________________________________________________________
Phil Windley                          |  windley@iris.ucdavis.edu
Division of Computer Science          |  ucbvax!ucdavis!iris!windley
College of Engineering                |  (916) 752-7324 (or 3168)
University of California, Davis       |  Davis, CA 95616


------------- cut here --------------------------------------------
%
 ADD_NORMALIZE_TAC --
 original by Mike Gordon; extended by Phil Windley
%


% ADD3_SYM = |- !a b c. (a + b) + c = (a + c) + b     %

let ADD3_SYM =
 TAC_PROOF
  (([], "!a b c. (a+b)+c = (a+c)+b"),
   REPEAT GEN_TAC
    THEN REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)]
    THEN SUBST_TAC[SPECL["b:num";"c:num"]ADD_SYM]
    THEN REFL_TAC);;

let const_name  = fst o dest_const;;

let is_plus_term t =
   if is_comb t & ((const_name (fst (strip_comb t))) = `+`) then
      true
   else
      false;;

% is l1 less than l2 ? %
letrec lst_less (l1: int list) (l2: int list) = (
    if null l1 & not null l2 then
        true
    else if null l2 then
        false
    else if ((hd l1) < (hd l2)) then
        true
    else if ((hd l1) > (hd l2)) then
        false
    else
        lst_less (tl l1) (tl l2));;

% is s1 less than s2 ? %
let str_less (s1:string) (s2:string) =
   lst_less (map ascii_code (explode s1))
            (map ascii_code (explode s2));;

% convert a term to a prefix string %
letrec term_to_str t =
   if is_comb t then
      let op,tlst = strip_comb t in (
         if is_const op then
            ((const_name op)^(concatl (map term_to_str tlst)))
         else if is_var op then
            ((var_name op)^(concatl (map term_to_str tlst)))
         else
            fail)
   else if (is_var t) then
      (var_name t)
   else if (is_const t) then
      (const_name t)
   else
      fail;;


% << is an arbitrary total ordering over terms %
ml_curried_infix `<<`;;
let t1 << t2 = (str_less (term_to_str t1) (term_to_str t2));;


%
   ADD_SYM_CONV "a+b"      --> |- a+b     = b+a       if b << a
   ADD_SYM_CONV "(a+b)+c"  --> |- (a+b)+c = (a+c)+b   if c << b

%

let ADD_SYM_CONV t =
 let op1,[t1;t2] = strip_comb t
 in
 if op1 = "$+" & not (is_plus_term t1) & (t2 << t1)    % t=a+b %
  then SPECL[t1;t2]ADD_SYM
  else
   (let op2,[t3;t4] = strip_comb t1
    in
    if op1 = "$+" & op2 = "$+" & (t2 << t4)                % t=(a+b)+c %
     then SPECL[t3;t4;t2]ADD3_SYM
     else fail);;


%
   ADD_ASSOC_CONV "a+(b+c)"  --> |- a+(b+c) = (a+b)+c
%

let ADD_ASSOC_CONV t =
 let op1,[t1;t2] = strip_comb t
 in
 let op2,[t3;t4] = strip_comb t2
 in
 if op1 = "$+"  & op2 = "$+"
  then SPECL[t1;t3;t4]ADD_ASSOC
  else fail;;

let ADD_NORMALIZE_CONV =
 TOP_DEPTH_CONV ADD_ASSOC_CONV
  THENC TOP_DEPTH_CONV ADD_SYM_CONV;;

let ADD_NORMALIZE_TAC =
 CONV_TAC ADD_NORMALIZE_CONV
  THEN REFL_TAC;;

% Example

#timer true;;
() : void
Run time: 0.1s
Garbage collection time: 0.0s

let Th =
 TAC_PROOF
  (([], "((((a + (b + a)) + (d + e)) + e) + f) + h =
         a + ((e + f) + ((e + (d + (b + a))) + h))"),
   ADD_NORMALIZE_TAC);;
Th =
|- ((((a + (b + a)) + (d + e)) + e) + f) + h =
   a + ((e + f) + ((e + (d + (b + a))) + h))
Run time: 11.0s
Garbage collection time: 3.5s
Intermediate theorems generated: 883

let Th1 = TAC_PROOF(
     ([], "((((ask + (bee + a)) + (deer + e)) + e) + f) + h =
           ask + ((e + f) + ((e + (deer + (bee + a))) + h))"
     ), ADD_NORMALIZE_TAC);;


let Th2 = TAC_PROOF(
     ([], "(((((a * 2) + (bee + a)) + (deer + (e * 2))) + e) + f) + h =
         (a * 2) + ((e + f) + (((e * 2) + (deer + (bee + a))) + h))"
     ), ADD_NORMALIZE_TAC);;


---------------------------------------------------------------------------
  This next one won't work unless all the terms are defined, but it shows
  what I was doing that prompted this.
---------------------------------------------------------------------------

let Th3 = TAC_PROOF(
    ([],"((bv_to_nat w a) + ((bv_to_nat w b) + (bv cin))) +
            (((2 EXP (SUC w)) * (bv(a(SUC w)))) +
              ((2 EXP (SUC w)) * (bv(b(SUC w))))) =
         ((bv_to_nat w a) + ((2 EXP (SUC w)) * (bv(a(SUC w))))) +
      (((bv_to_nat w b) + ((2 EXP (SUC w)) * (bv(b(SUC w))))) + (bv cin))"
    ), ADD_NORMALIZE_TAC);;


%