prefer symbols for "floor", "ceiling";
authorwenzelm
Sun Dec 27 21:46:36 2015 +0100 (2015-12-27)
changeset 61942f02b26f7d39d
parent 61941 31f2105521ee
child 61943 7fba644ed827
prefer symbols for "floor", "ceiling";
src/HOL/Archimedean_Field.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Library/Float.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/TPTP/THF_Arith.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Sun Dec 27 17:16:21 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Sun Dec 27 21:46:36 2015 +0100
     1.3 @@ -138,13 +138,10 @@
     1.4  subsection \<open>Floor function\<close>
     1.5  
     1.6  class floor_ceiling = archimedean_field +
     1.7 -  fixes floor :: "'a \<Rightarrow> int"
     1.8 -  assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
     1.9 +  fixes floor :: "'a \<Rightarrow> int"  ("\<lfloor>_\<rfloor>")
    1.10 +  assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
    1.11  
    1.12 -notation (xsymbols)
    1.13 -  floor  ("\<lfloor>_\<rfloor>")
    1.14 -
    1.15 -lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
    1.16 +lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> \<lfloor>x\<rfloor> = z"
    1.17    using floor_correct [of x] floor_exists1 [of x] by auto
    1.18  
    1.19  lemma floor_unique_iff:
    1.20 @@ -152,156 +149,158 @@
    1.21    shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
    1.22  using floor_correct floor_unique by auto
    1.23  
    1.24 -lemma of_int_floor_le [simp]: "of_int (floor x) \<le> x"
    1.25 +lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
    1.26    using floor_correct ..
    1.27  
    1.28 -lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
    1.29 +lemma le_floor_iff: "z \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z \<le> x"
    1.30  proof
    1.31 -  assume "z \<le> floor x"
    1.32 -  then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp
    1.33 -  also have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
    1.34 +  assume "z \<le> \<lfloor>x\<rfloor>"
    1.35 +  then have "(of_int z :: 'a) \<le> of_int \<lfloor>x\<rfloor>" by simp
    1.36 +  also have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le)
    1.37    finally show "of_int z \<le> x" .
    1.38  next
    1.39    assume "of_int z \<le> x"
    1.40 -  also have "x < of_int (floor x + 1)" using floor_correct ..
    1.41 -  finally show "z \<le> floor x" by (simp del: of_int_add)
    1.42 +  also have "x < of_int (\<lfloor>x\<rfloor> + 1)" using floor_correct ..
    1.43 +  finally show "z \<le> \<lfloor>x\<rfloor>" by (simp del: of_int_add)
    1.44  qed
    1.45  
    1.46 -lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z"
    1.47 +lemma floor_less_iff: "\<lfloor>x\<rfloor> < z \<longleftrightarrow> x < of_int z"
    1.48    by (simp add: not_le [symmetric] le_floor_iff)
    1.49  
    1.50 -lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x"
    1.51 +lemma less_floor_iff: "z < \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z + 1 \<le> x"
    1.52    using le_floor_iff [of "z + 1" x] by auto
    1.53  
    1.54 -lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1"
    1.55 +lemma floor_le_iff: "\<lfloor>x\<rfloor> \<le> z \<longleftrightarrow> x < of_int z + 1"
    1.56    by (simp add: not_less [symmetric] less_floor_iff)
    1.57  
    1.58 -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.59 +lemma floor_split[arith_split]: "P \<lfloor>t\<rfloor> \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
    1.60    by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
    1.61  
    1.62 -lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
    1.63 +lemma floor_mono:
    1.64 +  assumes "x \<le> y"
    1.65 +  shows "\<lfloor>x\<rfloor> \<le> \<lfloor>y\<rfloor>"
    1.66  proof -
    1.67 -  have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
    1.68 +  have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le)
    1.69    also note \<open>x \<le> y\<close>
    1.70    finally show ?thesis by (simp add: le_floor_iff)
    1.71  qed
    1.72  
    1.73 -lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y"
    1.74 +lemma floor_less_cancel: "\<lfloor>x\<rfloor> < \<lfloor>y\<rfloor> \<Longrightarrow> x < y"
    1.75    by (auto simp add: not_le [symmetric] floor_mono)
    1.76  
    1.77 -lemma floor_of_int [simp]: "floor (of_int z) = z"
    1.78 +lemma floor_of_int [simp]: "\<lfloor>of_int z\<rfloor> = z"
    1.79    by (rule floor_unique) simp_all
    1.80  
    1.81 -lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
    1.82 +lemma floor_of_nat [simp]: "\<lfloor>of_nat n\<rfloor> = int n"
    1.83    using floor_of_int [of "of_nat n"] by simp
    1.84  
    1.85 -lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
    1.86 +lemma le_floor_add: "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>"
    1.87    by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
    1.88  
    1.89  text \<open>Floor with numerals\<close>
    1.90  
    1.91 -lemma floor_zero [simp]: "floor 0 = 0"
    1.92 +lemma floor_zero [simp]: "\<lfloor>0\<rfloor> = 0"
    1.93    using floor_of_int [of 0] by simp
    1.94  
    1.95 -lemma floor_one [simp]: "floor 1 = 1"
    1.96 +lemma floor_one [simp]: "\<lfloor>1\<rfloor> = 1"
    1.97    using floor_of_int [of 1] by simp
    1.98  
    1.99 -lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
   1.100 +lemma floor_numeral [simp]: "\<lfloor>numeral v\<rfloor> = numeral v"
   1.101    using floor_of_int [of "numeral v"] by simp
   1.102  
   1.103 -lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
   1.104 +lemma floor_neg_numeral [simp]: "\<lfloor>- numeral v\<rfloor> = - numeral v"
   1.105    using floor_of_int [of "- numeral v"] by simp
   1.106  
   1.107 -lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
   1.108 +lemma zero_le_floor [simp]: "0 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 0 \<le> x"
   1.109    by (simp add: le_floor_iff)
   1.110  
   1.111 -lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x"
   1.112 +lemma one_le_floor [simp]: "1 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
   1.113    by (simp add: le_floor_iff)
   1.114  
   1.115  lemma numeral_le_floor [simp]:
   1.116 -  "numeral v \<le> floor x \<longleftrightarrow> numeral v \<le> x"
   1.117 +  "numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v \<le> x"
   1.118    by (simp add: le_floor_iff)
   1.119  
   1.120  lemma neg_numeral_le_floor [simp]:
   1.121 -  "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
   1.122 +  "- numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v \<le> x"
   1.123    by (simp add: le_floor_iff)
   1.124  
   1.125 -lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
   1.126 +lemma zero_less_floor [simp]: "0 < \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
   1.127    by (simp add: less_floor_iff)
   1.128  
   1.129 -lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x"
   1.130 +lemma one_less_floor [simp]: "1 < \<lfloor>x\<rfloor> \<longleftrightarrow> 2 \<le> x"
   1.131    by (simp add: less_floor_iff)
   1.132  
   1.133  lemma numeral_less_floor [simp]:
   1.134 -  "numeral v < floor x \<longleftrightarrow> numeral v + 1 \<le> x"
   1.135 +  "numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v + 1 \<le> x"
   1.136    by (simp add: less_floor_iff)
   1.137  
   1.138  lemma neg_numeral_less_floor [simp]:
   1.139 -  "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
   1.140 +  "- numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v + 1 \<le> x"
   1.141    by (simp add: less_floor_iff)
   1.142  
   1.143 -lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
   1.144 +lemma floor_le_zero [simp]: "\<lfloor>x\<rfloor> \<le> 0 \<longleftrightarrow> x < 1"
   1.145    by (simp add: floor_le_iff)
   1.146  
   1.147 -lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2"
   1.148 +lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2"
   1.149    by (simp add: floor_le_iff)
   1.150  
   1.151  lemma floor_le_numeral [simp]:
   1.152 -  "floor x \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
   1.153 +  "\<lfloor>x\<rfloor> \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
   1.154    by (simp add: floor_le_iff)
   1.155  
   1.156  lemma floor_le_neg_numeral [simp]:
   1.157 -  "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   1.158 +  "\<lfloor>x\<rfloor> \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   1.159    by (simp add: floor_le_iff)
   1.160  
   1.161 -lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
   1.162 +lemma floor_less_zero [simp]: "\<lfloor>x\<rfloor> < 0 \<longleftrightarrow> x < 0"
   1.163    by (simp add: floor_less_iff)
   1.164  
   1.165 -lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1"
   1.166 +lemma floor_less_one [simp]: "\<lfloor>x\<rfloor> < 1 \<longleftrightarrow> x < 1"
   1.167    by (simp add: floor_less_iff)
   1.168  
   1.169  lemma floor_less_numeral [simp]:
   1.170 -  "floor x < numeral v \<longleftrightarrow> x < numeral v"
   1.171 +  "\<lfloor>x\<rfloor> < numeral v \<longleftrightarrow> x < numeral v"
   1.172    by (simp add: floor_less_iff)
   1.173  
   1.174  lemma floor_less_neg_numeral [simp]:
   1.175 -  "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
   1.176 +  "\<lfloor>x\<rfloor> < - numeral v \<longleftrightarrow> x < - numeral v"
   1.177    by (simp add: floor_less_iff)
   1.178  
   1.179  text \<open>Addition and subtraction of integers\<close>
   1.180  
   1.181 -lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z"
   1.182 +lemma floor_add_of_int [simp]: "\<lfloor>x + of_int z\<rfloor> = \<lfloor>x\<rfloor> + z"
   1.183    using floor_correct [of x] by (simp add: floor_unique)
   1.184  
   1.185  lemma floor_add_numeral [simp]:
   1.186 -    "floor (x + numeral v) = floor x + numeral v"
   1.187 +    "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
   1.188    using floor_add_of_int [of x "numeral v"] by simp
   1.189  
   1.190 -lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   1.191 +lemma floor_add_one [simp]: "\<lfloor>x + 1\<rfloor> = \<lfloor>x\<rfloor> + 1"
   1.192    using floor_add_of_int [of x 1] by simp
   1.193  
   1.194 -lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
   1.195 +lemma floor_diff_of_int [simp]: "\<lfloor>x - of_int z\<rfloor> = \<lfloor>x\<rfloor> - z"
   1.196    using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
   1.197  
   1.198 -lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
   1.199 +lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z"
   1.200    by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
   1.201  
   1.202  lemma floor_diff_numeral [simp]:
   1.203 -  "floor (x - numeral v) = floor x - numeral v"
   1.204 +  "\<lfloor>x - numeral v\<rfloor> = \<lfloor>x\<rfloor> - numeral v"
   1.205    using floor_diff_of_int [of x "numeral v"] by simp
   1.206  
   1.207 -lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
   1.208 +lemma floor_diff_one [simp]: "\<lfloor>x - 1\<rfloor> = \<lfloor>x\<rfloor> - 1"
   1.209    using floor_diff_of_int [of x 1] by simp
   1.210  
   1.211  lemma le_mult_floor:
   1.212    assumes "0 \<le> a" and "0 \<le> b"
   1.213 -  shows "floor a * floor b \<le> floor (a * b)"
   1.214 +  shows "\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor> \<le> \<lfloor>a * b\<rfloor>"
   1.215  proof -
   1.216 -  have "of_int (floor a) \<le> a"
   1.217 -    and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le)
   1.218 -  hence "of_int (floor a * floor b) \<le> a * b"
   1.219 +  have "of_int \<lfloor>a\<rfloor> \<le> a"
   1.220 +    and "of_int \<lfloor>b\<rfloor> \<le> b" by (auto intro: of_int_floor_le)
   1.221 +  hence "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> a * b"
   1.222      using assms by (auto intro!: mult_mono)
   1.223 -  also have "a * b < of_int (floor (a * b) + 1)"  
   1.224 +  also have "a * b < of_int (\<lfloor>a * b\<rfloor> + 1)"
   1.225      using floor_correct[of "a * b"] by auto
   1.226    finally show ?thesis unfolding of_int_less_iff by simp
   1.227  qed
   1.228 @@ -373,150 +372,145 @@
   1.229  
   1.230  subsection \<open>Ceiling function\<close>
   1.231  
   1.232 -definition
   1.233 -  ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
   1.234 -  "ceiling x = - floor (- x)"
   1.235 +definition ceiling :: "'a::floor_ceiling \<Rightarrow> int"  ("\<lceil>_\<rceil>")
   1.236 +  where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
   1.237  
   1.238 -notation (xsymbols)
   1.239 -  ceiling  ("\<lceil>_\<rceil>")
   1.240 -
   1.241 -lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
   1.242 +lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
   1.243    unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) 
   1.244  
   1.245 -lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
   1.246 +lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> \<lceil>x\<rceil> = z"
   1.247    unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
   1.248  
   1.249 -lemma le_of_int_ceiling [simp]: "x \<le> of_int (ceiling x)"
   1.250 +lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
   1.251    using ceiling_correct ..
   1.252  
   1.253 -lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
   1.254 +lemma ceiling_le_iff: "\<lceil>x\<rceil> \<le> z \<longleftrightarrow> x \<le> of_int z"
   1.255    unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto
   1.256  
   1.257 -lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x"
   1.258 +lemma less_ceiling_iff: "z < \<lceil>x\<rceil> \<longleftrightarrow> of_int z < x"
   1.259    by (simp add: not_le [symmetric] ceiling_le_iff)
   1.260  
   1.261 -lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1"
   1.262 +lemma ceiling_less_iff: "\<lceil>x\<rceil> < z \<longleftrightarrow> x \<le> of_int z - 1"
   1.263    using ceiling_le_iff [of x "z - 1"] by simp
   1.264  
   1.265 -lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x"
   1.266 +lemma le_ceiling_iff: "z \<le> \<lceil>x\<rceil> \<longleftrightarrow> of_int z - 1 < x"
   1.267    by (simp add: not_less [symmetric] ceiling_less_iff)
   1.268  
   1.269 -lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y"
   1.270 +lemma ceiling_mono: "x \<ge> y \<Longrightarrow> \<lceil>x\<rceil> \<ge> \<lceil>y\<rceil>"
   1.271    unfolding ceiling_def by (simp add: floor_mono)
   1.272  
   1.273 -lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y"
   1.274 +lemma ceiling_less_cancel: "\<lceil>x\<rceil> < \<lceil>y\<rceil> \<Longrightarrow> x < y"
   1.275    by (auto simp add: not_le [symmetric] ceiling_mono)
   1.276  
   1.277 -lemma ceiling_of_int [simp]: "ceiling (of_int z) = z"
   1.278 +lemma ceiling_of_int [simp]: "\<lceil>of_int z\<rceil> = z"
   1.279    by (rule ceiling_unique) simp_all
   1.280  
   1.281 -lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
   1.282 +lemma ceiling_of_nat [simp]: "\<lceil>of_nat n\<rceil> = int n"
   1.283    using ceiling_of_int [of "of_nat n"] by simp
   1.284  
   1.285 -lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
   1.286 +lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>"
   1.287    by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
   1.288  
   1.289  text \<open>Ceiling with numerals\<close>
   1.290  
   1.291 -lemma ceiling_zero [simp]: "ceiling 0 = 0"
   1.292 +lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
   1.293    using ceiling_of_int [of 0] by simp
   1.294  
   1.295 -lemma ceiling_one [simp]: "ceiling 1 = 1"
   1.296 +lemma ceiling_one [simp]: "\<lceil>1\<rceil> = 1"
   1.297    using ceiling_of_int [of 1] by simp
   1.298  
   1.299 -lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
   1.300 +lemma ceiling_numeral [simp]: "\<lceil>numeral v\<rceil> = numeral v"
   1.301    using ceiling_of_int [of "numeral v"] by simp
   1.302  
   1.303 -lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
   1.304 +lemma ceiling_neg_numeral [simp]: "\<lceil>- numeral v\<rceil> = - numeral v"
   1.305    using ceiling_of_int [of "- numeral v"] by simp
   1.306  
   1.307 -lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
   1.308 +lemma ceiling_le_zero [simp]: "\<lceil>x\<rceil> \<le> 0 \<longleftrightarrow> x \<le> 0"
   1.309    by (simp add: ceiling_le_iff)
   1.310  
   1.311 -lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1"
   1.312 +lemma ceiling_le_one [simp]: "\<lceil>x\<rceil> \<le> 1 \<longleftrightarrow> x \<le> 1"
   1.313    by (simp add: ceiling_le_iff)
   1.314  
   1.315  lemma ceiling_le_numeral [simp]:
   1.316 -  "ceiling x \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   1.317 +  "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   1.318    by (simp add: ceiling_le_iff)
   1.319  
   1.320  lemma ceiling_le_neg_numeral [simp]:
   1.321 -  "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   1.322 +  "\<lceil>x\<rceil> \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   1.323    by (simp add: ceiling_le_iff)
   1.324  
   1.325 -lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
   1.326 +lemma ceiling_less_zero [simp]: "\<lceil>x\<rceil> < 0 \<longleftrightarrow> x \<le> -1"
   1.327    by (simp add: ceiling_less_iff)
   1.328  
   1.329 -lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0"
   1.330 +lemma ceiling_less_one [simp]: "\<lceil>x\<rceil> < 1 \<longleftrightarrow> x \<le> 0"
   1.331    by (simp add: ceiling_less_iff)
   1.332  
   1.333  lemma ceiling_less_numeral [simp]:
   1.334 -  "ceiling x < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   1.335 +  "\<lceil>x\<rceil> < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   1.336    by (simp add: ceiling_less_iff)
   1.337  
   1.338  lemma ceiling_less_neg_numeral [simp]:
   1.339 -  "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   1.340 +  "\<lceil>x\<rceil> < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   1.341    by (simp add: ceiling_less_iff)
   1.342  
   1.343 -lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
   1.344 +lemma zero_le_ceiling [simp]: "0 \<le> \<lceil>x\<rceil> \<longleftrightarrow> -1 < x"
   1.345    by (simp add: le_ceiling_iff)
   1.346  
   1.347 -lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x"
   1.348 +lemma one_le_ceiling [simp]: "1 \<le> \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
   1.349    by (simp add: le_ceiling_iff)
   1.350  
   1.351  lemma numeral_le_ceiling [simp]:
   1.352 -  "numeral v \<le> ceiling x \<longleftrightarrow> numeral v - 1 < x"
   1.353 +  "numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> numeral v - 1 < x"
   1.354    by (simp add: le_ceiling_iff)
   1.355  
   1.356  lemma neg_numeral_le_ceiling [simp]:
   1.357 -  "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
   1.358 +  "- numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> - numeral v - 1 < x"
   1.359    by (simp add: le_ceiling_iff)
   1.360  
   1.361 -lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
   1.362 +lemma zero_less_ceiling [simp]: "0 < \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
   1.363    by (simp add: less_ceiling_iff)
   1.364  
   1.365 -lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x"
   1.366 +lemma one_less_ceiling [simp]: "1 < \<lceil>x\<rceil> \<longleftrightarrow> 1 < x"
   1.367    by (simp add: less_ceiling_iff)
   1.368  
   1.369  lemma numeral_less_ceiling [simp]:
   1.370 -  "numeral v < ceiling x \<longleftrightarrow> numeral v < x"
   1.371 +  "numeral v < \<lceil>x\<rceil> \<longleftrightarrow> numeral v < x"
   1.372    by (simp add: less_ceiling_iff)
   1.373  
   1.374  lemma neg_numeral_less_ceiling [simp]:
   1.375 -  "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   1.376 +  "- numeral v < \<lceil>x\<rceil> \<longleftrightarrow> - numeral v < x"
   1.377    by (simp add: less_ceiling_iff)
   1.378  
   1.379 -lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
   1.380 +lemma ceiling_altdef: "\<lceil>x\<rceil> = (if x = of_int \<lfloor>x\<rfloor> then \<lfloor>x\<rfloor> else \<lfloor>x\<rfloor> + 1)"
   1.381    by (intro ceiling_unique, (simp, linarith?)+)
   1.382  
   1.383 -lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
   1.384 +lemma floor_le_ceiling [simp]: "\<lfloor>x\<rfloor> \<le> \<lceil>x\<rceil>"
   1.385 +  by (simp add: ceiling_altdef)
   1.386  
   1.387  text \<open>Addition and subtraction of integers\<close>
   1.388  
   1.389 -lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
   1.390 +lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
   1.391    using ceiling_correct [of x] by (simp add: ceiling_def)
   1.392  
   1.393 -lemma ceiling_add_numeral [simp]:
   1.394 -    "ceiling (x + numeral v) = ceiling x + numeral v"
   1.395 +lemma ceiling_add_numeral [simp]: "\<lceil>x + numeral v\<rceil> = \<lceil>x\<rceil> + numeral v"
   1.396    using ceiling_add_of_int [of x "numeral v"] by simp
   1.397  
   1.398 -lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   1.399 +lemma ceiling_add_one [simp]: "\<lceil>x + 1\<rceil> = \<lceil>x\<rceil> + 1"
   1.400    using ceiling_add_of_int [of x 1] by simp
   1.401  
   1.402 -lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z"
   1.403 +lemma ceiling_diff_of_int [simp]: "\<lceil>x - of_int z\<rceil> = \<lceil>x\<rceil> - z"
   1.404    using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)
   1.405  
   1.406 -lemma ceiling_diff_numeral [simp]:
   1.407 -  "ceiling (x - numeral v) = ceiling x - numeral v"
   1.408 +lemma ceiling_diff_numeral [simp]: "\<lceil>x - numeral v\<rceil> = \<lceil>x\<rceil> - numeral v"
   1.409    using ceiling_diff_of_int [of x "numeral v"] by simp
   1.410  
   1.411 -lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   1.412 +lemma ceiling_diff_one [simp]: "\<lceil>x - 1\<rceil> = \<lceil>x\<rceil> - 1"
   1.413    using ceiling_diff_of_int [of x 1] by simp
   1.414  
   1.415 -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.416 +lemma ceiling_split[arith_split]: "P \<lceil>t\<rceil> \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
   1.417    by (auto simp add: ceiling_unique ceiling_correct)
   1.418  
   1.419 -lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
   1.420 +lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"
   1.421  proof -
   1.422    have "of_int \<lceil>x\<rceil> - 1 < x" 
   1.423      using ceiling_correct[of x] by simp
   1.424 @@ -530,15 +524,15 @@
   1.425  
   1.426  subsection \<open>Negation\<close>
   1.427  
   1.428 -lemma floor_minus: "floor (- x) = - ceiling x"
   1.429 +lemma floor_minus: "\<lfloor>- x\<rfloor> = - \<lceil>x\<rceil>"
   1.430    unfolding ceiling_def by simp
   1.431  
   1.432 -lemma ceiling_minus: "ceiling (- x) = - floor x"
   1.433 +lemma ceiling_minus: "\<lceil>- x\<rceil> = - \<lfloor>x\<rfloor>"
   1.434    unfolding ceiling_def by simp
   1.435  
   1.436 +
   1.437  subsection \<open>Frac Function\<close>
   1.438  
   1.439 -
   1.440  definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
   1.441    "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
   1.442  
   1.443 @@ -642,7 +636,7 @@
   1.444    from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
   1.445  qed
   1.446  
   1.447 -lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
   1.448 +lemma round_altdef: "round x = (if frac x \<ge> 1/2 then \<lceil>x\<rceil> else \<lfloor>x\<rfloor>)"
   1.449    by (cases "frac x \<ge> 1/2")
   1.450       (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
   1.451  
   1.452 @@ -656,18 +650,18 @@
   1.453    shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
   1.454  proof (cases "of_int m \<ge> z")
   1.455    case True
   1.456 -  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
   1.457 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
   1.458      unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
   1.459    also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
   1.460 -  with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
   1.461 +  with True have "\<bar>of_int \<lceil>z\<rceil> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
   1.462      by (simp add: ceiling_le_iff)
   1.463    finally show ?thesis .
   1.464  next
   1.465    case False
   1.466 -  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
   1.467 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lfloor>z\<rfloor> - z\<bar>"
   1.468      unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
   1.469    also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
   1.470 -  with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
   1.471 +  with False have "\<bar>of_int \<lfloor>z\<rfloor> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
   1.472      by (simp add: le_floor_iff)
   1.473    finally show ?thesis .
   1.474  qed
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Dec 27 17:16:21 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Dec 27 21:46:36 2015 +0100
     2.3 @@ -29,17 +29,17 @@
     2.4    where "x rdvd y \<longleftrightarrow> (\<exists>k::int. y = x * real_of_int k)"
     2.5  
     2.6  lemma int_rdvd_real:
     2.7 -  "real_of_int (i::int) rdvd x = (i dvd (floor x) \<and> real_of_int (floor x) = x)" (is "?l = ?r")
     2.8 +  "real_of_int (i::int) rdvd x = (i dvd \<lfloor>x\<rfloor> \<and> real_of_int \<lfloor>x\<rfloor> = x)" (is "?l = ?r")
     2.9  proof
    2.10    assume "?l"
    2.11    hence th: "\<exists> k. x=real_of_int (i*k)" by (simp add: rdvd_def)
    2.12 -  hence th': "real_of_int (floor x) = x" by (auto simp del: of_int_mult)
    2.13 -  with th have "\<exists> k. real_of_int (floor x) = real_of_int (i*k)" by simp
    2.14 -  hence "\<exists> k. floor x = i*k" by presburger
    2.15 -  thus ?r  using th' by (simp add: dvd_def)
    2.16 +  hence th': "real_of_int \<lfloor>x\<rfloor> = x" by (auto simp del: of_int_mult)
    2.17 +  with th have "\<exists> k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)" by simp
    2.18 +  hence "\<exists>k. \<lfloor>x\<rfloor> = i*k" by presburger
    2.19 +  thus ?r using th' by (simp add: dvd_def)
    2.20  next
    2.21    assume "?r" hence "(i::int) dvd \<lfloor>x::real\<rfloor>" ..
    2.22 -  hence "\<exists> k. real_of_int (floor x) = real_of_int (i*k)"
    2.23 +  hence "\<exists>k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)"
    2.24      by (metis (no_types) dvd_def)
    2.25    thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
    2.26  qed
    2.27 @@ -51,17 +51,18 @@
    2.28  lemma rdvd_abs1: "(abs (real_of_int d) rdvd t) = (real_of_int (d ::int) rdvd t)"
    2.29  proof
    2.30    assume d: "real_of_int d rdvd t"
    2.31 -  from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real_of_int (floor t) = t"
    2.32 +  from d int_rdvd_real have d2: "d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
    2.33      by auto
    2.34  
    2.35 -  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
    2.36 +  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd \<lfloor>t\<rfloor>" by blast
    2.37    with ti int_rdvd_real[symmetric] have "real_of_int (abs d) rdvd t" by blast
    2.38    thus "abs (real_of_int d) rdvd t" by simp
    2.39  next
    2.40    assume "abs (real_of_int d) rdvd t" hence "real_of_int (abs d) rdvd t" by simp
    2.41 -  with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real_of_int (floor t) =t"
    2.42 +  with int_rdvd_real[where i="abs d" and x="t"]
    2.43 +  have d2: "abs d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
    2.44      by auto
    2.45 -  from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
    2.46 +  from iffD1[OF abs_dvd_iff] d2 have "d dvd \<lfloor>t\<rfloor>" by blast
    2.47    with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
    2.48  qed
    2.49  
    2.50 @@ -107,11 +108,11 @@
    2.51  | "Inum bs (Add a b) = Inum bs a + Inum bs b"
    2.52  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    2.53  | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
    2.54 -| "Inum bs (Floor a) = real_of_int (floor (Inum bs a))"
    2.55 -| "Inum bs (CF c a b) = real_of_int c * real_of_int (floor (Inum bs a)) + Inum bs b"
    2.56 -definition "isint t bs \<equiv> real_of_int (floor (Inum bs t)) = Inum bs t"
    2.57 -
    2.58 -lemma isint_iff: "isint n bs = (real_of_int (floor (Inum bs n)) = Inum bs n)"
    2.59 +| "Inum bs (Floor a) = real_of_int \<lfloor>Inum bs a\<rfloor>"
    2.60 +| "Inum bs (CF c a b) = real_of_int c * real_of_int \<lfloor>Inum bs a\<rfloor> + Inum bs b"
    2.61 +definition "isint t bs \<equiv> real_of_int \<lfloor>Inum bs t\<rfloor> = Inum bs t"
    2.62 +
    2.63 +lemma isint_iff: "isint n bs = (real_of_int \<lfloor>Inum bs n\<rfloor> = Inum bs n)"
    2.64    by (simp add: isint_def)
    2.65  
    2.66  lemma isint_Floor: "isint (Floor n) bs"
    2.67 @@ -120,10 +121,10 @@
    2.68  lemma isint_Mul: "isint e bs \<Longrightarrow> isint (Mul c e) bs"
    2.69  proof-
    2.70    let ?e = "Inum bs e"
    2.71 -  let ?fe = "floor ?e"
    2.72 -  assume be: "isint e bs" hence efe:"real_of_int ?fe = ?e" by (simp add: isint_iff)
    2.73 -  have "real_of_int ((floor (Inum bs (Mul c e)))) = real_of_int (floor (real_of_int (c * ?fe)))" using efe by simp
    2.74 -  also have "\<dots> = real_of_int (c* ?fe)"  by (metis floor_of_int)
    2.75 +  assume be: "isint e bs" hence efe:"real_of_int \<lfloor>?e\<rfloor> = ?e" by (simp add: isint_iff)
    2.76 +  have "real_of_int \<lfloor>Inum bs (Mul c e)\<rfloor> = real_of_int \<lfloor>real_of_int (c * \<lfloor>?e\<rfloor>)\<rfloor>"
    2.77 +    using efe by simp
    2.78 +  also have "\<dots> = real_of_int (c* \<lfloor>?e\<rfloor>)" by (metis floor_of_int)
    2.79    also have "\<dots> = real_of_int c * ?e" using efe by simp
    2.80    finally show ?thesis using isint_iff by simp
    2.81  qed
    2.82 @@ -132,9 +133,10 @@
    2.83  proof-
    2.84    let ?I = "\<lambda> t. Inum bs t"
    2.85    assume ie: "isint e bs"
    2.86 -  hence th: "real_of_int (floor (?I e)) = ?I e" by (simp add: isint_def)
    2.87 -  have "real_of_int (floor (?I (Neg e))) = real_of_int (floor (- (real_of_int (floor (?I e)))))" by (simp add: th)
    2.88 -  also have "\<dots> = - real_of_int (floor (?I e))" by simp
    2.89 +  hence th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def)
    2.90 +  have "real_of_int \<lfloor>?I (Neg e)\<rfloor> = real_of_int \<lfloor>- (real_of_int \<lfloor>?I e\<rfloor>)\<rfloor>"
    2.91 +    by (simp add: th)
    2.92 +  also have "\<dots> = - real_of_int \<lfloor>?I e\<rfloor>" by simp
    2.93    finally show "isint (Neg e) bs" by (simp add: isint_def th)
    2.94  qed
    2.95  
    2.96 @@ -142,9 +144,10 @@
    2.97    assumes ie: "isint e bs" shows "isint (Sub (C c) e) bs"
    2.98  proof-
    2.99    let ?I = "\<lambda> t. Inum bs t"
   2.100 -  from ie have th: "real_of_int (floor (?I e)) = ?I e" by (simp add: isint_def)
   2.101 -  have "real_of_int (floor (?I (Sub (C c) e))) = real_of_int (floor ((real_of_int (c -floor (?I e)))))" by (simp add: th)
   2.102 -  also have "\<dots> = real_of_int (c- floor (?I e))" by simp
   2.103 +  from ie have th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def)
   2.104 +  have "real_of_int \<lfloor>?I (Sub (C c) e)\<rfloor> = real_of_int \<lfloor>real_of_int (c - \<lfloor>?I e\<rfloor>)\<rfloor>"
   2.105 +    by (simp add: th)
   2.106 +  also have "\<dots> = real_of_int (c - \<lfloor>?I e\<rfloor>)" by simp
   2.107    finally show "isint (Sub (C c) e) bs" by (simp add: isint_def th)
   2.108  qed
   2.109  
   2.110 @@ -154,9 +157,9 @@
   2.111  proof-
   2.112    let ?a = "Inum bs a"
   2.113    let ?b = "Inum bs b"
   2.114 -  from ai bi isint_iff have "real_of_int (floor (?a + ?b)) = real_of_int (floor (real_of_int (floor ?a) + real_of_int (floor ?b)))"
   2.115 +  from ai bi isint_iff have "real_of_int \<lfloor>?a + ?b\<rfloor> = real_of_int \<lfloor>real_of_int \<lfloor>?a\<rfloor> + real_of_int \<lfloor>?b\<rfloor>\<rfloor>"
   2.116      by simp
   2.117 -  also have "\<dots> = real_of_int (floor ?a) + real_of_int (floor ?b)" by simp
   2.118 +  also have "\<dots> = real_of_int \<lfloor>?a\<rfloor> + real_of_int \<lfloor>?b\<rfloor>" by simp
   2.119    also have "\<dots> = ?a + ?b" using ai bi isint_iff by simp
   2.120    finally show "isint (Add a b) bs" by (simp add: isint_iff)
   2.121  qed
   2.122 @@ -830,15 +833,15 @@
   2.123      hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)"
   2.124        by (cases ?tv) (auto simp add: numfloor_def Let_def split_def)
   2.125      from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+
   2.126 -    hence "?N (Floor t) = real_of_int (floor (?N (Add ?tv ?ti)))" by simp
   2.127 -    also have "\<dots> = real_of_int (floor (?N ?tv) + (floor (?N ?ti)))"
   2.128 +    hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp
   2.129 +    also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)"
   2.130        by (simp,subst tii[simplified isint_iff, symmetric]) simp
   2.131      also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])
   2.132      finally have ?thesis using th1 by simp}
   2.133    moreover {fix v assume H:"?tv = C v"
   2.134      from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+
   2.135 -    hence "?N (Floor t) = real_of_int (floor (?N (Add ?tv ?ti)))" by simp
   2.136 -    also have "\<dots> = real_of_int (floor (?N ?tv) + (floor (?N ?ti)))"
   2.137 +    hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp
   2.138 +    also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)"
   2.139        by (simp,subst tii[simplified isint_iff, symmetric]) simp
   2.140      also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])
   2.141      finally have ?thesis by (simp add: H numfloor_def Let_def split_def) }
   2.142 @@ -1520,11 +1523,11 @@
   2.143    hence na: "?N a" using th by simp
   2.144    have th': "(real_of_int ?nt)*(real_of_int x) = real_of_int (?nt * x)" by simp
   2.145    have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp
   2.146 -  also have "\<dots> = real_of_int (floor ((real_of_int ?nt)* real_of_int(x) + ?I x ?at))" by simp
   2.147 -  also have "\<dots> = real_of_int (floor (?I x ?at + real_of_int (?nt* x)))" by (simp add: ac_simps)
   2.148 -  also have "\<dots> = real_of_int (floor (?I x ?at) + (?nt* x))"
   2.149 -    using floor_add_of_int[of "?I x ?at" "?nt* x"] by simp
   2.150 -  also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int (floor (?I x ?at))" by (simp add: ac_simps)
   2.151 +  also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp
   2.152 +  also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)
   2.153 +  also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"
   2.154 +    using floor_add_of_int[of "?I x ?at" "?nt * x"] by simp
   2.155 +  also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)
   2.156    finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
   2.157    with na show ?case by simp
   2.158  qed
   2.159 @@ -1622,26 +1625,28 @@
   2.160    "zlfm p = p" (hints simp add: fmsize_pos)
   2.161  
   2.162  lemma split_int_less_real:
   2.163 -  "(real_of_int (a::int) < b) = (a < floor b \<or> (a = floor b \<and> real_of_int (floor b) < b))"
   2.164 +  "(real_of_int (a::int) < b) = (a < \<lfloor>b\<rfloor> \<or> (a = \<lfloor>b\<rfloor> \<and> real_of_int \<lfloor>b\<rfloor> < b))"
   2.165  proof( auto)
   2.166 -  assume alb: "real_of_int a < b" and agb: "\<not> a < floor b"
   2.167 -  from agb have "floor b \<le> a" by simp hence th: "b < real_of_int a + 1" by (simp only: floor_le_iff)
   2.168 -  from floor_eq[OF alb th] show "a= floor b" by simp
   2.169 +  assume alb: "real_of_int a < b" and agb: "\<not> a < \<lfloor>b\<rfloor>"
   2.170 +  from agb have "\<lfloor>b\<rfloor> \<le> a" by simp
   2.171 +  hence th: "b < real_of_int a + 1" by (simp only: floor_le_iff)
   2.172 +  from floor_eq[OF alb th] show "a = \<lfloor>b\<rfloor>" by simp
   2.173  next
   2.174 -  assume alb: "a < floor b"
   2.175 -  hence "real_of_int a < real_of_int (floor b)" by simp
   2.176 -  moreover have "real_of_int (floor b) \<le> b" by simp ultimately show  "real_of_int a < b" by arith
   2.177 +  assume alb: "a < \<lfloor>b\<rfloor>"
   2.178 +  hence "real_of_int a < real_of_int \<lfloor>b\<rfloor>" by simp
   2.179 +  moreover have "real_of_int \<lfloor>b\<rfloor> \<le> b" by simp
   2.180 +  ultimately show  "real_of_int a < b" by arith
   2.181  qed
   2.182  
   2.183  lemma split_int_less_real':
   2.184 -  "(real_of_int (a::int) + b < 0) = (real_of_int a - real_of_int (floor(-b)) < 0 \<or> (real_of_int a - real_of_int (floor (-b)) = 0 \<and> real_of_int (floor (-b)) + b < 0))"
   2.185 +  "(real_of_int (a::int) + b < 0) = (real_of_int a - real_of_int \<lfloor>- b\<rfloor> < 0 \<or> (real_of_int a - real_of_int \<lfloor>- b\<rfloor> = 0 \<and> real_of_int \<lfloor>- b\<rfloor> + b < 0))"
   2.186  proof-
   2.187    have "(real_of_int a + b <0) = (real_of_int a < -b)" by arith
   2.188    with split_int_less_real[where a="a" and b="-b"] show ?thesis by arith
   2.189  qed
   2.190  
   2.191  lemma split_int_gt_real':
   2.192 -  "(real_of_int (a::int) + b > 0) = (real_of_int a + real_of_int (floor b) > 0 \<or> (real_of_int a + real_of_int (floor b) = 0 \<and> real_of_int (floor b) - b < 0))"
   2.193 +  "(real_of_int (a::int) + b > 0) = (real_of_int a + real_of_int \<lfloor>b\<rfloor> > 0 \<or> (real_of_int a + real_of_int \<lfloor>b\<rfloor> = 0 \<and> real_of_int \<lfloor>b\<rfloor> - b < 0))"
   2.194  proof-
   2.195    have th: "(real_of_int a + b >0) = (real_of_int (-a) + (-b)< 0)" by arith
   2.196    show ?thesis 
   2.197 @@ -1649,36 +1654,36 @@
   2.198  qed
   2.199  
   2.200  lemma split_int_le_real:
   2.201 -  "(real_of_int (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real_of_int (floor b) < b))"
   2.202 +  "(real_of_int (a::int) \<le> b) = (a \<le> \<lfloor>b\<rfloor> \<or> (a = \<lfloor>b\<rfloor> \<and> real_of_int \<lfloor>b\<rfloor> < b))"
   2.203  proof( auto)
   2.204 -  assume alb: "real_of_int a \<le> b" and agb: "\<not> a \<le> floor b"
   2.205 -  from alb have "floor (real_of_int a) \<le> floor b " by (simp only: floor_mono)
   2.206 -  hence "a \<le> floor b" by simp with agb show "False" by simp
   2.207 +  assume alb: "real_of_int a \<le> b" and agb: "\<not> a \<le> \<lfloor>b\<rfloor>"
   2.208 +  from alb have "\<lfloor>real_of_int a\<rfloor> \<le> \<lfloor>b\<rfloor>" by (simp only: floor_mono)
   2.209 +  hence "a \<le> \<lfloor>b\<rfloor>" by simp with agb show "False" by simp
   2.210  next
   2.211 -  assume alb: "a \<le> floor b"
   2.212 -  hence "real_of_int a \<le> real_of_int (floor b)" by (simp only: floor_mono)
   2.213 +  assume alb: "a \<le> \<lfloor>b\<rfloor>"
   2.214 +  hence "real_of_int a \<le> real_of_int \<lfloor>b\<rfloor>" by (simp only: floor_mono)
   2.215    also have "\<dots>\<le> b" by simp  finally show  "real_of_int a \<le> b" .
   2.216  qed
   2.217  
   2.218  lemma split_int_le_real':
   2.219 -  "(real_of_int (a::int) + b \<le> 0) = (real_of_int a - real_of_int (floor(-b)) \<le> 0 \<or> (real_of_int a - real_of_int (floor (-b)) = 0 \<and> real_of_int (floor (-b)) + b < 0))"
   2.220 +  "(real_of_int (a::int) + b \<le> 0) = (real_of_int a - real_of_int \<lfloor>- b\<rfloor> \<le> 0 \<or> (real_of_int a - real_of_int \<lfloor>- b\<rfloor> = 0 \<and> real_of_int \<lfloor>- b\<rfloor> + b < 0))"
   2.221  proof-
   2.222    have "(real_of_int a + b \<le>0) = (real_of_int a \<le> -b)" by arith
   2.223    with split_int_le_real[where a="a" and b="-b"] show ?thesis by arith
   2.224  qed
   2.225  
   2.226  lemma split_int_ge_real':
   2.227 -  "(real_of_int (a::int) + b \<ge> 0) = (real_of_int a + real_of_int (floor b) \<ge> 0 \<or> (real_of_int a + real_of_int (floor b) = 0 \<and> real_of_int (floor b) - b < 0))"
   2.228 +  "(real_of_int (a::int) + b \<ge> 0) = (real_of_int a + real_of_int \<lfloor>b\<rfloor> \<ge> 0 \<or> (real_of_int a + real_of_int \<lfloor>b\<rfloor> = 0 \<and> real_of_int \<lfloor>b\<rfloor> - b < 0))"
   2.229  proof-
   2.230    have th: "(real_of_int a + b \<ge>0) = (real_of_int (-a) + (-b) \<le> 0)" by arith
   2.231    show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
   2.232      (simp add: algebra_simps ,arith)
   2.233  qed
   2.234  
   2.235 -lemma split_int_eq_real: "(real_of_int (a::int) = b) = ( a = floor b \<and> b = real_of_int (floor b))" (is "?l = ?r")
   2.236 +lemma split_int_eq_real: "(real_of_int (a::int) = b) = ( a = \<lfloor>b\<rfloor> \<and> b = real_of_int \<lfloor>b\<rfloor>)" (is "?l = ?r")
   2.237  by auto
   2.238  
   2.239 -lemma split_int_eq_real': "(real_of_int (a::int) + b = 0) = ( a - floor (-b) = 0 \<and> real_of_int (floor (-b)) + b = 0)" (is "?l = ?r")
   2.240 +lemma split_int_eq_real': "(real_of_int (a::int) + b = 0) = ( a - \<lfloor>- b\<rfloor> = 0 \<and> real_of_int \<lfloor>- b\<rfloor> + b = 0)" (is "?l = ?r")
   2.241  proof-
   2.242    have "?l = (real_of_int a = -b)" by arith
   2.243    with split_int_eq_real[where a="a" and b="-b"] show ?thesis by simp arith
   2.244 @@ -1862,8 +1867,8 @@
   2.245        using Ia by (simp add: Let_def split_def)
   2.246      also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
   2.247        by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
   2.248 -    also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
   2.249 -       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r))))"
   2.250 +    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
   2.251 +       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
   2.252        by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
   2.253      also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz
   2.254        by (simp add: Let_def split_def int_rdvd_iff[symmetric]
   2.255 @@ -1876,11 +1881,11 @@
   2.256        using Ia by (simp add: Let_def split_def)
   2.257      also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
   2.258        by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
   2.259 -    also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
   2.260 -       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r))))"
   2.261 +    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
   2.262 +       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
   2.263        by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
   2.264      also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
   2.265 -      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + floor (?N ?r))", simplified, symmetric]
   2.266 +      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
   2.267        by (simp add: Let_def split_def int_rdvd_iff[symmetric]
   2.268          del: of_int_mult) (auto simp add: ac_simps)
   2.269      finally have ?case using l jnz by blast }
   2.270 @@ -1908,8 +1913,8 @@
   2.271        using Ia by (simp add: Let_def split_def)
   2.272      also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
   2.273        by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
   2.274 -    also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
   2.275 -       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r)))))"
   2.276 +    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
   2.277 +       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
   2.278        by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
   2.279      also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz
   2.280        by (simp add: Let_def split_def int_rdvd_iff[symmetric]
   2.281 @@ -1922,11 +1927,11 @@
   2.282        using Ia by (simp add: Let_def split_def)
   2.283      also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
   2.284        by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
   2.285 -    also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
   2.286 -       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r)))))"
   2.287 +    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
   2.288 +       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
   2.289        by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
   2.290      also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
   2.291 -      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + floor (?N ?r))", simplified, symmetric]
   2.292 +      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
   2.293        by (simp add: Let_def split_def int_rdvd_iff[symmetric]
   2.294          del: of_int_mult) (auto simp add: ac_simps)
   2.295      finally have ?case using l jnz by blast }
   2.296 @@ -2045,7 +2050,7 @@
   2.297    hence rcpos: "real_of_int c > 0" by simp
   2.298    from 3 have nbe: "numbound0 e" by simp
   2.299    fix y
   2.300 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"
   2.301 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"
   2.302    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.303      fix x :: int
   2.304      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.305 @@ -2062,7 +2067,7 @@
   2.306    then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   2.307    from 4 have nbe: "numbound0 e" by simp
   2.308    fix y
   2.309 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"
   2.310 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"
   2.311    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.312      fix x :: int
   2.313      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.314 @@ -2079,7 +2084,7 @@
   2.315    then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   2.316    from 5 have nbe: "numbound0 e" by simp
   2.317    fix y
   2.318 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"
   2.319 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"
   2.320    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.321      fix x :: int
   2.322      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.323 @@ -2095,7 +2100,7 @@
   2.324    then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   2.325    from 6 have nbe: "numbound0 e" by simp
   2.326    fix y
   2.327 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"
   2.328 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"
   2.329    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.330      fix x :: int
   2.331      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.332 @@ -2111,7 +2116,7 @@
   2.333    then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   2.334    from 7 have nbe: "numbound0 e" by simp
   2.335    fix y
   2.336 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"
   2.337 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"
   2.338    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.339      fix x :: int
   2.340      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.341 @@ -2127,7 +2132,7 @@
   2.342    then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   2.343    from 8 have nbe: "numbound0 e" by simp
   2.344    fix y
   2.345 -  have "\<forall> x < (floor (- (Inum (y#bs) e) / (real_of_int c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"
   2.346 +  have "\<forall> x < \<lfloor>- (Inum (y#bs) e) / (real_of_int c)\<rfloor>. ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"
   2.347    proof (simp add: less_floor_iff , rule allI, rule impI)
   2.348      fix x :: int
   2.349      assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
   2.350 @@ -2580,7 +2585,7 @@
   2.351    case (7 c e) hence p: "Ifm (real_of_int x #bs) (Gt (CN 0 c e))" and c1: "c=1"
   2.352      and bn:"numbound0 e" and ie1:"isint e (a#bs)" using dvd1_eq1[where x="c"] by simp_all
   2.353    let ?e = "Inum (real_of_int x # bs) e"
   2.354 -  from ie1 have ie: "real_of_int (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"]
   2.355 +  from ie1 have ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using isint_iff[where n="e" and bs="a#bs"]
   2.356        numbound0_I[OF bn,where b="a" and b'="real_of_int x" and bs="bs"]
   2.357      by (simp add: isint_iff)
   2.358      {assume "real_of_int (x-d) +?e > 0" hence ?case using c1
   2.359 @@ -2593,11 +2598,11 @@
   2.360        from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real_of_int x" and bs="bs"]]
   2.361        have nob: "\<not> (\<exists> j\<in> {1 ..d}. real_of_int x =  - ?e + real_of_int j)" by auto
   2.362        from H p have "real_of_int x + ?e > 0 \<and> real_of_int x + ?e \<le> real_of_int d" by (simp add: c1)
   2.363 -      hence "real_of_int (x + floor ?e) > real_of_int (0::int) \<and> real_of_int (x + floor ?e) \<le> real_of_int d"
   2.364 +      hence "real_of_int (x + \<lfloor>?e\<rfloor>) > real_of_int (0::int) \<and> real_of_int (x + \<lfloor>?e\<rfloor>) \<le> real_of_int d"
   2.365          using ie by simp
   2.366 -      hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
   2.367 -      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e" by simp
   2.368 -      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = real_of_int (- floor ?e + j)" by force
   2.369 +      hence "x + \<lfloor>?e\<rfloor> \<ge> 1 \<and> x + \<lfloor>?e\<rfloor> \<le> d"  by simp
   2.370 +      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + \<lfloor>?e\<rfloor>" by simp
   2.371 +      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = real_of_int (- \<lfloor>?e\<rfloor> + j)" by force
   2.372        hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = - ?e + real_of_int j"
   2.373          by (simp add: ie[simplified isint_iff])
   2.374        with nob have ?case by auto}
   2.375 @@ -2606,7 +2611,7 @@
   2.376    case (8 c e) hence p: "Ifm (real_of_int x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
   2.377      and ie1:"isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
   2.378      let ?e = "Inum (real_of_int x # bs) e"
   2.379 -    from ie1 have ie: "real_of_int (floor ?e) = ?e" using numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real_of_int x)#bs"]
   2.380 +    from ie1 have ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real_of_int x)#bs"]
   2.381        by (simp add: isint_iff)
   2.382      {assume "real_of_int (x-d) +?e \<ge> 0" hence ?case using  c1
   2.383        numbound0_I[OF bn,where b="real_of_int (x-d)" and b'="real_of_int x" and bs="bs"]
   2.384 @@ -2618,12 +2623,12 @@
   2.385        from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real_of_int x" and bs="bs"]]
   2.386        have nob: "\<not> (\<exists> j\<in> {1 ..d}. real_of_int x =  - ?e - 1 + real_of_int j)" by auto
   2.387        from H p have "real_of_int x + ?e \<ge> 0 \<and> real_of_int x + ?e < real_of_int d" by (simp add: c1)
   2.388 -      hence "real_of_int (x + floor ?e) \<ge> real_of_int (0::int) \<and> real_of_int (x + floor ?e) < real_of_int d"
   2.389 +      hence "real_of_int (x + \<lfloor>?e\<rfloor>) \<ge> real_of_int (0::int) \<and> real_of_int (x + \<lfloor>?e\<rfloor>) < real_of_int d"
   2.390          using ie by simp
   2.391 -      hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
   2.392 -      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
   2.393 -      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps)
   2.394 -      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by presburger
   2.395 +      hence "x + \<lfloor>?e\<rfloor> + 1 \<ge> 1 \<and> x + \<lfloor>?e\<rfloor> + 1 \<le> d" by simp
   2.396 +      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + \<lfloor>?e\<rfloor> + 1" by simp
   2.397 +      hence "\<exists> (j::int) \<in> {1 .. d}. x= - \<lfloor>?e\<rfloor> - 1 + j" by (simp add: algebra_simps)
   2.398 +      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- \<lfloor>?e\<rfloor> - 1 + j)" by presburger
   2.399        hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= - ?e - 1 + real_of_int j"
   2.400          by (simp add: ie[simplified isint_iff])
   2.401        with nob have ?case by simp }
   2.402 @@ -2657,16 +2662,16 @@
   2.403      and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   2.404    let ?e = "Inum (real_of_int x # bs) e"
   2.405    from 9 have "isint e (a #bs)"  by simp
   2.406 -  hence ie: "real_of_int (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real_of_int x)#bs"] numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"]
   2.407 +  hence ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using isint_iff[where n="e" and bs="(real_of_int x)#bs"] numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"]
   2.408      by (simp add: isint_iff)
   2.409    from 9 have id: "j dvd d" by simp
   2.410 -  from c1 ie[symmetric] have "?p x = (real_of_int j rdvd real_of_int (x+ floor ?e))" by simp
   2.411 -  also have "\<dots> = (j dvd x + floor ?e)"
   2.412 -    using int_rdvd_real[where i="j" and x="real_of_int (x+ floor ?e)"] by simp
   2.413 -  also have "\<dots> = (j dvd x - d + floor ?e)"
   2.414 -    using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp
   2.415 -  also have "\<dots> = (real_of_int j rdvd real_of_int (x - d + floor ?e))"
   2.416 -    using int_rdvd_real[where i="j" and x="real_of_int (x-d + floor ?e)",symmetric, simplified]
   2.417 +  from c1 ie[symmetric] have "?p x = (real_of_int j rdvd real_of_int (x + \<lfloor>?e\<rfloor>))" by simp
   2.418 +  also have "\<dots> = (j dvd x + \<lfloor>?e\<rfloor>)"
   2.419 +    using int_rdvd_real[where i="j" and x="real_of_int (x + \<lfloor>?e\<rfloor>)"] by simp
   2.420 +  also have "\<dots> = (j dvd x - d + \<lfloor>?e\<rfloor>)"
   2.421 +    using dvd_period[OF id, where x="x" and c="-1" and t="\<lfloor>?e\<rfloor>"] by simp
   2.422 +  also have "\<dots> = (real_of_int j rdvd real_of_int (x - d + \<lfloor>?e\<rfloor>))"
   2.423 +    using int_rdvd_real[where i="j" and x="real_of_int (x - d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
   2.424        ie by simp
   2.425    also have "\<dots> = (real_of_int j rdvd real_of_int x - real_of_int d + ?e)"
   2.426      using ie by simp
   2.427 @@ -2676,16 +2681,16 @@
   2.428    case (10 j c e) hence p: "Ifm (real_of_int x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   2.429    let ?e = "Inum (real_of_int x # bs) e"
   2.430    from 10 have "isint e (a#bs)"  by simp
   2.431 -  hence ie: "real_of_int (floor ?e) = ?e" using numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real_of_int x)#bs"]
   2.432 +  hence ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using numbound0_I[OF bn,where b="real_of_int x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real_of_int x)#bs"]
   2.433      by (simp add: isint_iff)
   2.434    from 10 have id: "j dvd d" by simp
   2.435 -  from c1 ie[symmetric] have "?p x = (\<not> real_of_int j rdvd real_of_int (x+ floor ?e))" by simp
   2.436 -  also have "\<dots> = (\<not> j dvd x + floor ?e)"
   2.437 -    using int_rdvd_real[where i="j" and x="real_of_int (x+ floor ?e)"] by simp
   2.438 -  also have "\<dots> = (\<not> j dvd x - d + floor ?e)"
   2.439 -    using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp
   2.440 -  also have "\<dots> = (\<not> real_of_int j rdvd real_of_int (x - d + floor ?e))"
   2.441 -    using int_rdvd_real[where i="j" and x="real_of_int (x-d + floor ?e)",symmetric, simplified]
   2.442 +  from c1 ie[symmetric] have "?p x = (\<not> real_of_int j rdvd real_of_int (x + \<lfloor>?e\<rfloor>))" by simp
   2.443 +  also have "\<dots> = (\<not> j dvd x + \<lfloor>?e\<rfloor>)"
   2.444 +    using int_rdvd_real[where i="j" and x="real_of_int (x + \<lfloor>?e\<rfloor>)"] by simp
   2.445 +  also have "\<dots> = (\<not> j dvd x - d + \<lfloor>?e\<rfloor>)"
   2.446 +    using dvd_period[OF id, where x="x" and c="-1" and t="\<lfloor>?e\<rfloor>"] by simp
   2.447 +  also have "\<dots> = (\<not> real_of_int j rdvd real_of_int (x - d + \<lfloor>?e\<rfloor>))"
   2.448 +    using int_rdvd_real[where i="j" and x="real_of_int (x - d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
   2.449        ie by simp
   2.450    also have "\<dots> = (\<not> real_of_int j rdvd real_of_int x - real_of_int d + ?e)"
   2.451      using ie by simp
   2.452 @@ -2745,12 +2750,12 @@
   2.453  proof-
   2.454    from minusinf_inf[OF lp]
   2.455    have th: "\<exists>(z::int). \<forall>x<z. ?P (real_of_int x) = ?M x" by blast
   2.456 -  let ?B' = "{floor (?I b) | b. b\<in> ?B}"
   2.457 -  from \<beta>_int[OF lp] isint_iff[where bs="a # bs"] have B: "\<forall> b\<in> ?B. real_of_int (floor (?I b)) = ?I b" by simp
   2.458 +  let ?B' = "{\<lfloor>?I b\<rfloor> | b. b\<in> ?B}"
   2.459 +  from \<beta>_int[OF lp] isint_iff[where bs="a # bs"] have B: "\<forall> b\<in> ?B. real_of_int \<lfloor>?I b\<rfloor> = ?I b" by simp
   2.460    from B[rule_format]
   2.461 -  have "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b + real_of_int j)) = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int (floor (?I b)) + real_of_int j))"
   2.462 +  have "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b + real_of_int j)) = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int \<lfloor>?I b\<rfloor> + real_of_int j))"
   2.463      by simp
   2.464 -  also have "\<dots> = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int (floor (?I b) + j)))" by simp
   2.465 +  also have "\<dots> = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int (\<lfloor>?I b\<rfloor> + j)))" by simp
   2.466    also have"\<dots> = (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P (real_of_int (b + j)))"  by blast
   2.467    finally have BB':
   2.468      "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b + real_of_int j)) = (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P (real_of_int (b + j)))"
   2.469 @@ -2820,23 +2825,22 @@
   2.470    and kpos: "real_of_int k > 0"
   2.471    and tnb: "numbound0 t"
   2.472    and tint: "isint t (real_of_int x#bs)"
   2.473 -  and kdt: "k dvd floor (Inum (b'#bs) t)"
   2.474 -  shows "Ifm (real_of_int x#bs) (\<sigma>_\<rho> p (t,k)) =
   2.475 -  (Ifm ((real_of_int ((floor (Inum (b'#bs) t)) div k))#bs) p)"
   2.476 -  (is "?I (real_of_int x) (?s p) = (?I (real_of_int ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)")
   2.477 +  and kdt: "k dvd \<lfloor>Inum (b'#bs) t\<rfloor>"
   2.478 +  shows "Ifm (real_of_int x#bs) (\<sigma>_\<rho> p (t,k)) = (Ifm ((real_of_int (\<lfloor>Inum (b'#bs) t\<rfloor> div k))#bs) p)"
   2.479 +  (is "?I (real_of_int x) (?s p) = (?I (real_of_int (\<lfloor>?N b' t\<rfloor> div k)) p)" is "_ = (?I ?tk p)")
   2.480  using linp kpos tnb
   2.481  proof(induct p rule: \<sigma>_\<rho>.induct)
   2.482    case (3 c e)
   2.483    from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
   2.484    { assume kdc: "k dvd c"
   2.485 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.486 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.487      from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.488        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.489        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.490    moreover
   2.491    { assume *: "\<not> k dvd c"
   2.492      from kpos have knz': "real_of_int k \<noteq> 0" by simp
   2.493 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t"
   2.494 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t"
   2.495        using isint_def by simp
   2.496      from assms * have "?I (real_of_int x) (?s (Eq (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k = 0)"
   2.497        using real_of_int_div[OF kdt]
   2.498 @@ -2855,14 +2859,14 @@
   2.499    case (4 c e)
   2.500    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.501    { assume kdc: "k dvd c"
   2.502 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.503 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.504      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.505        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.506        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.507    moreover
   2.508    { assume *: "\<not> k dvd c"
   2.509      from kpos have knz': "real_of_int k \<noteq> 0" by simp
   2.510 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.511 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.512      from assms * have "?I (real_of_int x) (?s (NEq (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k \<noteq> 0)"
   2.513        using real_of_int_div[OF kdt]
   2.514          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.515 @@ -2880,13 +2884,13 @@
   2.516    case (5 c e)
   2.517    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.518    { assume kdc: "k dvd c"
   2.519 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.520 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.521      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.522        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.523        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.524    moreover
   2.525    { assume *: "\<not> k dvd c"
   2.526 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.527 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.528      from assms * have "?I (real_of_int x) (?s (Lt (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k < 0)"
   2.529        using real_of_int_div[OF kdt]
   2.530          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.531 @@ -2904,13 +2908,13 @@
   2.532    case (6 c e)
   2.533    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.534    { assume kdc: "k dvd c"
   2.535 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.536 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.537      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.538        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.539        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.540    moreover
   2.541    { assume *: "\<not> k dvd c"
   2.542 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.543 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.544      from assms * have "?I (real_of_int x) (?s (Le (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k \<le> 0)"
   2.545        using real_of_int_div[OF kdt]
   2.546          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.547 @@ -2928,13 +2932,13 @@
   2.548    case (7 c e)
   2.549    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.550    { assume kdc: "k dvd c"
   2.551 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.552 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.553      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.554        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.555        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.556    moreover
   2.557    { assume *: "\<not> k dvd c"
   2.558 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.559 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.560      from assms * have "?I (real_of_int x) (?s (Gt (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k > 0)"
   2.561        using real_of_int_div[OF kdt]
   2.562          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.563 @@ -2952,13 +2956,13 @@
   2.564    case (8 c e)
   2.565    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.566    { assume kdc: "k dvd c"
   2.567 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.568 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.569      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.570        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.571        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.572    moreover
   2.573    { assume *: "\<not> k dvd c"
   2.574 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.575 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.576      from assms * have "?I (real_of_int x) (?s (Ge (CN 0 c e))) = ((real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k \<ge> 0)"
   2.577        using real_of_int_div[OF kdt]
   2.578          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.579 @@ -2976,14 +2980,14 @@
   2.580    case (9 i c e)
   2.581    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.582    { assume kdc: "k dvd c"
   2.583 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.584 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.585      from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.586        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.587        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.588    moreover
   2.589    { assume *: "\<not> k dvd c"
   2.590      from kpos have knz: "k\<noteq>0" by simp hence knz': "real_of_int k \<noteq> 0" by simp
   2.591 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.592 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.593      from assms * have "?I (real_of_int x) (?s (Dvd i (CN 0 c e))) = (real_of_int i * real_of_int k rdvd (real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k)"
   2.594        using real_of_int_div[OF kdt]
   2.595          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.596 @@ -3000,14 +3004,14 @@
   2.597    case (10 i c e)
   2.598    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.599    { assume kdc: "k dvd c"
   2.600 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.601 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.602      from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.603        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.604        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   2.605    moreover
   2.606    { assume *: "\<not> k dvd c"
   2.607      from kpos have knz: "k\<noteq>0" by simp hence knz': "real_of_int k \<noteq> 0" by simp
   2.608 -    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t" using isint_def by simp
   2.609 +    from tint have ti: "real_of_int \<lfloor>?N (real_of_int x) t\<rfloor> = ?N (real_of_int x) t" using isint_def by simp
   2.610      from assms * have "?I (real_of_int x) (?s (NDvd i (CN 0 c e))) = (\<not> (real_of_int i * real_of_int k rdvd (real_of_int c * (?N (real_of_int x) t / real_of_int k) + ?N (real_of_int x) e)* real_of_int k))"
   2.611        using real_of_int_div[OF kdt]
   2.612          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
   2.613 @@ -3020,8 +3024,8 @@
   2.614        by (simp add: ti)
   2.615      finally have ?case . }
   2.616    ultimately show ?case by blast
   2.617 -qed (simp_all add: bound0_I[where bs="bs" and b="real_of_int ((floor (?N b' t)) div k)" and b'="real_of_int x"]
   2.618 -  numbound0_I[where bs="bs" and b="real_of_int ((floor (?N b' t)) div k)" and b'="real_of_int x"])
   2.619 +qed (simp_all add: bound0_I[where bs="bs" and b="real_of_int (\<lfloor>?N b' t\<rfloor> div k)" and b'="real_of_int x"]
   2.620 +  numbound0_I[where bs="bs" and b="real_of_int (\<lfloor>?N b' t\<rfloor> div k)" and b'="real_of_int x"])
   2.621  
   2.622  
   2.623  lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
   2.624 @@ -3088,7 +3092,7 @@
   2.625      and nob: "\<forall> j\<in> {1 .. c*d}. real_of_int (c*i) \<noteq> - ?N i e + real_of_int j"
   2.626      and pi: "real_of_int (c*i) + ?N i e > 0" and cp': "real_of_int c >0"
   2.627      by simp+
   2.628 -  let ?fe = "floor (?N i e)"
   2.629 +  let ?fe = "\<lfloor>?N i e\<rfloor>"
   2.630    from pi cp have th:"(real_of_int i +?N i e / real_of_int c)*real_of_int c > 0" by (simp add: algebra_simps)
   2.631    from pi ei[simplified isint_iff] have "real_of_int (c*i + ?fe) > real_of_int (0::int)" by simp
   2.632    hence pi': "c*i + ?fe > 0" by (simp only: of_int_less_iff[symmetric])
   2.633 @@ -3111,7 +3115,7 @@
   2.634      and nob: "\<forall> j\<in> {1 .. c*d}. real_of_int (c*i) \<noteq> - 1 - ?N i e + real_of_int j"
   2.635      and pi: "real_of_int (c*i) + ?N i e \<ge> 0" and cp': "real_of_int c >0"
   2.636      by simp+
   2.637 -  let ?fe = "floor (?N i e)"
   2.638 +  let ?fe = "\<lfloor>?N i e\<rfloor>"
   2.639    from pi cp have th:"(real_of_int i +?N i e / real_of_int c)*real_of_int c \<ge> 0" by (simp add: algebra_simps)
   2.640    from pi ei[simplified isint_iff] have "real_of_int (c*i + ?fe) \<ge> real_of_int (0::int)" by simp
   2.641    hence pi': "c*i + 1 + ?fe \<ge> 1" by (simp only: of_int_le_iff[symmetric])
   2.642 @@ -3137,16 +3141,16 @@
   2.643    case (9 j c e)  hence p: "real_of_int j rdvd real_of_int (c*i) + ?N i e" (is "?p x") and cp: "c > 0" and bn:"numbound0 e"  by simp+
   2.644    let ?e = "Inum (real_of_int i # bs) e"
   2.645    from 9 have "isint e (real_of_int i #bs)"  by simp
   2.646 -  hence ie: "real_of_int (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real_of_int i)#bs"] numbound0_I[OF bn,where b="real_of_int i" and b'="real_of_int i" and bs="bs"]
   2.647 +  hence ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using isint_iff[where n="e" and bs="(real_of_int i)#bs"] numbound0_I[OF bn,where b="real_of_int i" and b'="real_of_int i" and bs="bs"]
   2.648      by (simp add: isint_iff)
   2.649    from 9 have id: "j dvd d" by simp
   2.650 -  from ie[symmetric] have "?p i = (real_of_int j rdvd real_of_int (c*i+ floor ?e))" by simp
   2.651 -  also have "\<dots> = (j dvd c*i + floor ?e)"
   2.652 -    using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp
   2.653 -  also have "\<dots> = (j dvd c*i - c*d + floor ?e)"
   2.654 -    using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
   2.655 -  also have "\<dots> = (real_of_int j rdvd real_of_int (c*i - c*d + floor ?e))"
   2.656 -    using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
   2.657 +  from ie[symmetric] have "?p i = (real_of_int j rdvd real_of_int (c*i + \<lfloor>?e\<rfloor>))" by simp
   2.658 +  also have "\<dots> = (j dvd c*i + \<lfloor>?e\<rfloor>)"
   2.659 +    using int_rdvd_iff [where i="j" and t="c*i + \<lfloor>?e\<rfloor>"] by simp
   2.660 +  also have "\<dots> = (j dvd c*i - c*d + \<lfloor>?e\<rfloor>)"
   2.661 +    using dvd_period[OF id, where x="c*i" and c="-c" and t="\<lfloor>?e\<rfloor>"] by simp
   2.662 +  also have "\<dots> = (real_of_int j rdvd real_of_int (c*i - c*d + \<lfloor>?e\<rfloor>))"
   2.663 +    using int_rdvd_iff[where i="j" and t="(c*i - c*d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
   2.664        ie by simp
   2.665    also have "\<dots> = (real_of_int j rdvd real_of_int (c*(i - d)) + ?e)"
   2.666      using ie by (simp add:algebra_simps)
   2.667 @@ -3159,17 +3163,17 @@
   2.668      by simp+
   2.669    let ?e = "Inum (real_of_int i # bs) e"
   2.670    from 10 have "isint e (real_of_int i #bs)"  by simp
   2.671 -  hence ie: "real_of_int (floor ?e) = ?e"
   2.672 +  hence ie: "real_of_int \<lfloor>?e\<rfloor> = ?e"
   2.673      using isint_iff[where n="e" and bs="(real_of_int i)#bs"] numbound0_I[OF bn,where b="real_of_int i" and b'="real_of_int i" and bs="bs"]
   2.674      by (simp add: isint_iff)
   2.675    from 10 have id: "j dvd d" by simp
   2.676 -  from ie[symmetric] have "?p i = (\<not> (real_of_int j rdvd real_of_int (c*i+ floor ?e)))" by simp
   2.677 -  also have "\<dots> = Not (j dvd c*i + floor ?e)"
   2.678 -    using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp
   2.679 -  also have "\<dots> = Not (j dvd c*i - c*d + floor ?e)"
   2.680 -    using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
   2.681 -  also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*i - c*d + floor ?e))"
   2.682 -    using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
   2.683 +  from ie[symmetric] have "?p i = (\<not> (real_of_int j rdvd real_of_int (c*i + \<lfloor>?e\<rfloor>)))" by simp
   2.684 +  also have "\<dots> = Not (j dvd c*i + \<lfloor>?e\<rfloor>)"
   2.685 +    using int_rdvd_iff [where i="j" and t="c*i + \<lfloor>?e\<rfloor>"] by simp
   2.686 +  also have "\<dots> = Not (j dvd c*i - c*d + \<lfloor>?e\<rfloor>)"
   2.687 +    using dvd_period[OF id, where x="c*i" and c="-c" and t="\<lfloor>?e\<rfloor>"] by simp
   2.688 +  also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*i - c*d + \<lfloor>?e\<rfloor>))"
   2.689 +    using int_rdvd_iff[where i="j" and t="(c*i - c*d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
   2.690        ie by simp
   2.691    also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*(i - d)) + ?e)"
   2.692      using ie by (simp add:algebra_simps)
   2.693 @@ -3195,20 +3199,19 @@
   2.694      fix e c j assume ecR: "(e,c) \<in> set (\<rho> p)" and jD: "j\<in> {1 .. c*d}"
   2.695        and cx: "real_of_int (c*x) = Inum (real_of_int x#bs) e + real_of_int j"
   2.696      let ?e = "Inum (real_of_int x#bs) e"
   2.697 -    let ?fe = "floor ?e"
   2.698      from \<rho>_l[OF lp'] ecR have ei:"isint e (real_of_int x#bs)" and cp:"c>0" and nb:"numbound0 e"
   2.699        by auto
   2.700      from numbound0_gen [OF nb ei, rule_format,where y="a"] have "isint e (a#bs)" .
   2.701 -    from cx ei[simplified isint_iff] have "real_of_int (c*x) = real_of_int (?fe + j)" by simp
   2.702 -    hence cx: "c*x = ?fe + j" by (simp only: of_int_eq_iff)
   2.703 -    hence cdej:"c dvd ?fe + j" by (simp add: dvd_def) (rule_tac x="x" in exI, simp)
   2.704 -    hence "real_of_int c rdvd real_of_int (?fe + j)" by (simp only: int_rdvd_iff)
   2.705 +    from cx ei[simplified isint_iff] have "real_of_int (c*x) = real_of_int (\<lfloor>?e\<rfloor> + j)" by simp
   2.706 +    hence cx: "c*x = \<lfloor>?e\<rfloor> + j" by (simp only: of_int_eq_iff)
   2.707 +    hence cdej:"c dvd \<lfloor>?e\<rfloor> + j" by (simp add: dvd_def) (rule_tac x="x" in exI, simp)
   2.708 +    hence "real_of_int c rdvd real_of_int (\<lfloor>?e\<rfloor> + j)" by (simp only: int_rdvd_iff)
   2.709      hence rcdej: "real_of_int c rdvd ?e + real_of_int j" by (simp add: ei[simplified isint_iff])
   2.710 -    from cx have "(c*x) div c = (?fe + j) div c" by simp
   2.711 -    with cp have "x = (?fe + j) div c" by simp
   2.712 -    with px have th: "?P ((?fe + j) div c)" by auto
   2.713 +    from cx have "(c*x) div c = (\<lfloor>?e\<rfloor> + j) div c" by simp
   2.714 +    with cp have "x = (\<lfloor>?e\<rfloor> + j) div c" by simp
   2.715 +    with px have th: "?P ((\<lfloor>?e\<rfloor> + j) div c)" by auto
   2.716      from cp have cp': "real_of_int c > 0" by simp
   2.717 -    from cdej have cdej': "c dvd floor (Inum (real_of_int x#bs) (Add e (C j)))" by simp
   2.718 +    from cdej have cdej': "c dvd \<lfloor>Inum (real_of_int x#bs) (Add e (C j))\<rfloor>" by simp
   2.719      from nb have nb': "numbound0 (Add e (C j))" by simp
   2.720      have ji: "isint (C j) (real_of_int x#bs)" by (simp add: isint_def)
   2.721      from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real_of_int x#bs)" .
   2.722 @@ -3246,8 +3249,8 @@
   2.723      from spx' have rcdej:"real_of_int c rdvd (Inum (real_of_int i#bs) (Add e (C j)))"
   2.724        and sr:"Ifm (real_of_int i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
   2.725      from rcdej eji[simplified isint_iff]
   2.726 -    have "real_of_int c rdvd real_of_int (floor (Inum (real_of_int i#bs) (Add e (C j))))" by simp
   2.727 -    hence cdej:"c dvd floor (Inum (real_of_int i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff)
   2.728 +    have "real_of_int c rdvd real_of_int \<lfloor>Inum (real_of_int i#bs) (Add e (C j))\<rfloor>" by simp
   2.729 +    hence cdej:"c dvd \<lfloor>Inum (real_of_int i#bs) (Add e (C j))\<rfloor>" by (simp only: int_rdvd_iff)
   2.730      from cp have cp': "real_of_int c > 0" by simp
   2.731      from \<sigma>_\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real_of_int i # bs) (Add e (C j))\<rfloor> div c)"
   2.732        by (simp add: \<sigma>_def)
   2.733 @@ -3413,12 +3416,12 @@
   2.734        hence nb: "numbound0 s'" by simp
   2.735        from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by simp
   2.736        let ?nxs = "CN 0 n' s'"
   2.737 -      let ?l = "floor (?N s') + j"
   2.738 +      let ?l = "\<lfloor>?N s'\<rfloor> + j"
   2.739        from H
   2.740        have "?I (?p (p',n',s') j) \<longrightarrow>
   2.741            (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
   2.742          by (simp add: fp_def np algebra_simps)
   2.743 -      also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
   2.744 +      also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
   2.745          using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
   2.746        moreover
   2.747        have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
   2.748 @@ -3439,12 +3442,12 @@
   2.749        hence nb: "numbound0 s'" by simp
   2.750        from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by simp
   2.751        let ?nxs = "CN 0 n' s'"
   2.752 -      let ?l = "floor (?N s') + j"
   2.753 +      let ?l = "\<lfloor>?N s'\<rfloor> + j"
   2.754        from H
   2.755        have "?I (?p (p',n',s') j) \<longrightarrow>
   2.756            (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
   2.757          by (simp add: np fp_def algebra_simps)
   2.758 -      also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
   2.759 +      also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
   2.760          using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
   2.761        moreover
   2.762        have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"  by simp
   2.763 @@ -3461,7 +3464,7 @@
   2.764  lemma real_in_int_intervals:
   2.765    assumes xb: "real_of_int m \<le> x \<and> x < real_of_int ((n::int) + 1)"
   2.766    shows "\<exists> j\<in> {m.. n}. real_of_int j \<le> x \<and> x < real_of_int (j+1)" (is "\<exists> j\<in> ?N. ?P j")
   2.767 -by (rule bexI[where P="?P" and x="floor x" and A="?N"])
   2.768 +by (rule bexI[where P="?P" and x="\<lfloor>x\<rfloor>" and A="?N"])
   2.769  (auto simp add: floor_less_iff[where x="x" and z="n+1", simplified]
   2.770    xb[simplified] floor_mono[where x="real_of_int m" and y="x", OF conjunct1[OF xb], simplified floor_of_int[where z="m"]])
   2.771  
   2.772 @@ -3760,9 +3763,9 @@
   2.773  
   2.774  lemma rdvd01_cs:
   2.775    assumes up: "u \<ge> 0" and u1: "u<1" and np: "real_of_int n > 0"
   2.776 -  shows "(real_of_int (i::int) rdvd real_of_int (n::int) * u - s) = (\<exists> j\<in> {0 .. n - 1}. real_of_int n * u = s - real_of_int (floor s) + real_of_int j \<and> real_of_int i rdvd real_of_int (j - floor s))" (is "?lhs = ?rhs")
   2.777 +  shows "(real_of_int (i::int) rdvd real_of_int (n::int) * u - s) = (\<exists> j\<in> {0 .. n - 1}. real_of_int n * u = s - real_of_int \<lfloor>s\<rfloor> + real_of_int j \<and> real_of_int i rdvd real_of_int (j - \<lfloor>s\<rfloor>))" (is "?lhs = ?rhs")
   2.778  proof-
   2.779 -  let ?ss = "s - real_of_int (floor s)"
   2.780 +  let ?ss = "s - real_of_int \<lfloor>s\<rfloor>"
   2.781    from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
   2.782      of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1" by (auto simp: floor_less_cancel)
   2.783    from np have n0: "real_of_int n \<ge> 0" by simp
   2.784 @@ -3770,10 +3773,10 @@
   2.785    have nu0:"real_of_int n * u - s \<ge> -s" and nun:"real_of_int n * u -s < real_of_int n - s" by auto
   2.786    from int_rdvd_real[where i="i" and x="real_of_int (n::int) * u - s"]
   2.787    have "real_of_int i rdvd real_of_int n * u - s =
   2.788 -    (i dvd floor (real_of_int n * u -s) \<and> (real_of_int (floor (real_of_int n * u - s)) = real_of_int n * u - s ))"
   2.789 +    (i dvd \<lfloor>real_of_int n * u - s\<rfloor> \<and> (real_of_int \<lfloor>real_of_int n * u - s\<rfloor> = real_of_int n * u - s ))"
   2.790      (is "_ = (?DE)" is "_ = (?D \<and> ?E)") by simp
   2.791 -  also have "\<dots> = (?DE \<and> real_of_int(floor (real_of_int n * u - s) + floor s)\<ge> -?ss
   2.792 -    \<and> real_of_int(floor (real_of_int n * u - s) + floor s)< real_of_int n - ?ss)" (is "_=(?DE \<and>real_of_int ?a \<ge> _ \<and> real_of_int ?a < _)")
   2.793 +  also have "\<dots> = (?DE \<and> real_of_int (\<lfloor>real_of_int n * u - s\<rfloor> + \<lfloor>s\<rfloor>) \<ge> -?ss
   2.794 +    \<and> real_of_int (\<lfloor>real_of_int n * u - s\<rfloor> + \<lfloor>s\<rfloor>) < real_of_int n - ?ss)" (is "_=(?DE \<and>real_of_int ?a \<ge> _ \<and> real_of_int ?a < _)")
   2.795      using nu0 nun  by auto
   2.796    also have "\<dots> = (?DE \<and> ?a \<ge> 0 \<and> ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1])
   2.797    also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. ?a = j))" by simp
   2.798 @@ -3804,7 +3807,7 @@
   2.799    from foldr_disj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   2.800    have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
   2.801      by (simp add: np DVDJ_def)
   2.802 -  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real_of_int n * x = (- ?s) - real_of_int (floor (- ?s)) + real_of_int j \<and> real_of_int i rdvd real_of_int (j - floor (- ?s)))"
   2.803 +  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real_of_int n * x = (- ?s) - real_of_int \<lfloor>- ?s\<rfloor> + real_of_int j \<and> real_of_int i rdvd real_of_int (j - \<lfloor>- ?s\<rfloor>))"
   2.804      by (simp add: algebra_simps)
   2.805    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
   2.806    have "\<dots> = (real_of_int i rdvd real_of_int n * x - (-?s))" by simp
   2.807 @@ -3820,7 +3823,7 @@
   2.808    from foldr_conj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   2.809    have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
   2.810      by (simp add: np NDVDJ_def)
   2.811 -  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real_of_int n * x = (- ?s) - real_of_int (floor (- ?s)) + real_of_int j \<and> real_of_int i rdvd real_of_int (j - floor (- ?s))))"
   2.812 +  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real_of_int n * x = (- ?s) - real_of_int \<lfloor>- ?s\<rfloor> + real_of_int j \<and> real_of_int i rdvd real_of_int (j - \<lfloor>- ?s\<rfloor>)))"
   2.813      by (simp add: algebra_simps)
   2.814    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
   2.815    have "\<dots> = (\<not> (real_of_int i rdvd real_of_int n * x - (-?s)))" by simp
   2.816 @@ -4752,7 +4755,7 @@
   2.817  proof(auto)
   2.818    fix x
   2.819    assume Px: "P x"
   2.820 -  let ?i = "floor x"
   2.821 +  let ?i = "\<lfloor>x\<rfloor>"
   2.822    let ?u = "x - real_of_int ?i"
   2.823    have "x = real_of_int ?i + ?u" by simp
   2.824    hence "P (real_of_int ?i + ?u)" using Px by simp
     3.1 --- a/src/HOL/Library/Float.thy	Sun Dec 27 17:16:21 2015 +0100
     3.2 +++ b/src/HOL/Library/Float.thy	Sun Dec 27 21:46:36 2015 +0100
     3.3 @@ -619,10 +619,10 @@
     3.4  subsection \<open>Rounding Real Numbers\<close>
     3.5  
     3.6  definition round_down :: "int \<Rightarrow> real \<Rightarrow> real"
     3.7 -  where "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec"
     3.8 +  where "round_down prec x = \<lfloor>x * 2 powr prec\<rfloor> * 2 powr -prec"
     3.9  
    3.10  definition round_up :: "int \<Rightarrow> real \<Rightarrow> real"
    3.11 -  where "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec"
    3.12 +  where "round_up prec x = \<lceil>x * 2 powr prec\<rceil> * 2 powr -prec"
    3.13  
    3.14  lemma round_down_float[simp]: "round_down prec x \<in> float"
    3.15    unfolding round_down_def
    3.16 @@ -648,7 +648,7 @@
    3.17    "round_up prec x - round_down prec x \<le> 2 powr -prec"
    3.18  proof -
    3.19    have "round_up prec x - round_down prec x =
    3.20 -    (ceiling (x * 2 powr prec) - floor (x * 2 powr prec)) * 2 powr -prec"
    3.21 +    (\<lceil>x * 2 powr prec\<rceil> - \<lfloor>x * 2 powr prec\<rfloor>) * 2 powr -prec"
    3.22      by (simp add: round_up_def round_down_def field_simps)
    3.23    also have "\<dots> \<le> 1 * 2 powr -prec"
    3.24      by (rule mult_mono)
    3.25 @@ -889,7 +889,7 @@
    3.26  proof
    3.27    show "2 ^ nat (bitlen x - 1) \<le> x"
    3.28    proof -
    3.29 -    have "(2::real) ^ nat \<lfloor>log 2 (real_of_int x)\<rfloor> = 2 powr real_of_int (floor (log 2 (real_of_int x)))"
    3.30 +    have "(2::real) ^ nat \<lfloor>log 2 (real_of_int x)\<rfloor> = 2 powr real_of_int \<lfloor>log 2 (real_of_int x)\<rfloor>"
    3.31        using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real_of_int x)\<rfloor>"] \<open>x > 0\<close>
    3.32        by simp
    3.33      also have "\<dots> \<le> 2 powr log 2 (real_of_int x)"
    3.34 @@ -2244,15 +2244,18 @@
    3.35    "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
    3.36    apply transfer
    3.37    apply (simp add: powr_int floor_divide_of_int_eq)
    3.38 -  by (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
    3.39 +  apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
    3.40 +  done
    3.41  
    3.42 -lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int (floor x)" by simp
    3.43 +lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int \<lfloor>x\<rfloor>"
    3.44 +  by simp
    3.45  
    3.46  qualified lemma compute_floor_fl[code]:
    3.47    "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
    3.48    apply transfer
    3.49    apply (simp add: powr_int floor_divide_of_int_eq)
    3.50 -  by (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
    3.51 +  apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
    3.52 +  done
    3.53  
    3.54  end
    3.55  
     4.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Dec 27 17:16:21 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Dec 27 21:46:36 2015 +0100
     4.3 @@ -4830,7 +4830,7 @@
     4.4    case False
     4.5    have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \<i>) \<le> b + cmod (Ln w)}"
     4.6      apply (simp add: norm_mult finite_int_iff_bounded_le)
     4.7 -    apply (rule_tac x="floor ((b + cmod (Ln w)) / (2*pi))" in exI)
     4.8 +    apply (rule_tac x="\<lfloor>(b + cmod (Ln w)) / (2*pi)\<rfloor>" in exI)
     4.9      apply (auto simp: divide_simps le_floor_iff)
    4.10      done
    4.11    have [simp]: "\<And>P f. {z. P z \<and> (\<exists>n. z = f n)} = f ` {n. P (f n)}"
     5.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Dec 27 17:16:21 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Dec 27 21:46:36 2015 +0100
     5.3 @@ -1595,7 +1595,7 @@
     5.4      using e   by (auto simp: field_simps)
     5.5    with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
     5.6      apply (auto simp: norm_divide norm_powr_real divide_simps)
     5.7 -    apply (rule_tac x="nat (ceiling (exp xo))" in exI)
     5.8 +    apply (rule_tac x="nat \<lceil>exp xo\<rceil>" in exI)
     5.9      apply clarify
    5.10      apply (drule_tac x="ln n" in spec)
    5.11      apply (auto simp: exp_less_mono nat_ceiling_le_eq not_le)
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 27 17:16:21 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 27 21:46:36 2015 +0100
     6.3 @@ -1259,14 +1259,14 @@
     6.4  
     6.5  lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
     6.6  proof -
     6.7 -  have "\<bar>x \<bullet> b\<bar> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
     6.8 +  have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
     6.9      if [simp]: "b \<in> Basis" for x b :: 'a
    6.10    proof -
    6.11 -    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int (ceiling \<bar>x \<bullet> b\<bar>)"
    6.12 +    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
    6.13        by (rule le_of_int_ceiling)
    6.14 -    also have "\<dots> \<le> real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    6.15 +    also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
    6.16        by (auto intro!: ceiling_mono)
    6.17 -    also have "\<dots> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    6.18 +    also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
    6.19        by simp
    6.20      finally show ?thesis .
    6.21    qed
    6.22 @@ -4612,9 +4612,9 @@
    6.23    assumes "0 < e"
    6.24    obtains n :: nat where "1 / (Suc n) < e"
    6.25  proof atomize_elim
    6.26 -  have "1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
    6.27 +  have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
    6.28      by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
    6.29 -  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
    6.30 +  also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
    6.31      by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
    6.32    also have "\<dots> = e" by simp
    6.33    finally show  "\<exists>n. 1 / real (Suc n) < e" ..
     7.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 27 17:16:21 2015 +0100
     7.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 27 21:46:36 2015 +0100
     7.3 @@ -2494,7 +2494,7 @@
     7.4    from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
     7.5      by (auto split: split_indicator intro!: monoI)
     7.6    { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
     7.7 -      by (rule eventually_sequentiallyI[of "nat(ceiling x)"])
     7.8 +      by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
     7.9           (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
    7.10    from filterlim_cong[OF refl refl this]
    7.11    have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
     8.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Dec 27 17:16:21 2015 +0100
     8.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Dec 27 21:46:36 2015 +0100
     8.3 @@ -220,21 +220,22 @@
     8.4    shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
     8.5               (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
     8.6  proof -
     8.7 -  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else nat(floor (real_of_ereal (u x) * 2 ^ i))"
     8.8 +  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor>"
     8.9    { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
    8.10      proof (split split_if, intro conjI impI)
    8.11        assume "\<not> real j \<le> u x"
    8.12 -      then have "nat(floor (real_of_ereal (u x) * 2 ^ j)) \<le> nat(floor (j * 2 ^ j))"
    8.13 +      then have "nat \<lfloor>real_of_ereal (u x) * 2 ^ j\<rfloor> \<le> nat \<lfloor>j * 2 ^ j\<rfloor>"
    8.14           by (cases "u x") (auto intro!: nat_mono floor_mono)
    8.15 -      moreover have "real (nat(floor (j * 2 ^ j))) \<le> j * 2^j"
    8.16 +      moreover have "real (nat \<lfloor>j * 2 ^ j\<rfloor>) \<le> j * 2^j"
    8.17          by linarith
    8.18 -      ultimately show "nat(floor (real_of_ereal (u x) * 2 ^ j)) \<le> j * 2 ^ j"
    8.19 +      ultimately show "nat \<lfloor>real_of_ereal (u x) * 2 ^ j\<rfloor> \<le> j * 2 ^ j"
    8.20          unfolding of_nat_le_iff by auto
    8.21      qed auto }
    8.22    note f_upper = this
    8.23  
    8.24    have real_f:
    8.25 -    "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (nat(floor (real_of_ereal (u x) * 2 ^ i))))"
    8.26 +    "\<And>i x. real (f x i) =
    8.27 +      (if real i \<le> u x then i * 2 ^ i else real (nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor>))"
    8.28      unfolding f_def by auto
    8.29  
    8.30    let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
    8.31 @@ -259,17 +260,17 @@
    8.32        have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
    8.33        proof ((split split_if)+, intro conjI impI)
    8.34          assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
    8.35 -        then show "i * 2 ^ i * 2 \<le> nat(floor (real_of_ereal (u x) * 2 ^ Suc i))"
    8.36 +        then show "i * 2 ^ i * 2 \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>"
    8.37            by (cases "u x") (auto intro!: le_nat_floor)
    8.38        next
    8.39          assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"
    8.40 -        then show "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 \<le> Suc i * 2 ^ Suc i"
    8.41 +        then show "nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor> * 2 \<le> Suc i * 2 ^ Suc i"
    8.42            by (cases "u x") auto
    8.43        next
    8.44          assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
    8.45 -        have "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 = nat(floor (real_of_ereal (u x) * 2 ^ i)) * nat(floor(2::real))"
    8.46 +        have "nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor> * 2 = nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor> * nat \<lfloor>2::real\<rfloor>"
    8.47            by simp
    8.48 -        also have "\<dots> \<le> nat(floor (real_of_ereal (u x) * 2 ^ i * 2))"
    8.49 +        also have "\<dots> \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ i * 2\<rfloor>"
    8.50          proof cases
    8.51            assume "0 \<le> u x" then show ?thesis
    8.52              by (intro le_mult_nat_floor)
    8.53 @@ -277,9 +278,9 @@
    8.54            assume "\<not> 0 \<le> u x" then show ?thesis
    8.55              by (cases "u x") (auto simp: nat_floor_neg mult_nonpos_nonneg)
    8.56          qed
    8.57 -        also have "\<dots> = nat(floor (real_of_ereal (u x) * 2 ^ Suc i))"
    8.58 +        also have "\<dots> = nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>"
    8.59            by (simp add: ac_simps)
    8.60 -        finally show "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 \<le> nat(floor (real_of_ereal (u x) * 2 ^ Suc i))" .
    8.61 +        finally show "nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor> * 2 \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>" .
    8.62        qed simp
    8.63        then show "?g i x \<le> ?g (Suc i) x"
    8.64          by (auto simp: field_simps)
    8.65 @@ -308,7 +309,7 @@
    8.66            obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
    8.67            then have "r * 2^max N m < p * 2^max N m - 1" by simp
    8.68            moreover
    8.69 -          have "real (nat(floor (p * 2 ^ max N m))) \<le> r * 2 ^ max N m"
    8.70 +          have "real (nat \<lfloor>p * 2 ^ max N m\<rfloor>) \<le> r * 2 ^ max N m"
    8.71              using *[of "max N m"] m unfolding real_f using ux
    8.72              by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
    8.73            then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
     9.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Dec 27 17:16:21 2015 +0100
     9.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Dec 27 21:46:36 2015 +0100
     9.3 @@ -393,23 +393,19 @@
     9.4  
     9.5  subsubsection {* floor and ceiling functions *}
     9.6  
     9.7 -lemma
     9.8 -  "floor x + floor y = floor (x + y :: rat)"
     9.9 +lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>"
    9.10  quickcheck[expect = counterexample]
    9.11  oops
    9.12  
    9.13 -lemma
    9.14 -  "floor x + floor y = floor (x + y :: real)"
    9.15 +lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>"
    9.16  quickcheck[expect = counterexample]
    9.17  oops
    9.18  
    9.19 -lemma
    9.20 -  "ceiling x + ceiling y = ceiling (x + y :: rat)"
    9.21 +lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>"
    9.22  quickcheck[expect = counterexample]
    9.23  oops
    9.24  
    9.25 -lemma
    9.26 -  "ceiling x + ceiling y = ceiling (x + y :: real)"
    9.27 +lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>"
    9.28  quickcheck[expect = counterexample]
    9.29  oops
    9.30  
    10.1 --- a/src/HOL/Rat.thy	Sun Dec 27 17:16:21 2015 +0100
    10.2 +++ b/src/HOL/Rat.thy	Sun Dec 27 21:46:36 2015 +0100
    10.3 @@ -599,17 +599,18 @@
    10.4  begin
    10.5  
    10.6  definition [code del]:
    10.7 -  "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
    10.8 +  "\<lfloor>x::rat\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
    10.9  
   10.10 -instance proof
   10.11 +instance
   10.12 +proof
   10.13    fix x :: rat
   10.14 -  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
   10.15 +  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
   10.16      unfolding floor_rat_def using floor_exists1 by (rule theI')
   10.17  qed
   10.18  
   10.19  end
   10.20  
   10.21 -lemma floor_Fract: "floor (Fract a b) = a div b"
   10.22 +lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b"
   10.23    by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
   10.24  
   10.25  
   10.26 @@ -1017,8 +1018,8 @@
   10.27  qed
   10.28  
   10.29  lemma rat_floor_code [code]:
   10.30 -  "floor p = (let (a, b) = quotient_of p in a div b)"
   10.31 -by (cases p) (simp add: quotient_of_Fract floor_Fract)
   10.32 +  "\<lfloor>p\<rfloor> = (let (a, b) = quotient_of p in a div b)"
   10.33 +  by (cases p) (simp add: quotient_of_Fract floor_Fract)
   10.34  
   10.35  instantiation rat :: equal
   10.36  begin
    11.1 --- a/src/HOL/Real.thy	Sun Dec 27 17:16:21 2015 +0100
    11.2 +++ b/src/HOL/Real.thy	Sun Dec 27 21:46:36 2015 +0100
    11.3 @@ -667,7 +667,7 @@
    11.4    show "\<exists>z. x \<le> of_int z"
    11.5      apply (induct x)
    11.6      apply (frule cauchy_imp_bounded, clarify)
    11.7 -    apply (rule_tac x="ceiling b + 1" in exI)
    11.8 +    apply (rule_tac x="\<lceil>b\<rceil> + 1" in exI)
    11.9      apply (rule less_imp_le)
   11.10      apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
   11.11      apply (rule_tac x=1 in exI, simp add: algebra_simps)
   11.12 @@ -682,11 +682,12 @@
   11.13  begin
   11.14  
   11.15  definition [code del]:
   11.16 -  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   11.17 +  "\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   11.18  
   11.19 -instance proof
   11.20 +instance
   11.21 +proof
   11.22    fix x :: real
   11.23 -  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
   11.24 +  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
   11.25      unfolding floor_real_def using floor_exists1 by (rule theI')
   11.26  qed
   11.27  
   11.28 @@ -777,22 +778,22 @@
   11.29    def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
   11.30    obtain a where a: "\<not> P a"
   11.31    proof
   11.32 -    have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
   11.33 +    have "of_int \<lfloor>x - 1\<rfloor> \<le> x - 1" by (rule of_int_floor_le)
   11.34      also have "x - 1 < x" by simp
   11.35 -    finally have "of_int (floor (x - 1)) < x" .
   11.36 -    hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
   11.37 -    then show "\<not> P (of_int (floor (x - 1)))"
   11.38 +    finally have "of_int \<lfloor>x - 1\<rfloor> < x" .
   11.39 +    hence "\<not> x \<le> of_int \<lfloor>x - 1\<rfloor>" by (simp only: not_le)
   11.40 +    then show "\<not> P (of_int \<lfloor>x - 1\<rfloor>)"
   11.41        unfolding P_def of_rat_of_int_eq using x by blast
   11.42    qed
   11.43    obtain b where b: "P b"
   11.44    proof
   11.45 -    show "P (of_int (ceiling z))"
   11.46 +    show "P (of_int \<lceil>z\<rceil>)"
   11.47      unfolding P_def of_rat_of_int_eq
   11.48      proof
   11.49        fix y assume "y \<in> S"
   11.50        hence "y \<le> z" using z by simp
   11.51 -      also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
   11.52 -      finally show "y \<le> of_int (ceiling z)" .
   11.53 +      also have "z \<le> of_int \<lceil>z\<rceil>" by (rule le_of_int_ceiling)
   11.54 +      finally show "y \<le> of_int \<lceil>z\<rceil>" .
   11.55      qed
   11.56    qed
   11.57  
   11.58 @@ -1245,7 +1246,7 @@
   11.59    from \<open>x<y\<close> have "0 < y-x" by simp
   11.60    with reals_Archimedean obtain q::nat
   11.61      where q: "inverse (real q) < y-x" and "0 < q" by blast
   11.62 -  def p \<equiv> "ceiling (y * real q) - 1"
   11.63 +  def p \<equiv> "\<lceil>y * real q\<rceil> - 1"
   11.64    def r \<equiv> "of_int p / real q"
   11.65    from q have "x < y - inverse (real q)" by simp
   11.66    also have "y - inverse (real q) \<le> r"
   11.67 @@ -1445,40 +1446,40 @@
   11.68  declare of_int_floor_le [simp] (* FIXME*)
   11.69  
   11.70  lemma of_int_floor_cancel [simp]:
   11.71 -    "(of_int (floor x) = x) = (\<exists>n::int. x = of_int n)"
   11.72 +    "(of_int \<lfloor>x\<rfloor> = x) = (\<exists>n::int. x = of_int n)"
   11.73    by (metis floor_of_int)
   11.74  
   11.75 -lemma floor_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> floor x = n"
   11.76 +lemma floor_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
   11.77    by linarith
   11.78  
   11.79 -lemma floor_eq2: "[| real_of_int n \<le> x; x < real_of_int n + 1 |] ==> floor x = n"
   11.80 +lemma floor_eq2: "[| real_of_int n \<le> x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
   11.81    by linarith
   11.82  
   11.83 -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   11.84 +lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
   11.85    by linarith
   11.86  
   11.87 -lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   11.88 +lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
   11.89    by linarith
   11.90  
   11.91 -lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int(floor r)"
   11.92 +lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int \<lfloor>r\<rfloor>"
   11.93    by linarith
   11.94  
   11.95 -lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int(floor r)"
   11.96 +lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \<lfloor>r\<rfloor>"
   11.97    by linarith
   11.98  
   11.99 -lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real_of_int(floor r) + 1"
  11.100 +lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real_of_int \<lfloor>r\<rfloor> + 1"
  11.101    by linarith
  11.102  
  11.103 -lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int(floor r) + 1"
  11.104 +lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \<lfloor>r\<rfloor> + 1"
  11.105    by linarith
  11.106  
  11.107 -lemma floor_eq_iff: "floor x = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
  11.108 -by (simp add: floor_unique_iff)
  11.109 +lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
  11.110 +  by (simp add: floor_unique_iff)
  11.111  
  11.112 -lemma floor_add2[simp]: "floor (of_int a + x) = a + floor x"
  11.113 +lemma floor_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
  11.114    by (simp add: add.commute)
  11.115  
  11.116 -lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> floor (a / real_of_int b) = floor a div b"
  11.117 +lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> \<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
  11.118  proof cases
  11.119    assume "0 < b"
  11.120    { fix i j :: int assume "real_of_int i \<le> a" "a < 1 + real_of_int i"
  11.121 @@ -1509,20 +1510,19 @@
  11.122  lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
  11.123    by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
  11.124  
  11.125 -lemma of_int_ceiling_cancel [simp]:
  11.126 -     "(of_int (ceiling x) = x) = (\<exists>n::int. x = of_int n)"
  11.127 +lemma of_int_ceiling_cancel [simp]: "(of_int \<lceil>x\<rceil> = x) = (\<exists>n::int. x = of_int n)"
  11.128    using ceiling_of_int by metis
  11.129  
  11.130 -lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> ceiling x = n + 1"
  11.131 +lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> \<lceil>x\<rceil> = n + 1"
  11.132    by (simp add: ceiling_unique)
  11.133  
  11.134 -lemma of_int_ceiling_diff_one_le [simp]: "of_int (ceiling r) - 1 \<le> r"
  11.135 +lemma of_int_ceiling_diff_one_le [simp]: "of_int \<lceil>r\<rceil> - 1 \<le> r"
  11.136    by linarith
  11.137  
  11.138 -lemma of_int_ceiling_le_add_one [simp]: "of_int (ceiling r) \<le> r + 1"
  11.139 +lemma of_int_ceiling_le_add_one [simp]: "of_int \<lceil>r\<rceil> \<le> r + 1"
  11.140    by linarith
  11.141  
  11.142 -lemma ceiling_le: "x <= of_int a ==> ceiling x <= a"
  11.143 +lemma ceiling_le: "x <= of_int a ==> \<lceil>x\<rceil> <= a"
  11.144    by (simp add: ceiling_le_iff)
  11.145  
  11.146  lemma ceiling_divide_eq_div: "\<lceil>of_int a / of_int b\<rceil> = - (- a div b)"
  11.147 @@ -1539,28 +1539,27 @@
  11.148  text\<open>The following lemmas are remnants of the erstwhile functions natfloor
  11.149  and natceiling.\<close>
  11.150  
  11.151 -lemma nat_floor_neg: "(x::real) <= 0 ==> nat(floor x) = 0"
  11.152 +lemma nat_floor_neg: "(x::real) <= 0 ==> nat \<lfloor>x\<rfloor> = 0"
  11.153    by linarith
  11.154  
  11.155 -lemma le_nat_floor: "real x <= a ==> x <= nat(floor a)"
  11.156 +lemma le_nat_floor: "real x <= a ==> x <= nat \<lfloor>a\<rfloor>"
  11.157    by linarith
  11.158  
  11.159 -lemma le_mult_nat_floor:
  11.160 -  shows "nat(floor a) * nat(floor b) \<le> nat(floor (a * b))"
  11.161 +lemma le_mult_nat_floor: "nat \<lfloor>a\<rfloor> * nat \<lfloor>b\<rfloor> \<le> nat \<lfloor>a * b\<rfloor>"
  11.162    by (cases "0 <= a & 0 <= b")
  11.163       (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)
  11.164  
  11.165 -lemma nat_ceiling_le_eq [simp]: "(nat(ceiling x) <= a) = (x <= real a)"
  11.166 +lemma nat_ceiling_le_eq [simp]: "(nat \<lceil>x\<rceil> <= a) = (x <= real a)"
  11.167    by linarith
  11.168  
  11.169 -lemma real_nat_ceiling_ge: "x <= real(nat(ceiling x))"
  11.170 +lemma real_nat_ceiling_ge: "x <= real (nat \<lceil>x\<rceil>)"
  11.171    by linarith
  11.172  
  11.173  lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
  11.174 -  by (auto intro!: bexI[of _ "of_nat (nat(ceiling x))"]) linarith
  11.175 +  by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith
  11.176  
  11.177  lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
  11.178 -  apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
  11.179 +  apply (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"])
  11.180    apply (rule less_le_trans[OF _ of_int_floor_le])
  11.181    apply simp
  11.182    done
  11.183 @@ -1568,10 +1567,10 @@
  11.184  subsection \<open>Exponentiation with floor\<close>
  11.185  
  11.186  lemma floor_power:
  11.187 -  assumes "x = of_int (floor x)"
  11.188 -  shows "floor (x ^ n) = floor x ^ n"
  11.189 +  assumes "x = of_int \<lfloor>x\<rfloor>"
  11.190 +  shows "\<lfloor>x ^ n\<rfloor> = \<lfloor>x\<rfloor> ^ n"
  11.191  proof -
  11.192 -  have "x ^ n = of_int (floor x ^ n)"
  11.193 +  have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)"
  11.194      using assms by (induct n arbitrary: x) simp_all
  11.195    then show ?thesis by (metis floor_of_int) 
  11.196  qed
  11.197 @@ -1681,7 +1680,7 @@
  11.198  lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
  11.199    by (simp add: of_rat_divide)
  11.200  
  11.201 -lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
  11.202 +lemma real_floor_code [code]: "\<lfloor>Ratreal x\<rfloor> = \<lfloor>x\<rfloor>"
  11.203    by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)
  11.204  
  11.205  
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 17:16:21 2015 +0100
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 21:46:36 2015 +0100
    12.3 @@ -1701,8 +1701,10 @@
    12.4  lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
    12.5    unfolding filterlim_at_top
    12.6    apply (intro allI)
    12.7 -  apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
    12.8 -  by linarith
    12.9 +  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI)
   12.10 +  apply linarith
   12.11 +  done
   12.12 +
   12.13  
   12.14  subsubsection \<open>Limits of Sequences\<close>
   12.15  
    13.1 --- a/src/HOL/TPTP/THF_Arith.thy	Sun Dec 27 17:16:21 2015 +0100
    13.2 +++ b/src/HOL/TPTP/THF_Arith.thy	Sun Dec 27 21:46:36 2015 +0100
    13.3 @@ -36,12 +36,12 @@
    13.4  
    13.5  overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
    13.6  begin
    13.7 -  definition "rat_to_int (q::rat) = floor q"
    13.8 +  definition "rat_to_int (q::rat) = \<lfloor>q\<rfloor>"
    13.9  end
   13.10  
   13.11  overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
   13.12  begin
   13.13 -  definition "real_to_int (x::real) = floor x"
   13.14 +  definition "real_to_int (x::real) = \<lfloor>x\<rfloor>"
   13.15  end
   13.16  
   13.17  overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"
    14.1 --- a/src/HOL/Transcendental.thy	Sun Dec 27 17:16:21 2015 +0100
    14.2 +++ b/src/HOL/Transcendental.thy	Sun Dec 27 21:46:36 2015 +0100
    14.3 @@ -2378,7 +2378,7 @@
    14.4    fixes i::real
    14.5    shows "b powr i =
    14.6      (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
    14.7 -    else if floor i = i then (if 0 \<le> i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
    14.8 +    else if \<lfloor>i\<rfloor> = i then (if 0 \<le> i then b ^ nat \<lfloor>i\<rfloor> else 1 / b ^ nat \<lfloor>- i\<rfloor>)
    14.9      else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
   14.10    by (auto simp: powr_int)
   14.11  
   14.12 @@ -3568,7 +3568,7 @@
   14.13      using floor_correct [of "x/pi"]
   14.14      by (simp add: add.commute divide_less_eq)
   14.15    obtain n where "real n * pi \<le> x" "x < real (Suc n) * pi"
   14.16 -    apply (rule that [of "nat (floor (x/pi))"] )
   14.17 +    apply (rule that [of "nat \<lfloor>x/pi\<rfloor>"])
   14.18      using assms
   14.19      apply (simp_all add: xle)
   14.20      apply (metis floor_less_iff less_irrefl mult_imp_div_pos_less not_le pi_gt_zero)