[isabelle-dev] Evaluation of floor and ceiling
bulwahn at in.tum.de
Sat Jul 9 19:51:54 CEST 2011
On 07/08/2011 03:13 AM, Brian Huffman wrote:
> I wrote to Florian about this exact issue back in February 2010.
> Florian's recommended solution at the time was to add a new subclass
> of archimedean_field that fixes the floor function and assumes a
> correctness property about it. This solution is really easy to
> implement (see attached diff). If people think this is a reasonable
> design, then I'll let someone else go ahead and test and commit the
I think it is reasonable, so I added your changeset and set up the code
generator and added a simple test case for quickcheck showing that we
can evaluate floor and ceiling now.
These preliminary changesets can be inspected under
http://isabelle.in.tum.de/testboard/Isabelle, and I will push them into
the mainstream repository, once the tests ran through.
@Brian: Thanks for your effort.
More information about the isabelle-dev