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 <[email protected]> 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
> [email protected]
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
diff -r 47b0be18ccbe src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy Thu Jul 07 23:33:14 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy Thu Jul 07 17:45:45 2011 -0700
@@ -141,9 +141,9 @@
subsection {* Floor function *}
-definition
- floor :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+class floor_ceiling = archimedean_field +
+ fixes floor :: "'a \<Rightarrow> int"
+ assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
@@ -151,9 +151,6 @@
notation (HTML output)
floor ("\<lfloor>_\<rfloor>")
-lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
- unfolding floor_def using floor_exists1 by (rule theI')
-
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
using floor_correct [of x] floor_exists1 [of x] by auto
@@ -273,7 +270,7 @@
subsection {* Ceiling function *}
definition
- ceiling :: "'a::archimedean_field \<Rightarrow> int" where
+ ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
[code del]: "ceiling x = - floor (- x)"
notation (xsymbols)
diff -r 47b0be18ccbe src/HOL/Rat.thy
--- a/src/HOL/Rat.thy Thu Jul 07 23:33:14 2011 +0200
+++ b/src/HOL/Rat.thy Thu Jul 07 17:45:45 2011 -0700
@@ -739,6 +739,20 @@
qed
qed
+instantiation rat :: floor_ceiling
+begin
+
+definition [code del]:
+ "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+ fix x :: rat
+ show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+ unfolding floor_rat_def using floor_exists1 by (rule theI')
+qed
+
+end
+
lemma floor_Fract: "floor (Fract a b) = a div b"
using rat_floor_lemma [of a b]
by (simp add: floor_unique)
diff -r 47b0be18ccbe src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy Thu Jul 07 23:33:14 2011 +0200
+++ b/src/HOL/RealDef.thy Thu Jul 07 17:45:45 2011 -0700
@@ -793,6 +793,20 @@
done
qed
+instantiation real :: floor_ceiling
+begin
+
+definition [code del]:
+ "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+ fix x :: real
+ show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+ unfolding floor_real_def using floor_exists1 by (rule theI')
+qed
+
+end
+
subsection {* Completeness *}
lemma not_positive_Real:
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
