adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
authorbulwahn
Sat Jul 09 13:41:58 2011 +0200 (2011-07-09)
changeset 437326b2bdc57155b
parent 43713 1ba5331b4623
child 43733 a6ca7b83612f
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
src/HOL/Archimedean_Field.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Fri Jul 08 22:00:53 2011 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Sat Jul 09 13:41:58 2011 +0200
     1.3 @@ -141,9 +141,9 @@
     1.4  
     1.5  subsection {* Floor function *}
     1.6  
     1.7 -definition
     1.8 -  floor :: "'a::archimedean_field \<Rightarrow> int" where
     1.9 -  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
    1.10 +class floor_ceiling = archimedean_field +
    1.11 +  fixes floor :: "'a \<Rightarrow> int"
    1.12 +  assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
    1.13  
    1.14  notation (xsymbols)
    1.15    floor  ("\<lfloor>_\<rfloor>")
    1.16 @@ -151,9 +151,6 @@
    1.17  notation (HTML output)
    1.18    floor  ("\<lfloor>_\<rfloor>")
    1.19  
    1.20 -lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
    1.21 -  unfolding floor_def using floor_exists1 by (rule theI')
    1.22 -
    1.23  lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
    1.24    using floor_correct [of x] floor_exists1 [of x] by auto
    1.25  
    1.26 @@ -273,7 +270,7 @@
    1.27  subsection {* Ceiling function *}
    1.28  
    1.29  definition
    1.30 -  ceiling :: "'a::archimedean_field \<Rightarrow> int" where
    1.31 +  ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
    1.32    [code del]: "ceiling x = - floor (- x)"
    1.33  
    1.34  notation (xsymbols)
     2.1 --- a/src/HOL/Rat.thy	Fri Jul 08 22:00:53 2011 +0200
     2.2 +++ b/src/HOL/Rat.thy	Sat Jul 09 13:41:58 2011 +0200
     2.3 @@ -739,6 +739,20 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +instantiation rat :: floor_ceiling
     2.8 +begin
     2.9 +
    2.10 +definition [code del]:
    2.11 +  "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
    2.12 +
    2.13 +instance proof
    2.14 +  fix x :: rat
    2.15 +  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
    2.16 +    unfolding floor_rat_def using floor_exists1 by (rule theI')
    2.17 +qed
    2.18 +
    2.19 +end
    2.20 +
    2.21  lemma floor_Fract: "floor (Fract a b) = a div b"
    2.22    using rat_floor_lemma [of a b]
    2.23    by (simp add: floor_unique)
     3.1 --- a/src/HOL/RealDef.thy	Fri Jul 08 22:00:53 2011 +0200
     3.2 +++ b/src/HOL/RealDef.thy	Sat Jul 09 13:41:58 2011 +0200
     3.3 @@ -793,6 +793,20 @@
     3.4      done
     3.5  qed
     3.6  
     3.7 +instantiation real :: floor_ceiling
     3.8 +begin
     3.9 +
    3.10 +definition [code del]:
    3.11 +  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
    3.12 +
    3.13 +instance proof
    3.14 +  fix x :: real
    3.15 +  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
    3.16 +    unfolding floor_real_def using floor_exists1 by (rule theI')
    3.17 +qed
    3.18 +
    3.19 +end
    3.20 +
    3.21  subsection {* Completeness *}
    3.22  
    3.23  lemma not_positive_Real: