[isabelle-dev] quickcheck on type real

[Stefan Berghofer]

Amine Chaieb wrote:
> This is perhaps an occasion to advertise Library/Executable_real.thy, 
> which contains a verified implementation of rational numbers to be have 
> like HOL --- So here you would no get an exception when dividing by 
> zero, but just zero as you expect.
> 
> [...]
> 
> Brian Huffman wrote:
> 
>>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. 
>>[...]
>>
>>The other bug is a false counterexample; I have no idea what causes it:

Hello all,

the code generator setup contained in the theories Library/Executable_Real.thy
and Library/Executable_Rat.thy have now been integrated into the theories
Real/RealDef.thy and Real/Rational.thy. Moreover, I modified the setup in such
a way that it also works with the "old" code generator and therefore with
quickcheck, so the abovementioned bugs should now be fixed.

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe