[isabelle-dev] Evaluation of floor and ceiling

[Lukas Bulwahn]

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
> patch.
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.

Lukas