[Hol-info] Procedure for equations with addition and multiplication

[Michael N. <Mic...@ni...>]

Alexey Gotsman writes:
 
> Does anyone know if there is a procedure in HOL for proving simple 
> statements about equations with addition and multiplication like the 
> following one?
 
> (e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum=bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 
> ==>        (2*e*bv_cout+e*wb_sum+wbs_sum=bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)
 
> Unfortunately, PROVE_TAC and RW_TAC arith_ss [] don't do the job.
 
Further to my last post, it's actually easy enough to get
multiplicative AC-normalisation happening in this goal using the
rewriter.  Then after applying distributivity, the d.p. inside
arith_ss solves the goal.

Again, assuming natural numbers, and that arithmeticTheory is "open",
use

  RW_TAC arith_ss [AC MULT_COMM MULT_ASSOC, LEFT_ADD_DISTRIB]

to solve the goal.  

Nonetheless, I still regard it as a bug that

* neither procedure does distributivity itself; and 
* numLib.ARITH_CONV doesn't normalise multiplicative terms

Michael.