|
From: Joe H. <joe...@co...> - 2005-10-20 20:01:33
|
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 > |