Hello all, I would like to report some bugs I found when using quickcheck on lemmas involving division on reals. When auto_quickcheck is enabled (which it is by default) these bugs cause the "lemma" command to fail, preventing me from even attempting a proof.
The first bug is that sometimes quickcheck fails with a DIVZERO exception. This could probably be fixed by changing rat.ML to return zero when dividing by zero. ML {* Codegen.auto_quickcheck := false; *} lemma "(a::real) = 1 / (1 / a)" quickcheck *** DIVZERO *** At command "quickcheck". The same error is also appears with other, more useful lemmas like this one: lemma real_divide_cancel_lemma: "(b = 0 ==> a = 0) ==> (a / b::real) * (b / c) = a / c" The other bug is a false counterexample; I have no idea what causes it: lemma "inverse (a::real) = (1 / a)" quickcheck Test data size: 0 Test data size: 1 Counterexample found: a = -1 I am using the current CVS version of Isabelle, by the way. - Brian