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.