[isabelle-dev] Evaluation of floor and ceiling

[Brian Huffman]

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.

The drawback to this design is that it requires yet another type
class, of which we have plenty already. The other alternative would be
to make floor into a parameter of class archimedean_field, replacing
the current axiom ex_le_of_int:

OLD:
class archimedean_field = linordered_field + number_ring +
  assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"

NEW:
class archimedean_field = ordered_field + number_ring +
  fixes floor :: "'a \<Rightarrow> int"
  assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int
(floor x + 1)"

One problem with this class definition is that floor_correct is a
stronger property than ex_le_of_int, and more difficult to prove
(especially for type real). To keep class instance proofs as easy as
they are now, Archimedean_Field.thy could provide a lemma like the
following:

lemma archimedean_field_class:
  assumes ex_le_of_int:
    "\<And>(x::'a::{ordered_field, number_ring}). \<exists>z. x \<le> of_int z"
  assumes floor_def:
    "\<And>(x::'a::{ordered_field, number_ring}).
      floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
  shows "OFCLASS('a::{ordered_field, number_ring}, archimedean_field_class)"

This second approach would be less trivial to implement, but it might
be worth it to keep everything in a single type class.

- Brian

On Thu, Jul 7, 2011 at 2:26 PM, Lukas Bulwahn <bulwahn at in.tum.de> wrote:
> 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?
>
>
> Lukas
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: floor.diff
Type: text/x-patch
Size: 2458 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110707/83e306ee/attachment-0002.bin>