Re: [isabelle] Strange counter example given by arith



>    lemma div_less_square: "[| x < n * n; 0 < n |] ==> x div n < (n::nat)";
> arith fails with the following counter example:

Multiplication and div are outside linear arithmetic and lead into
undecidable territory. Hence arith ignores them (except in special cases
involving numerals) which means that "n * n" and "x div n" are simply
regarded as new variables. In such cases one may get bogus counter examples.

Tobias





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