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
*** DIVZERO
*** At command quickcheck.
I also ran into this one (and notified Stefan).
lemma inverse (a::real) = (1 / a)
Counterexample found:
a = -1
I love it, a false counterexample to a false thm ;-)
Thanks!
Tobias
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.
Florian integrated this into the CVS to work with
