src/HOL/RComplete.thy
changeset 36979 da7c06ab3169
parent 36826 4d4462d644ae
child 37887 2ae085b07f2f
     1.1 --- a/src/HOL/RComplete.thy	Tue May 18 06:28:42 2010 -0700
     1.2 +++ b/src/HOL/RComplete.thy	Tue May 18 19:00:55 2010 -0700
     1.3 @@ -117,10 +117,12 @@
     1.4  lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
     1.5    by (drule reals_Archimedean6) auto
     1.6  
     1.7 +text {* TODO: delete *}
     1.8  lemma reals_Archimedean_6b_int:
     1.9       "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.10    unfolding real_of_int_def by (rule floor_exists)
    1.11  
    1.12 +text {* TODO: delete *}
    1.13  lemma reals_Archimedean_6c_int:
    1.14       "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.15    unfolding real_of_int_def by (rule floor_exists)
    1.16 @@ -204,9 +206,6 @@
    1.17       "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
    1.18  by (simp add: linorder_not_less [symmetric])
    1.19  
    1.20 -lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
    1.21 -by auto (* delete? *)
    1.22 -
    1.23  lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
    1.24  unfolding real_of_nat_def by simp
    1.25  
    1.26 @@ -259,10 +258,6 @@
    1.27  apply (auto intro: floor_eq3)
    1.28  done
    1.29  
    1.30 -lemma floor_number_of_eq:
    1.31 -     "floor(number_of n :: real) = (number_of n :: int)"
    1.32 -  by (rule floor_number_of) (* already declared [simp] *)
    1.33 -
    1.34  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
    1.35    unfolding real_of_int_def using floor_correct [of r] by simp
    1.36  
    1.37 @@ -284,68 +279,21 @@
    1.38  lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
    1.39    unfolding real_of_int_def by (rule le_floor_iff)
    1.40  
    1.41 -lemma le_floor_eq_number_of:
    1.42 -    "(number_of n <= floor x) = (number_of n <= x)"
    1.43 -  by (rule number_of_le_floor) (* already declared [simp] *)
    1.44 -
    1.45 -lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
    1.46 -  by (rule zero_le_floor) (* already declared [simp] *)
    1.47 -
    1.48 -lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
    1.49 -  by (rule one_le_floor) (* already declared [simp] *)
    1.50 -
    1.51  lemma floor_less_eq: "(floor x < a) = (x < real a)"
    1.52    unfolding real_of_int_def by (rule floor_less_iff)
    1.53  
    1.54 -lemma floor_less_eq_number_of:
    1.55 -    "(floor x < number_of n) = (x < number_of n)"
    1.56 -  by (rule floor_less_number_of) (* already declared [simp] *)
    1.57 -
    1.58 -lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
    1.59 -  by (rule floor_less_zero) (* already declared [simp] *)
    1.60 -
    1.61 -lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
    1.62 -  by (rule floor_less_one) (* already declared [simp] *)
    1.63 -
    1.64  lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
    1.65    unfolding real_of_int_def by (rule less_floor_iff)
    1.66  
    1.67 -lemma less_floor_eq_number_of:
    1.68 -    "(number_of n < floor x) = (number_of n + 1 <= x)"
    1.69 -  by (rule number_of_less_floor) (* already declared [simp] *)
    1.70 -
    1.71 -lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
    1.72 -  by (rule zero_less_floor) (* already declared [simp] *)
    1.73 -
    1.74 -lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
    1.75 -  by (rule one_less_floor) (* already declared [simp] *)
    1.76 -
    1.77  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
    1.78    unfolding real_of_int_def by (rule floor_le_iff)
    1.79  
    1.80 -lemma floor_le_eq_number_of:
    1.81 -    "(floor x <= number_of n) = (x < number_of n + 1)"
    1.82 -  by (rule floor_le_number_of) (* already declared [simp] *)
    1.83 -
    1.84 -lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
    1.85 -  by (rule floor_le_zero) (* already declared [simp] *)
    1.86 -
    1.87 -lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
    1.88 -  by (rule floor_le_one) (* already declared [simp] *)
    1.89 -
    1.90  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
    1.91    unfolding real_of_int_def by (rule floor_add_of_int)
    1.92  
    1.93  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
    1.94    unfolding real_of_int_def by (rule floor_diff_of_int)
    1.95  
    1.96 -lemma floor_subtract_number_of: "floor (x - number_of n) =
    1.97 -    floor x - number_of n"
    1.98 -  by (rule floor_diff_number_of) (* already declared [simp] *)
    1.99 -
   1.100 -lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
   1.101 -  by (rule floor_diff_one) (* already declared [simp] *)
   1.102 -
   1.103  lemma le_mult_floor:
   1.104    assumes "0 \<le> (a :: real)" and "0 \<le> b"
   1.105    shows "floor a * floor b \<le> floor (a * b)"
   1.106 @@ -361,9 +309,6 @@
   1.107  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   1.108    unfolding real_of_nat_def by simp
   1.109  
   1.110 -lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
   1.111 -by auto (* delete? *)
   1.112 -
   1.113  lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
   1.114    unfolding real_of_int_def by simp
   1.115  
   1.116 @@ -389,10 +334,6 @@
   1.117  lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   1.118    unfolding real_of_int_def using ceiling_unique [of n x] by simp
   1.119  
   1.120 -lemma ceiling_number_of_eq:
   1.121 -     "ceiling (number_of n :: real) = (number_of n)"
   1.122 -  by (rule ceiling_number_of) (* already declared [simp] *)
   1.123 -
   1.124  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   1.125    unfolding real_of_int_def using ceiling_correct [of r] by simp
   1.126  
   1.127 @@ -408,68 +349,21 @@
   1.128  lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   1.129    unfolding real_of_int_def by (rule ceiling_le_iff)
   1.130  
   1.131 -lemma ceiling_le_eq_number_of:
   1.132 -    "(ceiling x <= number_of n) = (x <= number_of n)"
   1.133 -  by (rule ceiling_le_number_of) (* already declared [simp] *)
   1.134 -
   1.135 -lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
   1.136 -  by (rule ceiling_le_zero) (* already declared [simp] *)
   1.137 -
   1.138 -lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
   1.139 -  by (rule ceiling_le_one) (* already declared [simp] *)
   1.140 -
   1.141  lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   1.142    unfolding real_of_int_def by (rule less_ceiling_iff)
   1.143  
   1.144 -lemma less_ceiling_eq_number_of:
   1.145 -    "(number_of n < ceiling x) = (number_of n < x)"
   1.146 -  by (rule number_of_less_ceiling) (* already declared [simp] *)
   1.147 -
   1.148 -lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
   1.149 -  by (rule zero_less_ceiling) (* already declared [simp] *)
   1.150 -
   1.151 -lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
   1.152 -  by (rule one_less_ceiling) (* already declared [simp] *)
   1.153 -
   1.154  lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   1.155    unfolding real_of_int_def by (rule ceiling_less_iff)
   1.156  
   1.157 -lemma ceiling_less_eq_number_of:
   1.158 -    "(ceiling x < number_of n) = (x <= number_of n - 1)"
   1.159 -  by (rule ceiling_less_number_of) (* already declared [simp] *)
   1.160 -
   1.161 -lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
   1.162 -  by (rule ceiling_less_zero) (* already declared [simp] *)
   1.163 -
   1.164 -lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
   1.165 -  by (rule ceiling_less_one) (* already declared [simp] *)
   1.166 -
   1.167  lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   1.168    unfolding real_of_int_def by (rule le_ceiling_iff)
   1.169  
   1.170 -lemma le_ceiling_eq_number_of:
   1.171 -    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
   1.172 -  by (rule number_of_le_ceiling) (* already declared [simp] *)
   1.173 -
   1.174 -lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
   1.175 -  by (rule zero_le_ceiling) (* already declared [simp] *)
   1.176 -
   1.177 -lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
   1.178 -  by (rule one_le_ceiling) (* already declared [simp] *)
   1.179 -
   1.180  lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   1.181    unfolding real_of_int_def by (rule ceiling_add_of_int)
   1.182  
   1.183  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   1.184    unfolding real_of_int_def by (rule ceiling_diff_of_int)
   1.185  
   1.186 -lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
   1.187 -    ceiling x - number_of n"
   1.188 -  by (rule ceiling_diff_number_of) (* already declared [simp] *)
   1.189 -
   1.190 -lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
   1.191 -  by (rule ceiling_diff_one) (* already declared [simp] *)
   1.192 -
   1.193  
   1.194  subsection {* Versions for the natural numbers *}
   1.195