# Re: [isabelle] Use of simp add:

`In response to my submission, Lars Noschinski wrote: 'The goal "2*x
``~= 3" is a bit tricky for automated tools: The reasoning is that 2*x
``is even and 3 is odd. However, neither "even" nor "odd" is mentioned
``in the goal.' But a proof that "2*x ~= 3" by reference to even and
``odd doesn't generalize in even simple ways, such as "3*x ~= 5".
``The real solution, it would appear to me, is that ax=b (for the free
``variable x, and constant natural numbers a and b) should simplify to
``b mod a = 0. Since a and b are constants, this should be easy to
``check. Similarly, ax ~= b should simplify to b mod a ~= 0. For "2*x
``~= 3", this would simplify to 3 mod 2 ~= 0, or 1 ~= 0. -Douglas
`--
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*