src/HOL/Archimedean_Field.thy
changeset 58040 9a867afaab5a
parent 54489 03ff4d1e6784
child 58097 cfd3cff9387b
     1.1 --- a/src/HOL/Archimedean_Field.thy	Mon Aug 25 09:40:50 2014 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Aug 19 18:37:32 2014 +0200
     1.3 @@ -174,6 +174,9 @@
     1.4  lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1"
     1.5    by (simp add: not_less [symmetric] less_floor_iff)
     1.6  
     1.7 +lemma floor_split[arith_split]: "P (floor t) \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
     1.8 +  by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
     1.9 +
    1.10  lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
    1.11  proof -
    1.12    have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
    1.13 @@ -285,7 +288,6 @@
    1.14  lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
    1.15    using floor_diff_of_int [of x 1] by simp
    1.16  
    1.17 -
    1.18  subsection {* Ceiling function *}
    1.19  
    1.20  definition
    1.21 @@ -426,6 +428,9 @@
    1.22  lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
    1.23    using ceiling_diff_of_int [of x 1] by simp
    1.24  
    1.25 +lemma ceiling_split[arith_split]: "P (ceiling t) \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
    1.26 +  by (auto simp add: ceiling_unique ceiling_correct)
    1.27 +
    1.28  lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
    1.29  proof -
    1.30    have "of_int \<lceil>x\<rceil> - 1 < x"