src/HOL/Archimedean_Field.thy
 changeset 66515 85c505c98332 parent 66154 bc5e6461f759 child 66793 deabce3ccf1f
```     1.1 --- a/src/HOL/Archimedean_Field.thy	Sat Aug 26 09:10:42 2017 +0200
1.2 +++ b/src/HOL/Archimedean_Field.thy	Sat Aug 26 16:47:25 2017 +0200
1.3 @@ -224,9 +224,8 @@
1.4  lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
1.5    using floor_correct [of x] floor_exists1 [of x] by auto
1.6
1.7 -lemma floor_unique_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
1.8 -  for x :: "'a::floor_ceiling"
1.9 -  using floor_correct floor_unique by auto
1.10 +lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
1.11 +using floor_correct floor_unique by auto
1.12
1.13  lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
1.14    using floor_correct ..
1.15 @@ -467,6 +466,9 @@
1.16  lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z"
1.17    unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
1.18
1.19 +lemma ceiling_eq_iff: "\<lceil>x\<rceil> = a \<longleftrightarrow> of_int a - 1 < x \<and> x \<le> of_int a"
1.20 +using ceiling_correct ceiling_unique by auto
1.21 +
1.22  lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
1.23    using ceiling_correct ..
1.24
1.25 @@ -673,7 +675,7 @@
1.27    moreover
1.28    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>)"
1.29 -    apply (simp add: floor_unique_iff)
1.30 +    apply (simp add: floor_eq_iff)
1.31      apply (auto simp add: algebra_simps)
1.32      apply linarith
1.33      done
1.34 @@ -727,7 +729,7 @@
1.35  qed
1.36
1.37  lemma round_of_int [simp]: "round (of_int n) = n"
1.38 -  unfolding round_def by (subst floor_unique_iff) force
1.39 +  unfolding round_def by (subst floor_eq_iff) force
1.40
1.41  lemma round_0 [simp]: "round 0 = 0"
1.42    using round_of_int[of 0] by simp
```