src/HOL/Archimedean_Field.thy

   assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
 
 lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
-lemma floor_unique_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
-  for x :: "'a::floor_ceiling"
-  using floor_correct floor_unique by auto
+lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
+using floor_correct floor_unique by auto
 
 lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
   using floor_correct ..
 
 lemma le_floor_iff: "z \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z \<le> x"

   by (simp add: le_minus_iff)
 
 lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z"
   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
 
+lemma ceiling_eq_iff: "\<lceil>x\<rceil> = a \<longleftrightarrow> of_int a - 1 < x \<and> x \<le> of_int a"
+using ceiling_correct ceiling_unique by auto
+
 lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
   using ceiling_correct ..
 
 lemma ceiling_le_iff: "\<lceil>x\<rceil> \<le> z \<longleftrightarrow> x \<le> of_int z"
   unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto

 proof -
   have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
     by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
   moreover
   have "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
-    apply (simp add: floor_unique_iff)
+    apply (simp add: floor_eq_iff)
     apply (auto simp add: algebra_simps)
     apply linarith
     done
   ultimately show ?thesis by (auto simp add: frac_def algebra_simps)
 qed

   with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
     by linarith
 qed
 
 lemma round_of_int [simp]: "round (of_int n) = n"
-  unfolding round_def by (subst floor_unique_iff) force
+  unfolding round_def by (subst floor_eq_iff) force
 
 lemma round_0 [simp]: "round 0 = 0"
   using round_of_int[of 0] by simp
 
 lemma round_1 [simp]: "round 1 = 1"