remove several redundant lemmas about floor and ceiling
authorhuffman
Tue May 18 19:00:55 2010 -0700 (2010-05-18)
changeset 36979da7c06ab3169
parent 36978 4ec5131c6f46
child 36981 684d9dbd3dfc
child 36982 1d4478a797c2
remove several redundant lemmas about floor and ceiling
NEWS
src/HOL/RComplete.thy
     1.1 --- a/NEWS	Tue May 18 06:28:42 2010 -0700
     1.2 +++ b/NEWS	Tue May 18 19:00:55 2010 -0700
     1.3 @@ -159,6 +159,41 @@
     1.4  * Dropped normalizing_semiring etc; use the facts in semiring classes
     1.5  instead.  INCOMPATIBILITY.
     1.6  
     1.7 +* Dropped several real-specific versions of lemmas about floor and
     1.8 +ceiling; use the generic lemmas from Archimedean_Field.thy instead.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11 +  floor_number_of_eq         ~> floor_number_of
    1.12 +  le_floor_eq_number_of      ~> number_of_le_floor
    1.13 +  le_floor_eq_zero           ~> zero_le_floor
    1.14 +  le_floor_eq_one            ~> one_le_floor
    1.15 +  floor_less_eq_number_of    ~> floor_less_number_of
    1.16 +  floor_less_eq_zero         ~> floor_less_zero
    1.17 +  floor_less_eq_one          ~> floor_less_one
    1.18 +  less_floor_eq_number_of    ~> number_of_less_floor
    1.19 +  less_floor_eq_zero         ~> zero_less_floor
    1.20 +  less_floor_eq_one          ~> one_less_floor
    1.21 +  floor_le_eq_number_of      ~> floor_le_number_of
    1.22 +  floor_le_eq_zero           ~> floor_le_zero
    1.23 +  floor_le_eq_one            ~> floor_le_one
    1.24 +  floor_subtract_number_of   ~> floor_diff_number_of
    1.25 +  floor_subtract_one         ~> floor_diff_one
    1.26 +  ceiling_number_of_eq       ~> ceiling_number_of
    1.27 +  ceiling_le_eq_number_of    ~> ceiling_le_number_of
    1.28 +  ceiling_le_zero_eq         ~> ceiling_le_zero
    1.29 +  ceiling_le_eq_one          ~> ceiling_le_one
    1.30 +  less_ceiling_eq_number_of  ~> number_of_less_ceiling
    1.31 +  less_ceiling_eq_zero       ~> zero_less_ceiling
    1.32 +  less_ceiling_eq_one        ~> one_less_ceiling
    1.33 +  ceiling_less_eq_number_of  ~> ceiling_less_number_of
    1.34 +  ceiling_less_eq_zero       ~> ceiling_less_zero
    1.35 +  ceiling_less_eq_one        ~> ceiling_less_one
    1.36 +  le_ceiling_eq_number_of    ~> number_of_le_ceiling
    1.37 +  le_ceiling_eq_zero         ~> zero_le_ceiling
    1.38 +  le_ceiling_eq_one          ~> one_le_ceiling
    1.39 +  ceiling_subtract_number_of ~> ceiling_diff_number_of
    1.40 +  ceiling_subtract_one       ~> ceiling_diff_one
    1.41 +
    1.42  * Theory 'Finite_Set': various folding_XXX locales facilitate the
    1.43  application of the various fold combinators on finite sets.
    1.44  
     2.1 --- a/src/HOL/RComplete.thy	Tue May 18 06:28:42 2010 -0700
     2.2 +++ b/src/HOL/RComplete.thy	Tue May 18 19:00:55 2010 -0700
     2.3 @@ -117,10 +117,12 @@
     2.4  lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
     2.5    by (drule reals_Archimedean6) auto
     2.6  
     2.7 +text {* TODO: delete *}
     2.8  lemma reals_Archimedean_6b_int:
     2.9       "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    2.10    unfolding real_of_int_def by (rule floor_exists)
    2.11  
    2.12 +text {* TODO: delete *}
    2.13  lemma reals_Archimedean_6c_int:
    2.14       "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    2.15    unfolding real_of_int_def by (rule floor_exists)
    2.16 @@ -204,9 +206,6 @@
    2.17       "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
    2.18  by (simp add: linorder_not_less [symmetric])
    2.19  
    2.20 -lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
    2.21 -by auto (* delete? *)
    2.22 -
    2.23  lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
    2.24  unfolding real_of_nat_def by simp
    2.25  
    2.26 @@ -259,10 +258,6 @@
    2.27  apply (auto intro: floor_eq3)
    2.28  done
    2.29  
    2.30 -lemma floor_number_of_eq:
    2.31 -     "floor(number_of n :: real) = (number_of n :: int)"
    2.32 -  by (rule floor_number_of) (* already declared [simp] *)
    2.33 -
    2.34  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
    2.35    unfolding real_of_int_def using floor_correct [of r] by simp
    2.36  
    2.37 @@ -284,68 +279,21 @@
    2.38  lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
    2.39    unfolding real_of_int_def by (rule le_floor_iff)
    2.40  
    2.41 -lemma le_floor_eq_number_of:
    2.42 -    "(number_of n <= floor x) = (number_of n <= x)"
    2.43 -  by (rule number_of_le_floor) (* already declared [simp] *)
    2.44 -
    2.45 -lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
    2.46 -  by (rule zero_le_floor) (* already declared [simp] *)
    2.47 -
    2.48 -lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
    2.49 -  by (rule one_le_floor) (* already declared [simp] *)
    2.50 -
    2.51  lemma floor_less_eq: "(floor x < a) = (x < real a)"
    2.52    unfolding real_of_int_def by (rule floor_less_iff)
    2.53  
    2.54 -lemma floor_less_eq_number_of:
    2.55 -    "(floor x < number_of n) = (x < number_of n)"
    2.56 -  by (rule floor_less_number_of) (* already declared [simp] *)
    2.57 -
    2.58 -lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
    2.59 -  by (rule floor_less_zero) (* already declared [simp] *)
    2.60 -
    2.61 -lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
    2.62 -  by (rule floor_less_one) (* already declared [simp] *)
    2.63 -
    2.64  lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
    2.65    unfolding real_of_int_def by (rule less_floor_iff)
    2.66  
    2.67 -lemma less_floor_eq_number_of:
    2.68 -    "(number_of n < floor x) = (number_of n + 1 <= x)"
    2.69 -  by (rule number_of_less_floor) (* already declared [simp] *)
    2.70 -
    2.71 -lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
    2.72 -  by (rule zero_less_floor) (* already declared [simp] *)
    2.73 -
    2.74 -lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
    2.75 -  by (rule one_less_floor) (* already declared [simp] *)
    2.76 -
    2.77  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
    2.78    unfolding real_of_int_def by (rule floor_le_iff)
    2.79  
    2.80 -lemma floor_le_eq_number_of:
    2.81 -    "(floor x <= number_of n) = (x < number_of n + 1)"
    2.82 -  by (rule floor_le_number_of) (* already declared [simp] *)
    2.83 -
    2.84 -lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
    2.85 -  by (rule floor_le_zero) (* already declared [simp] *)
    2.86 -
    2.87 -lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
    2.88 -  by (rule floor_le_one) (* already declared [simp] *)
    2.89 -
    2.90  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
    2.91    unfolding real_of_int_def by (rule floor_add_of_int)
    2.92  
    2.93  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
    2.94    unfolding real_of_int_def by (rule floor_diff_of_int)
    2.95  
    2.96 -lemma floor_subtract_number_of: "floor (x - number_of n) =
    2.97 -    floor x - number_of n"
    2.98 -  by (rule floor_diff_number_of) (* already declared [simp] *)
    2.99 -
   2.100 -lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
   2.101 -  by (rule floor_diff_one) (* already declared [simp] *)
   2.102 -
   2.103  lemma le_mult_floor:
   2.104    assumes "0 \<le> (a :: real)" and "0 \<le> b"
   2.105    shows "floor a * floor b \<le> floor (a * b)"
   2.106 @@ -361,9 +309,6 @@
   2.107  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   2.108    unfolding real_of_nat_def by simp
   2.109  
   2.110 -lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
   2.111 -by auto (* delete? *)
   2.112 -
   2.113  lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
   2.114    unfolding real_of_int_def by simp
   2.115  
   2.116 @@ -389,10 +334,6 @@
   2.117  lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   2.118    unfolding real_of_int_def using ceiling_unique [of n x] by simp
   2.119  
   2.120 -lemma ceiling_number_of_eq:
   2.121 -     "ceiling (number_of n :: real) = (number_of n)"
   2.122 -  by (rule ceiling_number_of) (* already declared [simp] *)
   2.123 -
   2.124  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   2.125    unfolding real_of_int_def using ceiling_correct [of r] by simp
   2.126  
   2.127 @@ -408,68 +349,21 @@
   2.128  lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   2.129    unfolding real_of_int_def by (rule ceiling_le_iff)
   2.130  
   2.131 -lemma ceiling_le_eq_number_of:
   2.132 -    "(ceiling x <= number_of n) = (x <= number_of n)"
   2.133 -  by (rule ceiling_le_number_of) (* already declared [simp] *)
   2.134 -
   2.135 -lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
   2.136 -  by (rule ceiling_le_zero) (* already declared [simp] *)
   2.137 -
   2.138 -lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
   2.139 -  by (rule ceiling_le_one) (* already declared [simp] *)
   2.140 -
   2.141  lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   2.142    unfolding real_of_int_def by (rule less_ceiling_iff)
   2.143  
   2.144 -lemma less_ceiling_eq_number_of:
   2.145 -    "(number_of n < ceiling x) = (number_of n < x)"
   2.146 -  by (rule number_of_less_ceiling) (* already declared [simp] *)
   2.147 -
   2.148 -lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
   2.149 -  by (rule zero_less_ceiling) (* already declared [simp] *)
   2.150 -
   2.151 -lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
   2.152 -  by (rule one_less_ceiling) (* already declared [simp] *)
   2.153 -
   2.154  lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   2.155    unfolding real_of_int_def by (rule ceiling_less_iff)
   2.156  
   2.157 -lemma ceiling_less_eq_number_of:
   2.158 -    "(ceiling x < number_of n) = (x <= number_of n - 1)"
   2.159 -  by (rule ceiling_less_number_of) (* already declared [simp] *)
   2.160 -
   2.161 -lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
   2.162 -  by (rule ceiling_less_zero) (* already declared [simp] *)
   2.163 -
   2.164 -lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
   2.165 -  by (rule ceiling_less_one) (* already declared [simp] *)
   2.166 -
   2.167  lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   2.168    unfolding real_of_int_def by (rule le_ceiling_iff)
   2.169  
   2.170 -lemma le_ceiling_eq_number_of:
   2.171 -    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
   2.172 -  by (rule number_of_le_ceiling) (* already declared [simp] *)
   2.173 -
   2.174 -lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
   2.175 -  by (rule zero_le_ceiling) (* already declared [simp] *)
   2.176 -
   2.177 -lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
   2.178 -  by (rule one_le_ceiling) (* already declared [simp] *)
   2.179 -
   2.180  lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   2.181    unfolding real_of_int_def by (rule ceiling_add_of_int)
   2.182  
   2.183  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   2.184    unfolding real_of_int_def by (rule ceiling_diff_of_int)
   2.185  
   2.186 -lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
   2.187 -    ceiling x - number_of n"
   2.188 -  by (rule ceiling_diff_number_of) (* already declared [simp] *)
   2.189 -
   2.190 -lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
   2.191 -  by (rule ceiling_diff_one) (* already declared [simp] *)
   2.192 -
   2.193  
   2.194  subsection {* Versions for the natural numbers *}
   2.195