Re: [isabelle] Counterexamples produced by arith method



> Counter example:
> a * a div a = 2, a = 1

Remember that arith is *linear* arithmetic only, i.e. no multiplication or
division (except for n*x, x div n or x mod n, where n is a numeral).
Hence such subterms are treated as atomic. If the generalised goal is
provable, great. If not, the counterexample may be spurious, as in your
case. But Isabelle has no way to check this (it is again undecidable).
But showing you the "counterexample" will give you the chance to figure out
if it is a real one or a fake one. In the latter case you know that the goal
may still be true but is beyond linear arithmetic.

Tobias





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