src/HOL/Archimedean_Field.thy
changeset 61942 f02b26f7d39d
parent 61738 c4f6031f1310
child 61944 5d06ecfdb472
     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