prefer symbols for "floor", "ceiling";

--- a/src/HOL/Archimedean_Field.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -138,13 +138,10 @@
 subsection \<open>Floor function\<close>
 
 class floor_ceiling = archimedean_field +
-  fixes floor :: "'a \<Rightarrow> int"
-  assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+  fixes floor :: "'a \<Rightarrow> int"  ("\<lfloor>_\<rfloor>")
+  assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
 
-notation (xsymbols)
-  floor  ("\<lfloor>_\<rfloor>")
-
-lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
+lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> \<lfloor>x\<rfloor> = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
 lemma floor_unique_iff:
@@ -152,156 +149,158 @@
   shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
 using floor_correct floor_unique by auto
 
-lemma of_int_floor_le [simp]: "of_int (floor x) \<le> x"
+lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
   using floor_correct ..
 
-lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
+lemma le_floor_iff: "z \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z \<le> x"
 proof
-  assume "z \<le> floor x"
-  then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp
-  also have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
+  assume "z \<le> \<lfloor>x\<rfloor>"
+  then have "(of_int z :: 'a) \<le> of_int \<lfloor>x\<rfloor>" by simp
+  also have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le)
   finally show "of_int z \<le> x" .
 next
   assume "of_int z \<le> x"
-  also have "x < of_int (floor x + 1)" using floor_correct ..
-  finally show "z \<le> floor x" by (simp del: of_int_add)
+  also have "x < of_int (\<lfloor>x\<rfloor> + 1)" using floor_correct ..
+  finally show "z \<le> \<lfloor>x\<rfloor>" by (simp del: of_int_add)
 qed
 
-lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z"
+lemma floor_less_iff: "\<lfloor>x\<rfloor> < z \<longleftrightarrow> x < of_int z"
   by (simp add: not_le [symmetric] le_floor_iff)
 
-lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x"
+lemma less_floor_iff: "z < \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z + 1 \<le> x"
   using le_floor_iff [of "z + 1" x] by auto
 
-lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1"
+lemma floor_le_iff: "\<lfloor>x\<rfloor> \<le> z \<longleftrightarrow> x < of_int z + 1"
   by (simp add: not_less [symmetric] less_floor_iff)
 
-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)"
+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)"
   by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
 
-lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
+lemma floor_mono:
+  assumes "x \<le> y"
+  shows "\<lfloor>x\<rfloor> \<le> \<lfloor>y\<rfloor>"
 proof -
-  have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
+  have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le)
   also note \<open>x \<le> y\<close>
   finally show ?thesis by (simp add: le_floor_iff)
 qed
 
-lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y"
+lemma floor_less_cancel: "\<lfloor>x\<rfloor> < \<lfloor>y\<rfloor> \<Longrightarrow> x < y"
   by (auto simp add: not_le [symmetric] floor_mono)
 
-lemma floor_of_int [simp]: "floor (of_int z) = z"
+lemma floor_of_int [simp]: "\<lfloor>of_int z\<rfloor> = z"
   by (rule floor_unique) simp_all
 
-lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
+lemma floor_of_nat [simp]: "\<lfloor>of_nat n\<rfloor> = int n"
   using floor_of_int [of "of_nat n"] by simp
 
-lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
+lemma le_floor_add: "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>"
   by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
 
 text \<open>Floor with numerals\<close>
 
-lemma floor_zero [simp]: "floor 0 = 0"
+lemma floor_zero [simp]: "\<lfloor>0\<rfloor> = 0"
   using floor_of_int [of 0] by simp
 
-lemma floor_one [simp]: "floor 1 = 1"
+lemma floor_one [simp]: "\<lfloor>1\<rfloor> = 1"
   using floor_of_int [of 1] by simp
 
-lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
+lemma floor_numeral [simp]: "\<lfloor>numeral v\<rfloor> = numeral v"
   using floor_of_int [of "numeral v"] by simp
 
-lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
+lemma floor_neg_numeral [simp]: "\<lfloor>- numeral v\<rfloor> = - numeral v"
   using floor_of_int [of "- numeral v"] by simp
 
-lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
+lemma zero_le_floor [simp]: "0 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 0 \<le> x"
   by (simp add: le_floor_iff)
 
-lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x"
+lemma one_le_floor [simp]: "1 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
   by (simp add: le_floor_iff)
 
 lemma numeral_le_floor [simp]:
-  "numeral v \<le> floor x \<longleftrightarrow> numeral v \<le> x"
+  "numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v \<le> x"
   by (simp add: le_floor_iff)
 
 lemma neg_numeral_le_floor [simp]:
-  "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
+  "- numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v \<le> x"
   by (simp add: le_floor_iff)
 
-lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
+lemma zero_less_floor [simp]: "0 < \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
   by (simp add: less_floor_iff)
 
-lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x"
+lemma one_less_floor [simp]: "1 < \<lfloor>x\<rfloor> \<longleftrightarrow> 2 \<le> x"
   by (simp add: less_floor_iff)
 
 lemma numeral_less_floor [simp]:
-  "numeral v < floor x \<longleftrightarrow> numeral v + 1 \<le> x"
+  "numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v + 1 \<le> x"
   by (simp add: less_floor_iff)
 
 lemma neg_numeral_less_floor [simp]:
-  "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
+  "- numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v + 1 \<le> x"
   by (simp add: less_floor_iff)
 
-lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
+lemma floor_le_zero [simp]: "\<lfloor>x\<rfloor> \<le> 0 \<longleftrightarrow> x < 1"
   by (simp add: floor_le_iff)
 
-lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2"
+lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2"
   by (simp add: floor_le_iff)
 
 lemma floor_le_numeral [simp]:
-  "floor x \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
+  "\<lfloor>x\<rfloor> \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
   by (simp add: floor_le_iff)
 
 lemma floor_le_neg_numeral [simp]:
-  "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
+  "\<lfloor>x\<rfloor> \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   by (simp add: floor_le_iff)
 
-lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
+lemma floor_less_zero [simp]: "\<lfloor>x\<rfloor> < 0 \<longleftrightarrow> x < 0"
   by (simp add: floor_less_iff)
 
-lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1"
+lemma floor_less_one [simp]: "\<lfloor>x\<rfloor> < 1 \<longleftrightarrow> x < 1"
   by (simp add: floor_less_iff)
 
 lemma floor_less_numeral [simp]:
-  "floor x < numeral v \<longleftrightarrow> x < numeral v"
+  "\<lfloor>x\<rfloor> < numeral v \<longleftrightarrow> x < numeral v"
   by (simp add: floor_less_iff)
 
 lemma floor_less_neg_numeral [simp]:
-  "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
+  "\<lfloor>x\<rfloor> < - numeral v \<longleftrightarrow> x < - numeral v"
   by (simp add: floor_less_iff)
 
 text \<open>Addition and subtraction of integers\<close>
 
-lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z"
+lemma floor_add_of_int [simp]: "\<lfloor>x + of_int z\<rfloor> = \<lfloor>x\<rfloor> + z"
   using floor_correct [of x] by (simp add: floor_unique)
 
 lemma floor_add_numeral [simp]:
-    "floor (x + numeral v) = floor x + numeral v"
+    "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
   using floor_add_of_int [of x "numeral v"] by simp
 
-lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
+lemma floor_add_one [simp]: "\<lfloor>x + 1\<rfloor> = \<lfloor>x\<rfloor> + 1"
   using floor_add_of_int [of x 1] by simp
 
-lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
+lemma floor_diff_of_int [simp]: "\<lfloor>x - of_int z\<rfloor> = \<lfloor>x\<rfloor> - z"
   using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
 
-lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
+lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z"
   by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
 
 lemma floor_diff_numeral [simp]:
-  "floor (x - numeral v) = floor x - numeral v"
+  "\<lfloor>x - numeral v\<rfloor> = \<lfloor>x\<rfloor> - numeral v"
   using floor_diff_of_int [of x "numeral v"] by simp
 
-lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
+lemma floor_diff_one [simp]: "\<lfloor>x - 1\<rfloor> = \<lfloor>x\<rfloor> - 1"
   using floor_diff_of_int [of x 1] by simp
 
 lemma le_mult_floor:
   assumes "0 \<le> a" and "0 \<le> b"
-  shows "floor a * floor b \<le> floor (a * b)"
+  shows "\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor> \<le> \<lfloor>a * b\<rfloor>"
 proof -
-  have "of_int (floor a) \<le> a"
-    and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le)
-  hence "of_int (floor a * floor b) \<le> a * b"
+  have "of_int \<lfloor>a\<rfloor> \<le> a"
+    and "of_int \<lfloor>b\<rfloor> \<le> b" by (auto intro: of_int_floor_le)
+  hence "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> a * b"
     using assms by (auto intro!: mult_mono)
-  also have "a * b < of_int (floor (a * b) + 1)"  
+  also have "a * b < of_int (\<lfloor>a * b\<rfloor> + 1)"
     using floor_correct[of "a * b"] by auto
   finally show ?thesis unfolding of_int_less_iff by simp
 qed
@@ -373,150 +372,145 @@
 
 subsection \<open>Ceiling function\<close>
 
-definition
-  ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
-  "ceiling x = - floor (- x)"
+definition ceiling :: "'a::floor_ceiling \<Rightarrow> int"  ("\<lceil>_\<rceil>")
+  where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
 
-notation (xsymbols)
-  ceiling  ("\<lceil>_\<rceil>")
-
-lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
+lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
   unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) 
 
-lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
+lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> \<lceil>x\<rceil> = z"
   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
 
-lemma le_of_int_ceiling [simp]: "x \<le> of_int (ceiling x)"
+lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
   using ceiling_correct ..
 
-lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
+lemma ceiling_le_iff: "\<lceil>x\<rceil> \<le> z \<longleftrightarrow> x \<le> of_int z"
   unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto
 
-lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x"
+lemma less_ceiling_iff: "z < \<lceil>x\<rceil> \<longleftrightarrow> of_int z < x"
   by (simp add: not_le [symmetric] ceiling_le_iff)
 
-lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1"
+lemma ceiling_less_iff: "\<lceil>x\<rceil> < z \<longleftrightarrow> x \<le> of_int z - 1"
   using ceiling_le_iff [of x "z - 1"] by simp
 
-lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x"
+lemma le_ceiling_iff: "z \<le> \<lceil>x\<rceil> \<longleftrightarrow> of_int z - 1 < x"
   by (simp add: not_less [symmetric] ceiling_less_iff)
 
-lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y"
+lemma ceiling_mono: "x \<ge> y \<Longrightarrow> \<lceil>x\<rceil> \<ge> \<lceil>y\<rceil>"
   unfolding ceiling_def by (simp add: floor_mono)
 
-lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y"
+lemma ceiling_less_cancel: "\<lceil>x\<rceil> < \<lceil>y\<rceil> \<Longrightarrow> x < y"
   by (auto simp add: not_le [symmetric] ceiling_mono)
 
-lemma ceiling_of_int [simp]: "ceiling (of_int z) = z"
+lemma ceiling_of_int [simp]: "\<lceil>of_int z\<rceil> = z"
   by (rule ceiling_unique) simp_all
 
-lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
+lemma ceiling_of_nat [simp]: "\<lceil>of_nat n\<rceil> = int n"
   using ceiling_of_int [of "of_nat n"] by simp
 
-lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
+lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>"
   by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
 
 text \<open>Ceiling with numerals\<close>
 
-lemma ceiling_zero [simp]: "ceiling 0 = 0"
+lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
   using ceiling_of_int [of 0] by simp
 
-lemma ceiling_one [simp]: "ceiling 1 = 1"
+lemma ceiling_one [simp]: "\<lceil>1\<rceil> = 1"
   using ceiling_of_int [of 1] by simp
 
-lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
+lemma ceiling_numeral [simp]: "\<lceil>numeral v\<rceil> = numeral v"
   using ceiling_of_int [of "numeral v"] by simp
 
-lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
+lemma ceiling_neg_numeral [simp]: "\<lceil>- numeral v\<rceil> = - numeral v"
   using ceiling_of_int [of "- numeral v"] by simp
 
-lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
+lemma ceiling_le_zero [simp]: "\<lceil>x\<rceil> \<le> 0 \<longleftrightarrow> x \<le> 0"
   by (simp add: ceiling_le_iff)
 
-lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1"
+lemma ceiling_le_one [simp]: "\<lceil>x\<rceil> \<le> 1 \<longleftrightarrow> x \<le> 1"
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_le_numeral [simp]:
-  "ceiling x \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
+  "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_le_neg_numeral [simp]:
-  "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
+  "\<lceil>x\<rceil> \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   by (simp add: ceiling_le_iff)
 
-lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
+lemma ceiling_less_zero [simp]: "\<lceil>x\<rceil> < 0 \<longleftrightarrow> x \<le> -1"
   by (simp add: ceiling_less_iff)
 
-lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0"
+lemma ceiling_less_one [simp]: "\<lceil>x\<rceil> < 1 \<longleftrightarrow> x \<le> 0"
   by (simp add: ceiling_less_iff)
 
 lemma ceiling_less_numeral [simp]:
-  "ceiling x < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
+  "\<lceil>x\<rceil> < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   by (simp add: ceiling_less_iff)
 
 lemma ceiling_less_neg_numeral [simp]:
-  "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
+  "\<lceil>x\<rceil> < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   by (simp add: ceiling_less_iff)
 
-lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
+lemma zero_le_ceiling [simp]: "0 \<le> \<lceil>x\<rceil> \<longleftrightarrow> -1 < x"
   by (simp add: le_ceiling_iff)
 
-lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x"
+lemma one_le_ceiling [simp]: "1 \<le> \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
   by (simp add: le_ceiling_iff)
 
 lemma numeral_le_ceiling [simp]:
-  "numeral v \<le> ceiling x \<longleftrightarrow> numeral v - 1 < x"
+  "numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> numeral v - 1 < x"
   by (simp add: le_ceiling_iff)
 
 lemma neg_numeral_le_ceiling [simp]:
-  "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
+  "- numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> - numeral v - 1 < x"
   by (simp add: le_ceiling_iff)
 
-lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
+lemma zero_less_ceiling [simp]: "0 < \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
   by (simp add: less_ceiling_iff)
 
-lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x"
+lemma one_less_ceiling [simp]: "1 < \<lceil>x\<rceil> \<longleftrightarrow> 1 < x"
   by (simp add: less_ceiling_iff)
 
 lemma numeral_less_ceiling [simp]:
-  "numeral v < ceiling x \<longleftrightarrow> numeral v < x"
+  "numeral v < \<lceil>x\<rceil> \<longleftrightarrow> numeral v < x"
   by (simp add: less_ceiling_iff)
 
 lemma neg_numeral_less_ceiling [simp]:
-  "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
+  "- numeral v < \<lceil>x\<rceil> \<longleftrightarrow> - numeral v < x"
   by (simp add: less_ceiling_iff)
 
-lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
+lemma ceiling_altdef: "\<lceil>x\<rceil> = (if x = of_int \<lfloor>x\<rfloor> then \<lfloor>x\<rfloor> else \<lfloor>x\<rfloor> + 1)"
   by (intro ceiling_unique, (simp, linarith?)+)
 
-lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
+lemma floor_le_ceiling [simp]: "\<lfloor>x\<rfloor> \<le> \<lceil>x\<rceil>"
+  by (simp add: ceiling_altdef)
 
 text \<open>Addition and subtraction of integers\<close>
 
-lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
+lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
   using ceiling_correct [of x] by (simp add: ceiling_def)
 
-lemma ceiling_add_numeral [simp]:
-    "ceiling (x + numeral v) = ceiling x + numeral v"
+lemma ceiling_add_numeral [simp]: "\<lceil>x + numeral v\<rceil> = \<lceil>x\<rceil> + numeral v"
   using ceiling_add_of_int [of x "numeral v"] by simp
 
-lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
+lemma ceiling_add_one [simp]: "\<lceil>x + 1\<rceil> = \<lceil>x\<rceil> + 1"
   using ceiling_add_of_int [of x 1] by simp
 
-lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z"
+lemma ceiling_diff_of_int [simp]: "\<lceil>x - of_int z\<rceil> = \<lceil>x\<rceil> - z"
   using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)
 
-lemma ceiling_diff_numeral [simp]:
-  "ceiling (x - numeral v) = ceiling x - numeral v"
+lemma ceiling_diff_numeral [simp]: "\<lceil>x - numeral v\<rceil> = \<lceil>x\<rceil> - numeral v"
   using ceiling_diff_of_int [of x "numeral v"] by simp
 
-lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
+lemma ceiling_diff_one [simp]: "\<lceil>x - 1\<rceil> = \<lceil>x\<rceil> - 1"
   using ceiling_diff_of_int [of x 1] by simp
 
-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)"
+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)"
   by (auto simp add: ceiling_unique ceiling_correct)
 
-lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
+lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"
 proof -
   have "of_int \<lceil>x\<rceil> - 1 < x" 
     using ceiling_correct[of x] by simp
@@ -530,15 +524,15 @@
 
 subsection \<open>Negation\<close>
 
-lemma floor_minus: "floor (- x) = - ceiling x"
+lemma floor_minus: "\<lfloor>- x\<rfloor> = - \<lceil>x\<rceil>"
   unfolding ceiling_def by simp
 
-lemma ceiling_minus: "ceiling (- x) = - floor x"
+lemma ceiling_minus: "\<lceil>- x\<rceil> = - \<lfloor>x\<rfloor>"
   unfolding ceiling_def by simp
 
+
 subsection \<open>Frac Function\<close>
 
-
 definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
   "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
 
@@ -642,7 +636,7 @@
   from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
 qed
 
-lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
+lemma round_altdef: "round x = (if frac x \<ge> 1/2 then \<lceil>x\<rceil> else \<lfloor>x\<rfloor>)"
   by (cases "frac x \<ge> 1/2")
      (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
 
@@ -656,18 +650,18 @@
   shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
 proof (cases "of_int m \<ge> z")
   case True
-  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
+  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
     unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
   also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
-  with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+  with True have "\<bar>of_int \<lceil>z\<rceil> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
     by (simp add: ceiling_le_iff)
   finally show ?thesis .
 next
   case False
-  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
+  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lfloor>z\<rfloor> - z\<bar>"
     unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
   also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
-  with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+  with False have "\<bar>of_int \<lfloor>z\<rfloor> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
     by (simp add: le_floor_iff)
   finally show ?thesis .
 qed

--- a/src/HOL/Decision_Procs/MIR.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -29,17 +29,17 @@
   where "x rdvd y \<longleftrightarrow> (\<exists>k::int. y = x * real_of_int k)"
 
 lemma int_rdvd_real:
-  "real_of_int (i::int) rdvd x = (i dvd (floor x) \<and> real_of_int (floor x) = x)" (is "?l = ?r")
+  "real_of_int (i::int) rdvd x = (i dvd \<lfloor>x\<rfloor> \<and> real_of_int \<lfloor>x\<rfloor> = x)" (is "?l = ?r")
 proof
   assume "?l"
   hence th: "\<exists> k. x=real_of_int (i*k)" by (simp add: rdvd_def)
-  hence th': "real_of_int (floor x) = x" by (auto simp del: of_int_mult)
-  with th have "\<exists> k. real_of_int (floor x) = real_of_int (i*k)" by simp
-  hence "\<exists> k. floor x = i*k" by presburger
-  thus ?r  using th' by (simp add: dvd_def)
+  hence th': "real_of_int \<lfloor>x\<rfloor> = x" by (auto simp del: of_int_mult)
+  with th have "\<exists> k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)" by simp
+  hence "\<exists>k. \<lfloor>x\<rfloor> = i*k" by presburger
+  thus ?r using th' by (simp add: dvd_def)
 next
   assume "?r" hence "(i::int) dvd \<lfloor>x::real\<rfloor>" ..
-  hence "\<exists> k. real_of_int (floor x) = real_of_int (i*k)"
+  hence "\<exists>k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)"
     by (metis (no_types) dvd_def)
   thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
 qed
@@ -51,17 +51,18 @@
 lemma rdvd_abs1: "(abs (real_of_int d) rdvd t) = (real_of_int (d ::int) rdvd t)"
 proof
   assume d: "real_of_int d rdvd t"
-  from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real_of_int (floor t) = t"
+  from d int_rdvd_real have d2: "d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
     by auto
 
-  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
+  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd \<lfloor>t\<rfloor>" by blast
   with ti int_rdvd_real[symmetric] have "real_of_int (abs d) rdvd t" by blast
   thus "abs (real_of_int d) rdvd t" by simp
 next
   assume "abs (real_of_int d) rdvd t" hence "real_of_int (abs d) rdvd t" by simp
-  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"
+  with int_rdvd_real[where i="abs d" and x="t"]
+  have d2: "abs d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
     by auto
-  from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
+  from iffD1[OF abs_dvd_iff] d2 have "d dvd \<lfloor>t\<rfloor>" by blast
   with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
 qed
 
@@ -107,11 +108,11 @@
 | "Inum bs (Add a b) = Inum bs a + Inum bs b"
 | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
 | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
-| "Inum bs (Floor a) = real_of_int (floor (Inum bs a))"
-| "Inum bs (CF c a b) = real_of_int c * real_of_int (floor (Inum bs a)) + Inum bs b"
-definition "isint t bs \<equiv> real_of_int (floor (Inum bs t)) = Inum bs t"
-
-lemma isint_iff: "isint n bs = (real_of_int (floor (Inum bs n)) = Inum bs n)"
+| "Inum bs (Floor a) = real_of_int \<lfloor>Inum bs a\<rfloor>"
+| "Inum bs (CF c a b) = real_of_int c * real_of_int \<lfloor>Inum bs a\<rfloor> + Inum bs b"
+definition "isint t bs \<equiv> real_of_int \<lfloor>Inum bs t\<rfloor> = Inum bs t"
+
+lemma isint_iff: "isint n bs = (real_of_int \<lfloor>Inum bs n\<rfloor> = Inum bs n)"
   by (simp add: isint_def)
 
 lemma isint_Floor: "isint (Floor n) bs"
@@ -120,10 +121,10 @@
 lemma isint_Mul: "isint e bs \<Longrightarrow> isint (Mul c e) bs"
 proof-
   let ?e = "Inum bs e"
-  let ?fe = "floor ?e"
-  assume be: "isint e bs" hence efe:"real_of_int ?fe = ?e" by (simp add: isint_iff)
-  have "real_of_int ((floor (Inum bs (Mul c e)))) = real_of_int (floor (real_of_int (c * ?fe)))" using efe by simp
-  also have "\<dots> = real_of_int (c* ?fe)"  by (metis floor_of_int)
+  assume be: "isint e bs" hence efe:"real_of_int \<lfloor>?e\<rfloor> = ?e" by (simp add: isint_iff)
+  have "real_of_int \<lfloor>Inum bs (Mul c e)\<rfloor> = real_of_int \<lfloor>real_of_int (c * \<lfloor>?e\<rfloor>)\<rfloor>"
+    using efe by simp
+  also have "\<dots> = real_of_int (c* \<lfloor>?e\<rfloor>)" by (metis floor_of_int)
   also have "\<dots> = real_of_int c * ?e" using efe by simp
   finally show ?thesis using isint_iff by simp
 qed
@@ -132,9 +133,10 @@
 proof-
   let ?I = "\<lambda> t. Inum bs t"
   assume ie: "isint e bs"
-  hence th: "real_of_int (floor (?I e)) = ?I e" by (simp add: isint_def)
-  have "real_of_int (floor (?I (Neg e))) = real_of_int (floor (- (real_of_int (floor (?I e)))))" by (simp add: th)
-  also have "\<dots> = - real_of_int (floor (?I e))" by simp
+  hence th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def)
+  have "real_of_int \<lfloor>?I (Neg e)\<rfloor> = real_of_int \<lfloor>- (real_of_int \<lfloor>?I e\<rfloor>)\<rfloor>"
+    by (simp add: th)
+  also have "\<dots> = - real_of_int \<lfloor>?I e\<rfloor>" by simp
   finally show "isint (Neg e) bs" by (simp add: isint_def th)
 qed
 
@@ -142,9 +144,10 @@
   assumes ie: "isint e bs" shows "isint (Sub (C c) e) bs"
 proof-
   let ?I = "\<lambda> t. Inum bs t"
-  from ie have th: "real_of_int (floor (?I e)) = ?I e" by (simp add: isint_def)
-  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)
-  also have "\<dots> = real_of_int (c- floor (?I e))" by simp
+  from ie have th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def)
+  have "real_of_int \<lfloor>?I (Sub (C c) e)\<rfloor> = real_of_int \<lfloor>real_of_int (c - \<lfloor>?I e\<rfloor>)\<rfloor>"
+    by (simp add: th)
+  also have "\<dots> = real_of_int (c - \<lfloor>?I e\<rfloor>)" by simp
   finally show "isint (Sub (C c) e) bs" by (simp add: isint_def th)
 qed
 
@@ -154,9 +157,9 @@
 proof-
   let ?a = "Inum bs a"
   let ?b = "Inum bs b"
-  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)))"
+  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>"
     by simp
-  also have "\<dots> = real_of_int (floor ?a) + real_of_int (floor ?b)" by simp
+  also have "\<dots> = real_of_int \<lfloor>?a\<rfloor> + real_of_int \<lfloor>?b\<rfloor>" by simp
   also have "\<dots> = ?a + ?b" using ai bi isint_iff by simp
   finally show "isint (Add a b) bs" by (simp add: isint_iff)
 qed
@@ -830,15 +833,15 @@
     hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)"
       by (cases ?tv) (auto simp add: numfloor_def Let_def split_def)
     from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+
-    hence "?N (Floor t) = real_of_int (floor (?N (Add ?tv ?ti)))" by simp
-    also have "\<dots> = real_of_int (floor (?N ?tv) + (floor (?N ?ti)))"
+    hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp
+    also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)"
       by (simp,subst tii[simplified isint_iff, symmetric]) simp
     also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])
     finally have ?thesis using th1 by simp}
   moreover {fix v assume H:"?tv = C v"
     from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+
-    hence "?N (Floor t) = real_of_int (floor (?N (Add ?tv ?ti)))" by simp
-    also have "\<dots> = real_of_int (floor (?N ?tv) + (floor (?N ?ti)))"
+    hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp
+    also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)"
       by (simp,subst tii[simplified isint_iff, symmetric]) simp
     also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])
     finally have ?thesis by (simp add: H numfloor_def Let_def split_def) }
@@ -1520,11 +1523,11 @@
   hence na: "?N a" using th by simp
   have th': "(real_of_int ?nt)*(real_of_int x) = real_of_int (?nt * x)" by simp
   have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp
-  also have "\<dots> = real_of_int (floor ((real_of_int ?nt)* real_of_int(x) + ?I x ?at))" by simp
-  also have "\<dots> = real_of_int (floor (?I x ?at + real_of_int (?nt* x)))" by (simp add: ac_simps)
-  also have "\<dots> = real_of_int (floor (?I x ?at) + (?nt* x))"
-    using floor_add_of_int[of "?I x ?at" "?nt* x"] by simp
-  also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int (floor (?I x ?at))" by (simp add: ac_simps)
+  also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp
+  also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)
+  also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"
+    using floor_add_of_int[of "?I x ?at" "?nt * x"] by simp
+  also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)
   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
   with na show ?case by simp
 qed
@@ -1622,26 +1625,28 @@
   "zlfm p = p" (hints simp add: fmsize_pos)
 
 lemma split_int_less_real:
-  "(real_of_int (a::int) < b) = (a < floor b \<or> (a = floor b \<and> real_of_int (floor b) < b))"
+  "(real_of_int (a::int) < b) = (a < \<lfloor>b\<rfloor> \<or> (a = \<lfloor>b\<rfloor> \<and> real_of_int \<lfloor>b\<rfloor> < b))"
 proof( auto)
-  assume alb: "real_of_int a < b" and agb: "\<not> a < floor b"
-  from agb have "floor b \<le> a" by simp hence th: "b < real_of_int a + 1" by (simp only: floor_le_iff)
-  from floor_eq[OF alb th] show "a= floor b" by simp
+  assume alb: "real_of_int a < b" and agb: "\<not> a < \<lfloor>b\<rfloor>"
+  from agb have "\<lfloor>b\<rfloor> \<le> a" by simp
+  hence th: "b < real_of_int a + 1" by (simp only: floor_le_iff)
+  from floor_eq[OF alb th] show "a = \<lfloor>b\<rfloor>" by simp
 next
-  assume alb: "a < floor b"
-  hence "real_of_int a < real_of_int (floor b)" by simp
-  moreover have "real_of_int (floor b) \<le> b" by simp ultimately show  "real_of_int a < b" by arith
+  assume alb: "a < \<lfloor>b\<rfloor>"
+  hence "real_of_int a < real_of_int \<lfloor>b\<rfloor>" by simp
+  moreover have "real_of_int \<lfloor>b\<rfloor> \<le> b" by simp
+  ultimately show  "real_of_int a < b" by arith
 qed
 
 lemma split_int_less_real':
-  "(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))"
+  "(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))"
 proof-
   have "(real_of_int a + b <0) = (real_of_int a < -b)" by arith
   with split_int_less_real[where a="a" and b="-b"] show ?thesis by arith
 qed
 
 lemma split_int_gt_real':
-  "(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))"
+  "(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))"
 proof-
   have th: "(real_of_int a + b >0) = (real_of_int (-a) + (-b)< 0)" by arith
   show ?thesis 
@@ -1649,36 +1654,36 @@
 qed
 
 lemma split_int_le_real:
-  "(real_of_int (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real_of_int (floor b) < b))"
+  "(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))"
 proof( auto)
-  assume alb: "real_of_int a \<le> b" and agb: "\<not> a \<le> floor b"
-  from alb have "floor (real_of_int a) \<le> floor b " by (simp only: floor_mono)
-  hence "a \<le> floor b" by simp with agb show "False" by simp
+  assume alb: "real_of_int a \<le> b" and agb: "\<not> a \<le> \<lfloor>b\<rfloor>"
+  from alb have "\<lfloor>real_of_int a\<rfloor> \<le> \<lfloor>b\<rfloor>" by (simp only: floor_mono)
+  hence "a \<le> \<lfloor>b\<rfloor>" by simp with agb show "False" by simp
 next
-  assume alb: "a \<le> floor b"
-  hence "real_of_int a \<le> real_of_int (floor b)" by (simp only: floor_mono)
+  assume alb: "a \<le> \<lfloor>b\<rfloor>"
+  hence "real_of_int a \<le> real_of_int \<lfloor>b\<rfloor>" by (simp only: floor_mono)
   also have "\<dots>\<le> b" by simp  finally show  "real_of_int a \<le> b" .
 qed
 
 lemma split_int_le_real':
-  "(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))"
+  "(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))"
 proof-
   have "(real_of_int a + b \<le>0) = (real_of_int a \<le> -b)" by arith
   with split_int_le_real[where a="a" and b="-b"] show ?thesis by arith
 qed
 
 lemma split_int_ge_real':
-  "(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))"
+  "(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))"
 proof-
   have th: "(real_of_int a + b \<ge>0) = (real_of_int (-a) + (-b) \<le> 0)" by arith
   show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
     (simp add: algebra_simps ,arith)
 qed
 
-lemma split_int_eq_real: "(real_of_int (a::int) = b) = ( a = floor b \<and> b = real_of_int (floor b))" (is "?l = ?r")
+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")
 by auto
 
-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")
+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")
 proof-
   have "?l = (real_of_int a = -b)" by arith
   with split_int_eq_real[where a="a" and b="-b"] show ?thesis by simp arith
@@ -1862,8 +1867,8 @@
       using Ia by (simp add: Let_def split_def)
     also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
-       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r))))"
+    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
       by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
@@ -1876,11 +1881,11 @@
       using Ia by (simp add: Let_def split_def)
     also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
-       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r))))"
+    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
       by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
-      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + floor (?N ?r))", simplified, symmetric]
+      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
@@ -1908,8 +1913,8 @@
       using Ia by (simp add: Let_def split_def)
     also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
-       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r)))))"
+    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
       by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
@@ -1922,11 +1927,11 @@
       using Ia by (simp add: Let_def split_def)
     also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real_of_int (?c*i))) \<and>
-       (real_of_int (floor ((?N ?r) + real_of_int (?c*i))) = (real_of_int (?c*i) + (?N ?r)))))"
+    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+       (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
       by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
-      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + floor (?N ?r))", simplified, symmetric]
+      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
@@ -2045,7 +2050,7 @@
   hence rcpos: "real_of_int c > 0" by simp
   from 3 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2062,7 +2067,7 @@
   then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   from 4 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2079,7 +2084,7 @@
   then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   from 5 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2095,7 +2100,7 @@
   then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   from 6 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2111,7 +2116,7 @@
   then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   from 7 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2127,7 +2132,7 @@
   then have "c > 0" by simp hence rcpos: "real_of_int c > 0" by simp
   from 8 have nbe: "numbound0 e" by simp
   fix y
-  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))"
+  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))"
   proof (simp add: less_floor_iff , rule allI, rule impI)
     fix x :: int
     assume A: "real_of_int x + 1 \<le> - (Inum (y # bs) e / real_of_int c)"
@@ -2580,7 +2585,7 @@
   case (7 c e) hence p: "Ifm (real_of_int x #bs) (Gt (CN 0 c e))" and c1: "c=1"
     and bn:"numbound0 e" and ie1:"isint e (a#bs)" using dvd1_eq1[where x="c"] by simp_all
   let ?e = "Inum (real_of_int x # bs) e"
-  from ie1 have ie: "real_of_int (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"]
+  from ie1 have ie: "real_of_int \<lfloor>?e\<rfloor> = ?e" using isint_iff[where n="e" and bs="a#bs"]
       numbound0_I[OF bn,where b="a" and b'="real_of_int x" and bs="bs"]
     by (simp add: isint_iff)
     {assume "real_of_int (x-d) +?e > 0" hence ?case using c1
@@ -2593,11 +2598,11 @@
       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"]]
       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real_of_int x =  - ?e + real_of_int j)" by auto
       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)
-      hence "real_of_int (x + floor ?e) > real_of_int (0::int) \<and> real_of_int (x + floor ?e) \<le> real_of_int d"
+      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"
         using ie by simp
-      hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e" by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = real_of_int (- floor ?e + j)" by force
+      hence "x + \<lfloor>?e\<rfloor> \<ge> 1 \<and> x + \<lfloor>?e\<rfloor> \<le> d"  by simp
+      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + \<lfloor>?e\<rfloor>" by simp
+      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = real_of_int (- \<lfloor>?e\<rfloor> + j)" by force
       hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x = - ?e + real_of_int j"
         by (simp add: ie[simplified isint_iff])
       with nob have ?case by auto}
@@ -2606,7 +2611,7 @@
   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"
     and ie1:"isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
     let ?e = "Inum (real_of_int x # bs) e"
-    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"]
+    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"]
       by (simp add: isint_iff)
     {assume "real_of_int (x-d) +?e \<ge> 0" hence ?case using  c1
       numbound0_I[OF bn,where b="real_of_int (x-d)" and b'="real_of_int x" and bs="bs"]
@@ -2618,12 +2623,12 @@
       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"]]
       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real_of_int x =  - ?e - 1 + real_of_int j)" by auto
       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)
-      hence "real_of_int (x + floor ?e) \<ge> real_of_int (0::int) \<and> real_of_int (x + floor ?e) < real_of_int d"
+      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"
         using ie by simp
-      hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps)
-      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by presburger
+      hence "x + \<lfloor>?e\<rfloor> + 1 \<ge> 1 \<and> x + \<lfloor>?e\<rfloor> + 1 \<le> d" by simp
+      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + \<lfloor>?e\<rfloor> + 1" by simp
+      hence "\<exists> (j::int) \<in> {1 .. d}. x= - \<lfloor>?e\<rfloor> - 1 + j" by (simp add: algebra_simps)
+      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- \<lfloor>?e\<rfloor> - 1 + j)" by presburger
       hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= - ?e - 1 + real_of_int j"
         by (simp add: ie[simplified isint_iff])
       with nob have ?case by simp }
@@ -2657,16 +2662,16 @@
     and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
   let ?e = "Inum (real_of_int x # bs) e"
   from 9 have "isint e (a #bs)"  by simp
-  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"]
+  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"]
     by (simp add: isint_iff)
   from 9 have id: "j dvd d" by simp
-  from c1 ie[symmetric] have "?p x = (real_of_int j rdvd real_of_int (x+ floor ?e))" by simp
-  also have "\<dots> = (j dvd x + floor ?e)"
-    using int_rdvd_real[where i="j" and x="real_of_int (x+ floor ?e)"] by simp
-  also have "\<dots> = (j dvd x - d + floor ?e)"
-    using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp
-  also have "\<dots> = (real_of_int j rdvd real_of_int (x - d + floor ?e))"
-    using int_rdvd_real[where i="j" and x="real_of_int (x-d + floor ?e)",symmetric, simplified]
+  from c1 ie[symmetric] have "?p x = (real_of_int j rdvd real_of_int (x + \<lfloor>?e\<rfloor>))" by simp
+  also have "\<dots> = (j dvd x + \<lfloor>?e\<rfloor>)"
+    using int_rdvd_real[where i="j" and x="real_of_int (x + \<lfloor>?e\<rfloor>)"] by simp
+  also have "\<dots> = (j dvd x - d + \<lfloor>?e\<rfloor>)"
+    using dvd_period[OF id, where x="x" and c="-1" and t="\<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = (real_of_int j rdvd real_of_int (x - d + \<lfloor>?e\<rfloor>))"
+    using int_rdvd_real[where i="j" and x="real_of_int (x - d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
       ie by simp
   also have "\<dots> = (real_of_int j rdvd real_of_int x - real_of_int d + ?e)"
     using ie by simp
@@ -2676,16 +2681,16 @@
   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+
   let ?e = "Inum (real_of_int x # bs) e"
   from 10 have "isint e (a#bs)"  by simp
-  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"]
+  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"]
     by (simp add: isint_iff)
   from 10 have id: "j dvd d" by simp
-  from c1 ie[symmetric] have "?p x = (\<not> real_of_int j rdvd real_of_int (x+ floor ?e))" by simp
-  also have "\<dots> = (\<not> j dvd x + floor ?e)"
-    using int_rdvd_real[where i="j" and x="real_of_int (x+ floor ?e)"] by simp
-  also have "\<dots> = (\<not> j dvd x - d + floor ?e)"
-    using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp
-  also have "\<dots> = (\<not> real_of_int j rdvd real_of_int (x - d + floor ?e))"
-    using int_rdvd_real[where i="j" and x="real_of_int (x-d + floor ?e)",symmetric, simplified]
+  from c1 ie[symmetric] have "?p x = (\<not> real_of_int j rdvd real_of_int (x + \<lfloor>?e\<rfloor>))" by simp
+  also have "\<dots> = (\<not> j dvd x + \<lfloor>?e\<rfloor>)"
+    using int_rdvd_real[where i="j" and x="real_of_int (x + \<lfloor>?e\<rfloor>)"] by simp
+  also have "\<dots> = (\<not> j dvd x - d + \<lfloor>?e\<rfloor>)"
+    using dvd_period[OF id, where x="x" and c="-1" and t="\<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = (\<not> real_of_int j rdvd real_of_int (x - d + \<lfloor>?e\<rfloor>))"
+    using int_rdvd_real[where i="j" and x="real_of_int (x - d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
       ie by simp
   also have "\<dots> = (\<not> real_of_int j rdvd real_of_int x - real_of_int d + ?e)"
     using ie by simp
@@ -2745,12 +2750,12 @@
 proof-
   from minusinf_inf[OF lp]
   have th: "\<exists>(z::int). \<forall>x<z. ?P (real_of_int x) = ?M x" by blast
-  let ?B' = "{floor (?I b) | b. b\<in> ?B}"
-  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
+  let ?B' = "{\<lfloor>?I b\<rfloor> | b. b\<in> ?B}"
+  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
   from B[rule_format]
-  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))"
+  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))"
     by simp
-  also have "\<dots> = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int (floor (?I b) + j)))" by simp
+  also have "\<dots> = (\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (real_of_int (\<lfloor>?I b\<rfloor> + j)))" by simp
   also have"\<dots> = (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P (real_of_int (b + j)))"  by blast
   finally have BB':
     "(\<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)))"
@@ -2820,23 +2825,22 @@
   and kpos: "real_of_int k > 0"
   and tnb: "numbound0 t"
   and tint: "isint t (real_of_int x#bs)"
-  and kdt: "k dvd floor (Inum (b'#bs) t)"
-  shows "Ifm (real_of_int x#bs) (\<sigma>_\<rho> p (t,k)) =
-  (Ifm ((real_of_int ((floor (Inum (b'#bs) t)) div k))#bs) p)"
-  (is "?I (real_of_int x) (?s p) = (?I (real_of_int ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)")
+  and kdt: "k dvd \<lfloor>Inum (b'#bs) t\<rfloor>"
+  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)"
+  (is "?I (real_of_int x) (?s p) = (?I (real_of_int (\<lfloor>?N b' t\<rfloor> div k)) p)" is "_ = (?I ?tk p)")
 using linp kpos tnb
 proof(induct p rule: \<sigma>_\<rho>.induct)
   case (3 c e)
   from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
     from kpos have knz': "real_of_int k \<noteq> 0" by simp
-    from tint have ti: "real_of_int (floor (?N (real_of_int x) t)) = ?N (real_of_int x) t"
+    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
     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)"
       using real_of_int_div[OF kdt]
@@ -2855,14 +2859,14 @@
   case (4 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
     from kpos have knz': "real_of_int k \<noteq> 0" by simp
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -2880,13 +2884,13 @@
   case (5 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -2904,13 +2908,13 @@
   case (6 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -2928,13 +2932,13 @@
   case (7 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -2952,13 +2956,13 @@
   case (8 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -2976,14 +2980,14 @@
   case (9 i c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
     from kpos have knz: "k\<noteq>0" by simp hence knz': "real_of_int k \<noteq> 0" by simp
-    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
+    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
     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)"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -3000,14 +3004,14 @@
   case (10 i c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c"
-    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
+    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
     from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real_of_int x"] by (simp add: ti) }
   moreover
   { assume *: "\<not> k dvd c"
     from kpos have knz: "k\<noteq>0" by simp hence knz': "real_of_int k \<noteq> 0" by simp
-    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
+    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
     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))"
       using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real_of_int x"]
@@ -3020,8 +3024,8 @@
       by (simp add: ti)
     finally have ?case . }
   ultimately show ?case by blast
-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"]
-  numbound0_I[where bs="bs" and b="real_of_int ((floor (?N b' t)) div k)" and b'="real_of_int x"])
+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"]
+  numbound0_I[where bs="bs" and b="real_of_int (\<lfloor>?N b' t\<rfloor> div k)" and b'="real_of_int x"])
 
 
 lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
@@ -3088,7 +3092,7 @@
     and nob: "\<forall> j\<in> {1 .. c*d}. real_of_int (c*i) \<noteq> - ?N i e + real_of_int j"
     and pi: "real_of_int (c*i) + ?N i e > 0" and cp': "real_of_int c >0"
     by simp+
-  let ?fe = "floor (?N i e)"
+  let ?fe = "\<lfloor>?N i e\<rfloor>"
   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)
   from pi ei[simplified isint_iff] have "real_of_int (c*i + ?fe) > real_of_int (0::int)" by simp
   hence pi': "c*i + ?fe > 0" by (simp only: of_int_less_iff[symmetric])
@@ -3111,7 +3115,7 @@
     and nob: "\<forall> j\<in> {1 .. c*d}. real_of_int (c*i) \<noteq> - 1 - ?N i e + real_of_int j"
     and pi: "real_of_int (c*i) + ?N i e \<ge> 0" and cp': "real_of_int c >0"
     by simp+
-  let ?fe = "floor (?N i e)"
+  let ?fe = "\<lfloor>?N i e\<rfloor>"
   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)
   from pi ei[simplified isint_iff] have "real_of_int (c*i + ?fe) \<ge> real_of_int (0::int)" by simp
   hence pi': "c*i + 1 + ?fe \<ge> 1" by (simp only: of_int_le_iff[symmetric])
@@ -3137,16 +3141,16 @@
   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+
   let ?e = "Inum (real_of_int i # bs) e"
   from 9 have "isint e (real_of_int i #bs)"  by simp
-  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"]
+  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"]
     by (simp add: isint_iff)
   from 9 have id: "j dvd d" by simp
-  from ie[symmetric] have "?p i = (real_of_int j rdvd real_of_int (c*i+ floor ?e))" by simp
-  also have "\<dots> = (j dvd c*i + floor ?e)"
-    using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp
-  also have "\<dots> = (j dvd c*i - c*d + floor ?e)"
-    using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
-  also have "\<dots> = (real_of_int j rdvd real_of_int (c*i - c*d + floor ?e))"
-    using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
+  from ie[symmetric] have "?p i = (real_of_int j rdvd real_of_int (c*i + \<lfloor>?e\<rfloor>))" by simp
+  also have "\<dots> = (j dvd c*i + \<lfloor>?e\<rfloor>)"
+    using int_rdvd_iff [where i="j" and t="c*i + \<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = (j dvd c*i - c*d + \<lfloor>?e\<rfloor>)"
+    using dvd_period[OF id, where x="c*i" and c="-c" and t="\<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = (real_of_int j rdvd real_of_int (c*i - c*d + \<lfloor>?e\<rfloor>))"
+    using int_rdvd_iff[where i="j" and t="(c*i - c*d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
       ie by simp
   also have "\<dots> = (real_of_int j rdvd real_of_int (c*(i - d)) + ?e)"
     using ie by (simp add:algebra_simps)
@@ -3159,17 +3163,17 @@
     by simp+
   let ?e = "Inum (real_of_int i # bs) e"
   from 10 have "isint e (real_of_int i #bs)"  by simp
-  hence ie: "real_of_int (floor ?e) = ?e"
+  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"]
     by (simp add: isint_iff)
   from 10 have id: "j dvd d" by simp
-  from ie[symmetric] have "?p i = (\<not> (real_of_int j rdvd real_of_int (c*i+ floor ?e)))" by simp
-  also have "\<dots> = Not (j dvd c*i + floor ?e)"
-    using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp
-  also have "\<dots> = Not (j dvd c*i - c*d + floor ?e)"
-    using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
-  also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*i - c*d + floor ?e))"
-    using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
+  from ie[symmetric] have "?p i = (\<not> (real_of_int j rdvd real_of_int (c*i + \<lfloor>?e\<rfloor>)))" by simp
+  also have "\<dots> = Not (j dvd c*i + \<lfloor>?e\<rfloor>)"
+    using int_rdvd_iff [where i="j" and t="c*i + \<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = Not (j dvd c*i - c*d + \<lfloor>?e\<rfloor>)"
+    using dvd_period[OF id, where x="c*i" and c="-c" and t="\<lfloor>?e\<rfloor>"] by simp
+  also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*i - c*d + \<lfloor>?e\<rfloor>))"
+    using int_rdvd_iff[where i="j" and t="(c*i - c*d + \<lfloor>?e\<rfloor>)",symmetric, simplified]
       ie by simp
   also have "\<dots> = Not (real_of_int j rdvd real_of_int (c*(i - d)) + ?e)"
     using ie by (simp add:algebra_simps)
@@ -3195,20 +3199,19 @@
     fix e c j assume ecR: "(e,c) \<in> set (\<rho> p)" and jD: "j\<in> {1 .. c*d}"
       and cx: "real_of_int (c*x) = Inum (real_of_int x#bs) e + real_of_int j"
     let ?e = "Inum (real_of_int x#bs) e"
-    let ?fe = "floor ?e"
     from \<rho>_l[OF lp'] ecR have ei:"isint e (real_of_int x#bs)" and cp:"c>0" and nb:"numbound0 e"
       by auto
     from numbound0_gen [OF nb ei, rule_format,where y="a"] have "isint e (a#bs)" .
-    from cx ei[simplified isint_iff] have "real_of_int (c*x) = real_of_int (?fe + j)" by simp
-    hence cx: "c*x = ?fe + j" by (simp only: of_int_eq_iff)
-    hence cdej:"c dvd ?fe + j" by (simp add: dvd_def) (rule_tac x="x" in exI, simp)
-    hence "real_of_int c rdvd real_of_int (?fe + j)" by (simp only: int_rdvd_iff)
+    from cx ei[simplified isint_iff] have "real_of_int (c*x) = real_of_int (\<lfloor>?e\<rfloor> + j)" by simp
+    hence cx: "c*x = \<lfloor>?e\<rfloor> + j" by (simp only: of_int_eq_iff)
+    hence cdej:"c dvd \<lfloor>?e\<rfloor> + j" by (simp add: dvd_def) (rule_tac x="x" in exI, simp)
+    hence "real_of_int c rdvd real_of_int (\<lfloor>?e\<rfloor> + j)" by (simp only: int_rdvd_iff)
     hence rcdej: "real_of_int c rdvd ?e + real_of_int j" by (simp add: ei[simplified isint_iff])
-    from cx have "(c*x) div c = (?fe + j) div c" by simp
-    with cp have "x = (?fe + j) div c" by simp
-    with px have th: "?P ((?fe + j) div c)" by auto
+    from cx have "(c*x) div c = (\<lfloor>?e\<rfloor> + j) div c" by simp
+    with cp have "x = (\<lfloor>?e\<rfloor> + j) div c" by simp
+    with px have th: "?P ((\<lfloor>?e\<rfloor> + j) div c)" by auto
     from cp have cp': "real_of_int c > 0" by simp
-    from cdej have cdej': "c dvd floor (Inum (real_of_int x#bs) (Add e (C j)))" by simp
+    from cdej have cdej': "c dvd \<lfloor>Inum (real_of_int x#bs) (Add e (C j))\<rfloor>" by simp
     from nb have nb': "numbound0 (Add e (C j))" by simp
     have ji: "isint (C j) (real_of_int x#bs)" by (simp add: isint_def)
     from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real_of_int x#bs)" .
@@ -3246,8 +3249,8 @@
     from spx' have rcdej:"real_of_int c rdvd (Inum (real_of_int i#bs) (Add e (C j)))"
       and sr:"Ifm (real_of_int i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
     from rcdej eji[simplified isint_iff]
-    have "real_of_int c rdvd real_of_int (floor (Inum (real_of_int i#bs) (Add e (C j))))" by simp
-    hence cdej:"c dvd floor (Inum (real_of_int i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff)
+    have "real_of_int c rdvd real_of_int \<lfloor>Inum (real_of_int i#bs) (Add e (C j))\<rfloor>" by simp
+    hence cdej:"c dvd \<lfloor>Inum (real_of_int i#bs) (Add e (C j))\<rfloor>" by (simp only: int_rdvd_iff)
     from cp have cp': "real_of_int c > 0" by simp
     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)"
       by (simp add: \<sigma>_def)
@@ -3413,12 +3416,12 @@
       hence nb: "numbound0 s'" by simp
       from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by simp
       let ?nxs = "CN 0 n' s'"
-      let ?l = "floor (?N s') + j"
+      let ?l = "\<lfloor>?N s'\<rfloor> + j"
       from H
       have "?I (?p (p',n',s') j) \<longrightarrow>
           (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
         by (simp add: fp_def np algebra_simps)
-      also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
+      also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
         using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
       moreover
       have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
@@ -3439,12 +3442,12 @@
       hence nb: "numbound0 s'" by simp
       from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by simp
       let ?nxs = "CN 0 n' s'"
-      let ?l = "floor (?N s') + j"
+      let ?l = "\<lfloor>?N s'\<rfloor> + j"
       from H
       have "?I (?p (p',n',s') j) \<longrightarrow>
           (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
         by (simp add: np fp_def algebra_simps)
-      also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
+      also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
         using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
       moreover
       have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"  by simp
@@ -3461,7 +3464,7 @@
 lemma real_in_int_intervals:
   assumes xb: "real_of_int m \<le> x \<and> x < real_of_int ((n::int) + 1)"
   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")
-by (rule bexI[where P="?P" and x="floor x" and A="?N"])
+by (rule bexI[where P="?P" and x="\<lfloor>x\<rfloor>" and A="?N"])
 (auto simp add: floor_less_iff[where x="x" and z="n+1", simplified]
   xb[simplified] floor_mono[where x="real_of_int m" and y="x", OF conjunct1[OF xb], simplified floor_of_int[where z="m"]])
 
@@ -3760,9 +3763,9 @@
 
 lemma rdvd01_cs:
   assumes up: "u \<ge> 0" and u1: "u<1" and np: "real_of_int n > 0"
-  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")
+  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")
 proof-
-  let ?ss = "s - real_of_int (floor s)"
+  let ?ss = "s - real_of_int \<lfloor>s\<rfloor>"
   from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
     of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1" by (auto simp: floor_less_cancel)
   from np have n0: "real_of_int n \<ge> 0" by simp
@@ -3770,10 +3773,10 @@
   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
   from int_rdvd_real[where i="i" and x="real_of_int (n::int) * u - s"]
   have "real_of_int i rdvd real_of_int n * u - s =
-    (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 ))"
+    (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 ))"
     (is "_ = (?DE)" is "_ = (?D \<and> ?E)") by simp
-  also have "\<dots> = (?DE \<and> real_of_int(floor (real_of_int n * u - s) + floor s)\<ge> -?ss
-    \<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 < _)")
+  also have "\<dots> = (?DE \<and> real_of_int (\<lfloor>real_of_int n * u - s\<rfloor> + \<lfloor>s\<rfloor>) \<ge> -?ss
+    \<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 < _)")
     using nu0 nun  by auto
   also have "\<dots> = (?DE \<and> ?a \<ge> 0 \<and> ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1])
   also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. ?a = j))" by simp
@@ -3804,7 +3807,7 @@
   from foldr_disj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
     by (simp add: np DVDJ_def)
-  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)))"
+  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>))"
     by (simp add: algebra_simps)
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
   have "\<dots> = (real_of_int i rdvd real_of_int n * x - (-?s))" by simp
@@ -3820,7 +3823,7 @@
   from foldr_conj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
     by (simp add: np NDVDJ_def)
-  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))))"
+  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>)))"
     by (simp add: algebra_simps)
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
   have "\<dots> = (\<not> (real_of_int i rdvd real_of_int n * x - (-?s)))" by simp
@@ -4752,7 +4755,7 @@
 proof(auto)
   fix x
   assume Px: "P x"
-  let ?i = "floor x"
+  let ?i = "\<lfloor>x\<rfloor>"
   let ?u = "x - real_of_int ?i"
   have "x = real_of_int ?i + ?u" by simp
   hence "P (real_of_int ?i + ?u)" using Px by simp

--- a/src/HOL/Library/Float.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Library/Float.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -619,10 +619,10 @@
 subsection \<open>Rounding Real Numbers\<close>
 
 definition round_down :: "int \<Rightarrow> real \<Rightarrow> real"
-  where "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec"
+  where "round_down prec x = \<lfloor>x * 2 powr prec\<rfloor> * 2 powr -prec"
 
 definition round_up :: "int \<Rightarrow> real \<Rightarrow> real"
-  where "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec"
+  where "round_up prec x = \<lceil>x * 2 powr prec\<rceil> * 2 powr -prec"
 
 lemma round_down_float[simp]: "round_down prec x \<in> float"
   unfolding round_down_def
@@ -648,7 +648,7 @@
   "round_up prec x - round_down prec x \<le> 2 powr -prec"
 proof -
   have "round_up prec x - round_down prec x =
-    (ceiling (x * 2 powr prec) - floor (x * 2 powr prec)) * 2 powr -prec"
+    (\<lceil>x * 2 powr prec\<rceil> - \<lfloor>x * 2 powr prec\<rfloor>) * 2 powr -prec"
     by (simp add: round_up_def round_down_def field_simps)
   also have "\<dots> \<le> 1 * 2 powr -prec"
     by (rule mult_mono)
@@ -889,7 +889,7 @@
 proof
   show "2 ^ nat (bitlen x - 1) \<le> x"
   proof -
-    have "(2::real) ^ nat \<lfloor>log 2 (real_of_int x)\<rfloor> = 2 powr real_of_int (floor (log 2 (real_of_int x)))"
+    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>"
       using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real_of_int x)\<rfloor>"] \<open>x > 0\<close>
       by simp
     also have "\<dots> \<le> 2 powr log 2 (real_of_int x)"
@@ -2244,15 +2244,18 @@
   "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   apply transfer
   apply (simp add: powr_int floor_divide_of_int_eq)
-  by (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
+  apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
+  done
 
-lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int (floor x)" by simp
+lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int \<lfloor>x\<rfloor>"
+  by simp
 
 qualified lemma compute_floor_fl[code]:
   "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   apply transfer
   apply (simp add: powr_int floor_divide_of_int_eq)
-  by (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
+  apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
+  done
 
 end
 

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -4830,7 +4830,7 @@
   case False
   have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \<i>) \<le> b + cmod (Ln w)}"
     apply (simp add: norm_mult finite_int_iff_bounded_le)
-    apply (rule_tac x="floor ((b + cmod (Ln w)) / (2*pi))" in exI)
+    apply (rule_tac x="\<lfloor>(b + cmod (Ln w)) / (2*pi)\<rfloor>" in exI)
     apply (auto simp: divide_simps le_floor_iff)
     done
   have [simp]: "\<And>P f. {z. P z \<and> (\<exists>n. z = f n)} = f ` {n. P (f n)}"

--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -1595,7 +1595,7 @@
     using e   by (auto simp: field_simps)
   with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
     apply (auto simp: norm_divide norm_powr_real divide_simps)
-    apply (rule_tac x="nat (ceiling (exp xo))" in exI)
+    apply (rule_tac x="nat \<lceil>exp xo\<rceil>" in exI)
     apply clarify
     apply (drule_tac x="ln n" in spec)
     apply (auto simp: exp_less_mono nat_ceiling_le_eq not_le)

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -1259,14 +1259,14 @@
 
 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
 proof -
-  have "\<bar>x \<bullet> b\<bar> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
+  have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
     if [simp]: "b \<in> Basis" for x b :: 'a
   proof -
-    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int (ceiling \<bar>x \<bullet> b\<bar>)"
+    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
       by (rule le_of_int_ceiling)
-    also have "\<dots> \<le> real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
+    also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
       by (auto intro!: ceiling_mono)
-    also have "\<dots> < real_of_int (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
+    also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
       by simp
     finally show ?thesis .
   qed
@@ -4612,9 +4612,9 @@
   assumes "0 < e"
   obtains n :: nat where "1 / (Suc n) < e"
 proof atomize_elim
-  have "1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
+  have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
     by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
-  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
+  also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
     by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
   also have "\<dots> = e" by simp
   finally show  "\<exists>n. 1 / real (Suc n) < e" ..

--- a/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -2494,7 +2494,7 @@
   from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
     by (auto split: split_indicator intro!: monoI)
   { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
-      by (rule eventually_sequentiallyI[of "nat(ceiling x)"])
+      by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
          (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
   from filterlim_cong[OF refl refl this]
   have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"

--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -220,21 +220,22 @@
   shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
              (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
 proof -
-  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))"
+  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>"
   { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
     proof (split split_if, intro conjI impI)
       assume "\<not> real j \<le> u x"
-      then have "nat(floor (real_of_ereal (u x) * 2 ^ j)) \<le> nat(floor (j * 2 ^ j))"
+      then have "nat \<lfloor>real_of_ereal (u x) * 2 ^ j\<rfloor> \<le> nat \<lfloor>j * 2 ^ j\<rfloor>"
          by (cases "u x") (auto intro!: nat_mono floor_mono)
-      moreover have "real (nat(floor (j * 2 ^ j))) \<le> j * 2^j"
+      moreover have "real (nat \<lfloor>j * 2 ^ j\<rfloor>) \<le> j * 2^j"
         by linarith
-      ultimately show "nat(floor (real_of_ereal (u x) * 2 ^ j)) \<le> j * 2 ^ j"
+      ultimately show "nat \<lfloor>real_of_ereal (u x) * 2 ^ j\<rfloor> \<le> j * 2 ^ j"
         unfolding of_nat_le_iff by auto
     qed auto }
   note f_upper = this
 
   have real_f:
-    "\<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))))"
+    "\<And>i x. real (f x i) =
+      (if real i \<le> u x then i * 2 ^ i else real (nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor>))"
     unfolding f_def by auto
 
   let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
@@ -259,17 +260,17 @@
       have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
       proof ((split split_if)+, intro conjI impI)
         assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
-        then show "i * 2 ^ i * 2 \<le> nat(floor (real_of_ereal (u x) * 2 ^ Suc i))"
+        then show "i * 2 ^ i * 2 \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>"
           by (cases "u x") (auto intro!: le_nat_floor)
       next
         assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"
-        then show "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 \<le> Suc i * 2 ^ Suc i"
+        then show "nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor> * 2 \<le> Suc i * 2 ^ Suc i"
           by (cases "u x") auto
       next
         assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
-        have "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 = nat(floor (real_of_ereal (u x) * 2 ^ i)) * nat(floor(2::real))"
+        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>"
           by simp
-        also have "\<dots> \<le> nat(floor (real_of_ereal (u x) * 2 ^ i * 2))"
+        also have "\<dots> \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ i * 2\<rfloor>"
         proof cases
           assume "0 \<le> u x" then show ?thesis
             by (intro le_mult_nat_floor)
@@ -277,9 +278,9 @@
           assume "\<not> 0 \<le> u x" then show ?thesis
             by (cases "u x") (auto simp: nat_floor_neg mult_nonpos_nonneg)
         qed
-        also have "\<dots> = nat(floor (real_of_ereal (u x) * 2 ^ Suc i))"
+        also have "\<dots> = nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>"
           by (simp add: ac_simps)
-        finally show "nat(floor (real_of_ereal (u x) * 2 ^ i)) * 2 \<le> nat(floor (real_of_ereal (u x) * 2 ^ Suc i))" .
+        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>" .
       qed simp
       then show "?g i x \<le> ?g (Suc i) x"
         by (auto simp: field_simps)
@@ -308,7 +309,7 @@
           obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
           then have "r * 2^max N m < p * 2^max N m - 1" by simp
           moreover
-          have "real (nat(floor (p * 2 ^ max N m))) \<le> r * 2 ^ max N m"
+          have "real (nat \<lfloor>p * 2 ^ max N m\<rfloor>) \<le> r * 2 ^ max N m"
             using *[of "max N m"] m unfolding real_f using ux
             by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
           then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -393,23 +393,19 @@
 
 subsubsection {* floor and ceiling functions *}
 
-lemma
-  "floor x + floor y = floor (x + y :: rat)"
+lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>"
 quickcheck[expect = counterexample]
 oops
 
-lemma
-  "floor x + floor y = floor (x + y :: real)"
+lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>"
 quickcheck[expect = counterexample]
 oops
 
-lemma
-  "ceiling x + ceiling y = ceiling (x + y :: rat)"
+lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>"
 quickcheck[expect = counterexample]
 oops
 
-lemma
-  "ceiling x + ceiling y = ceiling (x + y :: real)"
+lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>"
 quickcheck[expect = counterexample]
 oops
 

--- a/src/HOL/Rat.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Rat.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -599,17 +599,18 @@
 begin
 
 definition [code del]:
-  "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+  "\<lfloor>x::rat\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
 
-instance proof
+instance
+proof
   fix x :: rat
-  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
     unfolding floor_rat_def using floor_exists1 by (rule theI')
 qed
 
 end
 
-lemma floor_Fract: "floor (Fract a b) = a div b"
+lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b"
   by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
 
 
@@ -1017,8 +1018,8 @@
 qed
 
 lemma rat_floor_code [code]:
-  "floor p = (let (a, b) = quotient_of p in a div b)"
-by (cases p) (simp add: quotient_of_Fract floor_Fract)
+  "\<lfloor>p\<rfloor> = (let (a, b) = quotient_of p in a div b)"
+  by (cases p) (simp add: quotient_of_Fract floor_Fract)
 
 instantiation rat :: equal
 begin

--- a/src/HOL/Real.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Real.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -667,7 +667,7 @@
   show "\<exists>z. x \<le> of_int z"
     apply (induct x)
     apply (frule cauchy_imp_bounded, clarify)
-    apply (rule_tac x="ceiling b + 1" in exI)
+    apply (rule_tac x="\<lceil>b\<rceil> + 1" in exI)
     apply (rule less_imp_le)
     apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
     apply (rule_tac x=1 in exI, simp add: algebra_simps)
@@ -682,11 +682,12 @@
 begin
 
 definition [code del]:
-  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+  "\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
 
-instance proof
+instance
+proof
   fix x :: real
-  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
     unfolding floor_real_def using floor_exists1 by (rule theI')
 qed
 
@@ -777,22 +778,22 @@
   def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
   obtain a where a: "\<not> P a"
   proof
-    have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
+    have "of_int \<lfloor>x - 1\<rfloor> \<le> x - 1" by (rule of_int_floor_le)
     also have "x - 1 < x" by simp
-    finally have "of_int (floor (x - 1)) < x" .
-    hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
-    then show "\<not> P (of_int (floor (x - 1)))"
+    finally have "of_int \<lfloor>x - 1\<rfloor> < x" .
+    hence "\<not> x \<le> of_int \<lfloor>x - 1\<rfloor>" by (simp only: not_le)
+    then show "\<not> P (of_int \<lfloor>x - 1\<rfloor>)"
       unfolding P_def of_rat_of_int_eq using x by blast
   qed
   obtain b where b: "P b"
   proof
-    show "P (of_int (ceiling z))"
+    show "P (of_int \<lceil>z\<rceil>)"
     unfolding P_def of_rat_of_int_eq
     proof
       fix y assume "y \<in> S"
       hence "y \<le> z" using z by simp
-      also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
-      finally show "y \<le> of_int (ceiling z)" .
+      also have "z \<le> of_int \<lceil>z\<rceil>" by (rule le_of_int_ceiling)
+      finally show "y \<le> of_int \<lceil>z\<rceil>" .
     qed
   qed
 
@@ -1245,7 +1246,7 @@
   from \<open>x<y\<close> have "0 < y-x" by simp
   with reals_Archimedean obtain q::nat
     where q: "inverse (real q) < y-x" and "0 < q" by blast
-  def p \<equiv> "ceiling (y * real q) - 1"
+  def p \<equiv> "\<lceil>y * real q\<rceil> - 1"
   def r \<equiv> "of_int p / real q"
   from q have "x < y - inverse (real q)" by simp
   also have "y - inverse (real q) \<le> r"
@@ -1445,40 +1446,40 @@
 declare of_int_floor_le [simp] (* FIXME*)
 
 lemma of_int_floor_cancel [simp]:
-    "(of_int (floor x) = x) = (\<exists>n::int. x = of_int n)"
+    "(of_int \<lfloor>x\<rfloor> = x) = (\<exists>n::int. x = of_int n)"
   by (metis floor_of_int)
 
-lemma floor_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> floor x = n"
+lemma floor_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
   by linarith
 
-lemma floor_eq2: "[| real_of_int n \<le> x; x < real_of_int n + 1 |] ==> floor x = n"
+lemma floor_eq2: "[| real_of_int n \<le> x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
   by linarith
 
-lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
+lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
   by linarith
 
-lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
+lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
   by linarith
 
-lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int(floor r)"
+lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int \<lfloor>r\<rfloor>"
   by linarith
 
-lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int(floor r)"
+lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \<lfloor>r\<rfloor>"
   by linarith
 
-lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real_of_int(floor r) + 1"
+lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real_of_int \<lfloor>r\<rfloor> + 1"
   by linarith
 
-lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int(floor r) + 1"
+lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \<lfloor>r\<rfloor> + 1"
   by linarith
 
-lemma floor_eq_iff: "floor x = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
-by (simp add: floor_unique_iff)
+lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
+  by (simp add: floor_unique_iff)
 
-lemma floor_add2[simp]: "floor (of_int a + x) = a + floor x"
+lemma floor_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
   by (simp add: add.commute)
 
-lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> floor (a / real_of_int b) = floor a div b"
+lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> \<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
 proof cases
   assume "0 < b"
   { fix i j :: int assume "real_of_int i \<le> a" "a < 1 + real_of_int i"
@@ -1509,20 +1510,19 @@
 lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
   by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
 
-lemma of_int_ceiling_cancel [simp]:
-     "(of_int (ceiling x) = x) = (\<exists>n::int. x = of_int n)"
+lemma of_int_ceiling_cancel [simp]: "(of_int \<lceil>x\<rceil> = x) = (\<exists>n::int. x = of_int n)"
   using ceiling_of_int by metis
 
-lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> ceiling x = n + 1"
+lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> \<lceil>x\<rceil> = n + 1"
   by (simp add: ceiling_unique)
 
-lemma of_int_ceiling_diff_one_le [simp]: "of_int (ceiling r) - 1 \<le> r"
+lemma of_int_ceiling_diff_one_le [simp]: "of_int \<lceil>r\<rceil> - 1 \<le> r"
   by linarith
 
-lemma of_int_ceiling_le_add_one [simp]: "of_int (ceiling r) \<le> r + 1"
+lemma of_int_ceiling_le_add_one [simp]: "of_int \<lceil>r\<rceil> \<le> r + 1"
   by linarith
 
-lemma ceiling_le: "x <= of_int a ==> ceiling x <= a"
+lemma ceiling_le: "x <= of_int a ==> \<lceil>x\<rceil> <= a"
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_divide_eq_div: "\<lceil>of_int a / of_int b\<rceil> = - (- a div b)"
@@ -1539,28 +1539,27 @@
 text\<open>The following lemmas are remnants of the erstwhile functions natfloor
 and natceiling.\<close>
 
-lemma nat_floor_neg: "(x::real) <= 0 ==> nat(floor x) = 0"
+lemma nat_floor_neg: "(x::real) <= 0 ==> nat \<lfloor>x\<rfloor> = 0"
   by linarith
 
-lemma le_nat_floor: "real x <= a ==> x <= nat(floor a)"
+lemma le_nat_floor: "real x <= a ==> x <= nat \<lfloor>a\<rfloor>"
   by linarith
 
-lemma le_mult_nat_floor:
-  shows "nat(floor a) * nat(floor b) \<le> nat(floor (a * b))"
+lemma le_mult_nat_floor: "nat \<lfloor>a\<rfloor> * nat \<lfloor>b\<rfloor> \<le> nat \<lfloor>a * b\<rfloor>"
   by (cases "0 <= a & 0 <= b")
      (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)
 
-lemma nat_ceiling_le_eq [simp]: "(nat(ceiling x) <= a) = (x <= real a)"
+lemma nat_ceiling_le_eq [simp]: "(nat \<lceil>x\<rceil> <= a) = (x <= real a)"
   by linarith
 
-lemma real_nat_ceiling_ge: "x <= real(nat(ceiling x))"
+lemma real_nat_ceiling_ge: "x <= real (nat \<lceil>x\<rceil>)"
   by linarith
 
 lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
-  by (auto intro!: bexI[of _ "of_nat (nat(ceiling x))"]) linarith
+  by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith
 
 lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
-  apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
+  apply (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"])
   apply (rule less_le_trans[OF _ of_int_floor_le])
   apply simp
   done
@@ -1568,10 +1567,10 @@
 subsection \<open>Exponentiation with floor\<close>
 
 lemma floor_power:
-  assumes "x = of_int (floor x)"
-  shows "floor (x ^ n) = floor x ^ n"
+  assumes "x = of_int \<lfloor>x\<rfloor>"
+  shows "\<lfloor>x ^ n\<rfloor> = \<lfloor>x\<rfloor> ^ n"
 proof -
-  have "x ^ n = of_int (floor x ^ n)"
+  have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)"
     using assms by (induct n arbitrary: x) simp_all
   then show ?thesis by (metis floor_of_int) 
 qed
@@ -1681,7 +1680,7 @@
 lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
   by (simp add: of_rat_divide)
 
-lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
+lemma real_floor_code [code]: "\<lfloor>Ratreal x\<rfloor> = \<lfloor>x\<rfloor>"
   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)
 
 

--- a/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -1701,8 +1701,10 @@
 lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   unfolding filterlim_at_top
   apply (intro allI)
-  apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
-  by linarith
+  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI)
+  apply linarith
+  done
+
 
 subsubsection \<open>Limits of Sequences\<close>
 

--- a/src/HOL/TPTP/THF_Arith.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/TPTP/THF_Arith.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -36,12 +36,12 @@
 
 overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
 begin
-  definition "rat_to_int (q::rat) = floor q"
+  definition "rat_to_int (q::rat) = \<lfloor>q\<rfloor>"
 end
 
 overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
 begin
-  definition "real_to_int (x::real) = floor x"
+  definition "real_to_int (x::real) = \<lfloor>x\<rfloor>"
 end
 
 overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"

--- a/src/HOL/Transcendental.thy	Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Transcendental.thy	Sun Dec 27 21:46:36 2015 +0100
@@ -2378,7 +2378,7 @@
   fixes i::real
   shows "b powr i =
     (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
-    else if floor i = i then (if 0 \<le> i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
+    else if \<lfloor>i\<rfloor> = i then (if 0 \<le> i then b ^ nat \<lfloor>i\<rfloor> else 1 / b ^ nat \<lfloor>- i\<rfloor>)
     else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
   by (auto simp: powr_int)
 
@@ -3568,7 +3568,7 @@
     using floor_correct [of "x/pi"]
     by (simp add: add.commute divide_less_eq)
   obtain n where "real n * pi \<le> x" "x < real (Suc n) * pi"
-    apply (rule that [of "nat (floor (x/pi))"] )
+    apply (rule that [of "nat \<lfloor>x/pi\<rfloor>"])
     using assms
     apply (simp_all add: xle)
     apply (metis floor_less_iff less_irrefl mult_imp_div_pos_less not_le pi_gt_zero)