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.26      by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
    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