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

[Joe H. <joe...@co...>]

It seems that METIS_TAC [] (an alternative to PROVE_TAC [] better on
hard equality problems) also gets bogged down in your problem :-(

I'd recommend proving an intermediate step between the hypothesis and
conclusion of your implication, which is

e*bv_c + A =3D e*bv_c + B

where A =3D B is the conclusion. I haven't tried it, but RW_TAC loaded
with AC simpsets for + and * together with the rewriting theorem
LEFT_ADD_DISTRIB (which |- !m n p. p * (m + n) =3D p * m + p * n) should
plug the gap between hypothesis and intermediate step. To get from
intermediate step to conclusion you'll need the rewrite theorem
EQ_ADD_LCANCEL (which is |- !m n p. (m + n =3D m + p) =3D (n =3D p)).

I do this kind of reasoning all the time, and would also welcome
improvements and advice from the HOL community.

Joe

On 10/20/05, Alexey Gotsman <ov...@ca...> wrote:
> Hi everyone,
>
> 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=3Dbv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wb=
s_b)
> =3D=3D>        (2*e*bv_cout+e*wb_sum+wbs_sum=3Dbv_cin+e*wb_a+e*wb_b+wbs_a=
+wbs_b)
>
> Unfortunately, PROVE_TAC and RW_TAC arith_ss [] don't do the job.
>
> Best regards,
> Alexey Gotsman
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by:
> Power Architecture Resource Center: Free content, downloads, discussions,
> and more. http://solutions.newsforge.com/ibmarch.tmpl
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>