[isabelle-dev] Evaluation of floor and ceiling

Lukas Bulwahn bulwahn at in.tum.de
Thu Jul 7 23:26:40 CEST 2011

Hi all,

Jasmin has pointed out that the evaluation of floor and ceiling showed 
surprising behaviour and I looked into the topic:

If we are interested to enable evaluation of terms such as "floor (5 / 6 
:: rat)" or "ceiling (1 / 2 :: real)", this will require different code 
equations for the different types -- hence the definition of floor and 
ceiling would have to be moved into the archimedian type class, and then 
one could provide actually different instantiations for the evaluation.
This seems like a non-trivial refactoring.

Is anyone interested to use evaluation for such terms which might 
motivate to do this refactoring?


More information about the isabelle-dev mailing list