1(* Title: HOL/Archimedean_Field.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Archimedean Fields, Floor and Ceiling Functions\<close> 6 7theory Archimedean_Field 8imports Main 9begin 10 11lemma cInf_abs_ge: 12 fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set" 13 assumes "S \<noteq> {}" 14 and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a" 15 shows "\<bar>Inf S\<bar> \<le> a" 16proof - 17 have "Sup (uminus ` S) = - (Inf S)" 18 proof (rule antisym) 19 show "- (Inf S) \<le> Sup (uminus ` S)" 20 apply (subst minus_le_iff) 21 apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>]) 22 apply (subst minus_le_iff) 23 apply (rule cSup_upper) 24 apply force 25 using bdd 26 apply (force simp: abs_le_iff bdd_above_def) 27 done 28 next 29 show "Sup (uminus ` S) \<le> - Inf S" 30 apply (rule cSup_least) 31 using \<open>S \<noteq> {}\<close> 32 apply force 33 apply clarsimp 34 apply (rule cInf_lower) 35 apply assumption 36 using bdd 37 apply (simp add: bdd_below_def) 38 apply (rule_tac x = "- a" in exI) 39 apply force 40 done 41 qed 42 with cSup_abs_le [of "uminus ` S"] assms show ?thesis 43 by fastforce 44qed 45 46lemma cSup_asclose: 47 fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set" 48 assumes S: "S \<noteq> {}" 49 and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" 50 shows "\<bar>Sup S - l\<bar> \<le> e" 51proof - 52 have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a 53 by arith 54 have "bdd_above S" 55 using b by (auto intro!: bdd_aboveI[of _ "l + e"]) 56 with S b show ?thesis 57 unfolding * by (auto intro!: cSup_upper2 cSup_least) 58qed 59 60lemma cInf_asclose: 61 fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set" 62 assumes S: "S \<noteq> {}" 63 and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" 64 shows "\<bar>Inf S - l\<bar> \<le> e" 65proof - 66 have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a 67 by arith 68 have "bdd_below S" 69 using b by (auto intro!: bdd_belowI[of _ "l - e"]) 70 with S b show ?thesis 71 unfolding * by (auto intro!: cInf_lower2 cInf_greatest) 72qed 73 74 75subsection \<open>Class of Archimedean fields\<close> 76 77text \<open>Archimedean fields have no infinite elements.\<close> 78 79class archimedean_field = linordered_field + 80 assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" 81 82lemma ex_less_of_int: "\<exists>z. x < of_int z" 83 for x :: "'a::archimedean_field" 84proof - 85 from ex_le_of_int obtain z where "x \<le> of_int z" .. 86 then have "x < of_int (z + 1)" by simp 87 then show ?thesis .. 88qed 89 90lemma ex_of_int_less: "\<exists>z. of_int z < x" 91 for x :: "'a::archimedean_field" 92proof - 93 from ex_less_of_int obtain z where "- x < of_int z" .. 94 then have "of_int (- z) < x" by simp 95 then show ?thesis .. 96qed 97 98lemma reals_Archimedean2: "\<exists>n. x < of_nat n" 99 for x :: "'a::archimedean_field" 100proof - 101 obtain z where "x < of_int z" 102 using ex_less_of_int .. 103 also have "\<dots> \<le> of_int (int (nat z))" 104 by simp 105 also have "\<dots> = of_nat (nat z)" 106 by (simp only: of_int_of_nat_eq) 107 finally show ?thesis .. 108qed 109 110lemma real_arch_simple: "\<exists>n. x \<le> of_nat n" 111 for x :: "'a::archimedean_field" 112proof - 113 obtain n where "x < of_nat n" 114 using reals_Archimedean2 .. 115 then have "x \<le> of_nat n" 116 by simp 117 then show ?thesis .. 118qed 119 120text \<open>Archimedean fields have no infinitesimal elements.\<close> 121 122lemma reals_Archimedean: 123 fixes x :: "'a::archimedean_field" 124 assumes "0 < x" 125 shows "\<exists>n. inverse (of_nat (Suc n)) < x" 126proof - 127 from \<open>0 < x\<close> have "0 < inverse x" 128 by (rule positive_imp_inverse_positive) 129 obtain n where "inverse x < of_nat n" 130 using reals_Archimedean2 .. 131 then obtain m where "inverse x < of_nat (Suc m)" 132 using \<open>0 < inverse x\<close> by (cases n) (simp_all del: of_nat_Suc) 133 then have "inverse (of_nat (Suc m)) < inverse (inverse x)" 134 using \<open>0 < inverse x\<close> by (rule less_imp_inverse_less) 135 then have "inverse (of_nat (Suc m)) < x" 136 using \<open>0 < x\<close> by (simp add: nonzero_inverse_inverse_eq) 137 then show ?thesis .. 138qed 139 140lemma ex_inverse_of_nat_less: 141 fixes x :: "'a::archimedean_field" 142 assumes "0 < x" 143 shows "\<exists>n>0. inverse (of_nat n) < x" 144 using reals_Archimedean [OF \<open>0 < x\<close>] by auto 145 146lemma ex_less_of_nat_mult: 147 fixes x :: "'a::archimedean_field" 148 assumes "0 < x" 149 shows "\<exists>n. y < of_nat n * x" 150proof - 151 obtain n where "y / x < of_nat n" 152 using reals_Archimedean2 .. 153 with \<open>0 < x\<close> have "y < of_nat n * x" 154 by (simp add: pos_divide_less_eq) 155 then show ?thesis .. 156qed 157 158 159subsection \<open>Existence and uniqueness of floor function\<close> 160 161lemma exists_least_lemma: 162 assumes "\<not> P 0" and "\<exists>n. P n" 163 shows "\<exists>n. \<not> P n \<and> P (Suc n)" 164proof - 165 from \<open>\<exists>n. P n\<close> have "P (Least P)" 166 by (rule LeastI_ex) 167 with \<open>\<not> P 0\<close> obtain n where "Least P = Suc n" 168 by (cases "Least P") auto 169 then have "n < Least P" 170 by simp 171 then have "\<not> P n" 172 by (rule not_less_Least) 173 then have "\<not> P n \<and> P (Suc n)" 174 using \<open>P (Least P)\<close> \<open>Least P = Suc n\<close> by simp 175 then show ?thesis .. 176qed 177 178lemma floor_exists: 179 fixes x :: "'a::archimedean_field" 180 shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" 181proof (cases "0 \<le> x") 182 case True 183 then have "\<not> x < of_nat 0" 184 by simp 185 then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)" 186 using reals_Archimedean2 by (rule exists_least_lemma) 187 then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" .. 188 then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" 189 by simp 190 then show ?thesis .. 191next 192 case False 193 then have "\<not> - x \<le> of_nat 0" 194 by simp 195 then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" 196 using real_arch_simple by (rule exists_least_lemma) 197 then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" .. 198 then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" 199 by simp 200 then show ?thesis .. 201qed 202 203lemma floor_exists1: "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)" 204 for x :: "'a::archimedean_field" 205proof (rule ex_ex1I) 206 show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" 207 by (rule floor_exists) 208next 209 fix y z 210 assume "of_int y \<le> x \<and> x < of_int (y + 1)" 211 and "of_int z \<le> x \<and> x < of_int (z + 1)" 212 with le_less_trans [of "of_int y" "x" "of_int (z + 1)"] 213 le_less_trans [of "of_int z" "x" "of_int (y + 1)"] show "y = z" 214 by (simp del: of_int_add) 215qed 216 217 218subsection \<open>Floor function\<close> 219 220class floor_ceiling = archimedean_field + 221 fixes floor :: "'a \<Rightarrow> int" ("\<lfloor>_\<rfloor>") 222 assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)" 223 224lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z" 225 using floor_correct [of x] floor_exists1 [of x] by auto 226 227lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1" 228using floor_correct floor_unique by auto 229 230lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x" 231 using floor_correct .. 232 233lemma le_floor_iff: "z \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z \<le> x" 234proof 235 assume "z \<le> \<lfloor>x\<rfloor>" 236 then have "(of_int z :: 'a) \<le> of_int \<lfloor>x\<rfloor>" by simp 237 also have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le) 238 finally show "of_int z \<le> x" . 239next 240 assume "of_int z \<le> x" 241 also have "x < of_int (\<lfloor>x\<rfloor> + 1)" using floor_correct .. 242 finally show "z \<le> \<lfloor>x\<rfloor>" by (simp del: of_int_add) 243qed 244 245lemma floor_less_iff: "\<lfloor>x\<rfloor> < z \<longleftrightarrow> x < of_int z" 246 by (simp add: not_le [symmetric] le_floor_iff) 247 248lemma less_floor_iff: "z < \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z + 1 \<le> x" 249 using le_floor_iff [of "z + 1" x] by auto 250 251lemma floor_le_iff: "\<lfloor>x\<rfloor> \<le> z \<longleftrightarrow> x < of_int z + 1" 252 by (simp add: not_less [symmetric] less_floor_iff) 253 254lemma 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)" 255 by (metis floor_correct floor_unique less_floor_iff not_le order_refl) 256 257lemma floor_mono: 258 assumes "x \<le> y" 259 shows "\<lfloor>x\<rfloor> \<le> \<lfloor>y\<rfloor>" 260proof - 261 have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le) 262 also note \<open>x \<le> y\<close> 263 finally show ?thesis by (simp add: le_floor_iff) 264qed 265 266lemma floor_less_cancel: "\<lfloor>x\<rfloor> < \<lfloor>y\<rfloor> \<Longrightarrow> x < y" 267 by (auto simp add: not_le [symmetric] floor_mono) 268 269lemma floor_of_int [simp]: "\<lfloor>of_int z\<rfloor> = z" 270 by (rule floor_unique) simp_all 271 272lemma floor_of_nat [simp]: "\<lfloor>of_nat n\<rfloor> = int n" 273 using floor_of_int [of "of_nat n"] by simp 274 275lemma le_floor_add: "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>" 276 by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le) 277 278 279text \<open>Floor with numerals.\<close> 280 281lemma floor_zero [simp]: "\<lfloor>0\<rfloor> = 0" 282 using floor_of_int [of 0] by simp 283 284lemma floor_one [simp]: "\<lfloor>1\<rfloor> = 1" 285 using floor_of_int [of 1] by simp 286 287lemma floor_numeral [simp]: "\<lfloor>numeral v\<rfloor> = numeral v" 288 using floor_of_int [of "numeral v"] by simp 289 290lemma floor_neg_numeral [simp]: "\<lfloor>- numeral v\<rfloor> = - numeral v" 291 using floor_of_int [of "- numeral v"] by simp 292 293lemma zero_le_floor [simp]: "0 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 0 \<le> x" 294 by (simp add: le_floor_iff) 295 296lemma one_le_floor [simp]: "1 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x" 297 by (simp add: le_floor_iff) 298 299lemma numeral_le_floor [simp]: "numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v \<le> x" 300 by (simp add: le_floor_iff) 301 302lemma neg_numeral_le_floor [simp]: "- numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v \<le> x" 303 by (simp add: le_floor_iff) 304 305lemma zero_less_floor [simp]: "0 < \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x" 306 by (simp add: less_floor_iff) 307 308lemma one_less_floor [simp]: "1 < \<lfloor>x\<rfloor> \<longleftrightarrow> 2 \<le> x" 309 by (simp add: less_floor_iff) 310 311lemma numeral_less_floor [simp]: "numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v + 1 \<le> x" 312 by (simp add: less_floor_iff) 313 314lemma neg_numeral_less_floor [simp]: "- numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v + 1 \<le> x" 315 by (simp add: less_floor_iff) 316 317lemma floor_le_zero [simp]: "\<lfloor>x\<rfloor> \<le> 0 \<longleftrightarrow> x < 1" 318 by (simp add: floor_le_iff) 319 320lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2" 321 by (simp add: floor_le_iff) 322 323lemma floor_le_numeral [simp]: "\<lfloor>x\<rfloor> \<le> numeral v \<longleftrightarrow> x < numeral v + 1" 324 by (simp add: floor_le_iff) 325 326lemma floor_le_neg_numeral [simp]: "\<lfloor>x\<rfloor> \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1" 327 by (simp add: floor_le_iff) 328 329lemma floor_less_zero [simp]: "\<lfloor>x\<rfloor> < 0 \<longleftrightarrow> x < 0" 330 by (simp add: floor_less_iff) 331 332lemma floor_less_one [simp]: "\<lfloor>x\<rfloor> < 1 \<longleftrightarrow> x < 1" 333 by (simp add: floor_less_iff) 334 335lemma floor_less_numeral [simp]: "\<lfloor>x\<rfloor> < numeral v \<longleftrightarrow> x < numeral v" 336 by (simp add: floor_less_iff) 337 338lemma floor_less_neg_numeral [simp]: "\<lfloor>x\<rfloor> < - numeral v \<longleftrightarrow> x < - numeral v" 339 by (simp add: floor_less_iff) 340 341lemma le_mult_floor_Ints: 342 assumes "0 \<le> a" "a \<in> Ints" 343 shows "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> (of_int\<lfloor>a * b\<rfloor> :: 'a :: linordered_idom)" 344 by (metis Ints_cases assms floor_less_iff floor_of_int linorder_not_less mult_left_mono of_int_floor_le of_int_less_iff of_int_mult) 345 346 347text \<open>Addition and subtraction of integers.\<close> 348 349lemma floor_add_int: "\<lfloor>x\<rfloor> + z = \<lfloor>x + of_int z\<rfloor>" 350 using floor_correct [of x] by (simp add: floor_unique[symmetric]) 351 352lemma int_add_floor: "z + \<lfloor>x\<rfloor> = \<lfloor>of_int z + x\<rfloor>" 353 using floor_correct [of x] by (simp add: floor_unique[symmetric]) 354 355lemma one_add_floor: "\<lfloor>x\<rfloor> + 1 = \<lfloor>x + 1\<rfloor>" 356 using floor_add_int [of x 1] by simp 357 358lemma floor_diff_of_int [simp]: "\<lfloor>x - of_int z\<rfloor> = \<lfloor>x\<rfloor> - z" 359 using floor_add_int [of x "- z"] by (simp add: algebra_simps) 360 361lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z" 362 by (metis floor_diff_of_int [of 0] diff_0 floor_zero) 363 364lemma floor_diff_numeral [simp]: "\<lfloor>x - numeral v\<rfloor> = \<lfloor>x\<rfloor> - numeral v" 365 using floor_diff_of_int [of x "numeral v"] by simp 366 367lemma floor_diff_one [simp]: "\<lfloor>x - 1\<rfloor> = \<lfloor>x\<rfloor> - 1" 368 using floor_diff_of_int [of x 1] by simp 369 370lemma le_mult_floor: 371 assumes "0 \<le> a" and "0 \<le> b" 372 shows "\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor> \<le> \<lfloor>a * b\<rfloor>" 373proof - 374 have "of_int \<lfloor>a\<rfloor> \<le> a" and "of_int \<lfloor>b\<rfloor> \<le> b" 375 by (auto intro: of_int_floor_le) 376 then have "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> a * b" 377 using assms by (auto intro!: mult_mono) 378 also have "a * b < of_int (\<lfloor>a * b\<rfloor> + 1)" 379 using floor_correct[of "a * b"] by auto 380 finally show ?thesis 381 unfolding of_int_less_iff by simp 382qed 383 384lemma floor_divide_of_int_eq: "\<lfloor>of_int k / of_int l\<rfloor> = k div l" 385 for k l :: int 386proof (cases "l = 0") 387 case True 388 then show ?thesis by simp 389next 390 case False 391 have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0" 392 proof (cases "l > 0") 393 case True 394 then show ?thesis 395 by (auto intro: floor_unique) 396 next 397 case False 398 obtain r where "r = - l" 399 by blast 400 then have l: "l = - r" 401 by simp 402 with \<open>l \<noteq> 0\<close> False have "r > 0" 403 by simp 404 with l show ?thesis 405 using pos_mod_bound [of r] 406 by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique) 407 qed 408 have "(of_int k :: 'a) = of_int (k div l * l + k mod l)" 409 by simp 410 also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l" 411 using False by (simp only: of_int_add) (simp add: field_simps) 412 finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l" 413 by simp 414 then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l" 415 using False by (simp only:) (simp add: field_simps) 416 then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>" 417 by simp 418 then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>" 419 by (simp add: ac_simps) 420 then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + k div l" 421 by (simp add: floor_add_int) 422 with * show ?thesis 423 by simp 424qed 425 426lemma floor_divide_of_nat_eq: "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)" 427 for m n :: nat 428proof (cases "n = 0") 429 case True 430 then show ?thesis by simp 431next 432 case False 433 then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0" 434 by (auto intro: floor_unique) 435 have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)" 436 by simp 437 also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n" 438 using False by (simp only: of_nat_add) (simp add: field_simps) 439 finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n" 440 by simp 441 then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n" 442 using False by (simp only:) simp 443 then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>" 444 by simp 445 then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>" 446 by (simp add: ac_simps) 447 moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))" 448 by simp 449 ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = 450 \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)" 451 by (simp only: floor_add_int) 452 with * show ?thesis 453 by simp 454qed 455 456lemma floor_divide_lower: 457 fixes q :: "'a::floor_ceiling" 458 shows "q > 0 \<Longrightarrow> of_int \<lfloor>p / q\<rfloor> * q \<le> p" 459 using of_int_floor_le pos_le_divide_eq by blast 460 461lemma floor_divide_upper: 462 fixes q :: "'a::floor_ceiling" 463 shows "q > 0 \<Longrightarrow> p < (of_int \<lfloor>p / q\<rfloor> + 1) * q" 464 by (meson floor_eq_iff pos_divide_less_eq) 465 466 467subsection \<open>Ceiling function\<close> 468 469definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" ("\<lceil>_\<rceil>") 470 where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>" 471 472lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>" 473 unfolding ceiling_def using floor_correct [of "- x"] 474 by (simp add: le_minus_iff) 475 476lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z" 477 unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp 478 479lemma ceiling_eq_iff: "\<lceil>x\<rceil> = a \<longleftrightarrow> of_int a - 1 < x \<and> x \<le> of_int a" 480using ceiling_correct ceiling_unique by auto 481 482lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>" 483 using ceiling_correct .. 484 485lemma ceiling_le_iff: "\<lceil>x\<rceil> \<le> z \<longleftrightarrow> x \<le> of_int z" 486 unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto 487 488lemma less_ceiling_iff: "z < \<lceil>x\<rceil> \<longleftrightarrow> of_int z < x" 489 by (simp add: not_le [symmetric] ceiling_le_iff) 490 491lemma ceiling_less_iff: "\<lceil>x\<rceil> < z \<longleftrightarrow> x \<le> of_int z - 1" 492 using ceiling_le_iff [of x "z - 1"] by simp 493 494lemma le_ceiling_iff: "z \<le> \<lceil>x\<rceil> \<longleftrightarrow> of_int z - 1 < x" 495 by (simp add: not_less [symmetric] ceiling_less_iff) 496 497lemma ceiling_mono: "x \<ge> y \<Longrightarrow> \<lceil>x\<rceil> \<ge> \<lceil>y\<rceil>" 498 unfolding ceiling_def by (simp add: floor_mono) 499 500lemma ceiling_less_cancel: "\<lceil>x\<rceil> < \<lceil>y\<rceil> \<Longrightarrow> x < y" 501 by (auto simp add: not_le [symmetric] ceiling_mono) 502 503lemma ceiling_of_int [simp]: "\<lceil>of_int z\<rceil> = z" 504 by (rule ceiling_unique) simp_all 505 506lemma ceiling_of_nat [simp]: "\<lceil>of_nat n\<rceil> = int n" 507 using ceiling_of_int [of "of_nat n"] by simp 508 509lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>" 510 by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling) 511 512lemma mult_ceiling_le: 513 assumes "0 \<le> a" and "0 \<le> b" 514 shows "\<lceil>a * b\<rceil> \<le> \<lceil>a\<rceil> * \<lceil>b\<rceil>" 515 by (metis assms ceiling_le_iff ceiling_mono le_of_int_ceiling mult_mono of_int_mult) 516 517lemma mult_ceiling_le_Ints: 518 assumes "0 \<le> a" "a \<in> Ints" 519 shows "(of_int \<lceil>a * b\<rceil> :: 'a :: linordered_idom) \<le> of_int(\<lceil>a\<rceil> * \<lceil>b\<rceil>)" 520 by (metis Ints_cases assms ceiling_le_iff ceiling_of_int le_of_int_ceiling mult_left_mono of_int_le_iff of_int_mult) 521 522lemma finite_int_segment: 523 fixes a :: "'a::floor_ceiling" 524 shows "finite {x \<in> \<int>. a \<le> x \<and> x \<le> b}" 525proof - 526 have "finite {ceiling a..floor b}" 527 by simp 528 moreover have "{x \<in> \<int>. a \<le> x \<and> x \<le> b} = of_int ` {ceiling a..floor b}" 529 by (auto simp: le_floor_iff ceiling_le_iff elim!: Ints_cases) 530 ultimately show ?thesis 531 by simp 532qed 533 534corollary finite_abs_int_segment: 535 fixes a :: "'a::floor_ceiling" 536 shows "finite {k \<in> \<int>. \<bar>k\<bar> \<le> a}" 537 using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff) 538 539 540subsubsection \<open>Ceiling with numerals.\<close> 541 542lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0" 543 using ceiling_of_int [of 0] by simp 544 545lemma ceiling_one [simp]: "\<lceil>1\<rceil> = 1" 546 using ceiling_of_int [of 1] by simp 547 548lemma ceiling_numeral [simp]: "\<lceil>numeral v\<rceil> = numeral v" 549 using ceiling_of_int [of "numeral v"] by simp 550 551lemma ceiling_neg_numeral [simp]: "\<lceil>- numeral v\<rceil> = - numeral v" 552 using ceiling_of_int [of "- numeral v"] by simp 553 554lemma ceiling_le_zero [simp]: "\<lceil>x\<rceil> \<le> 0 \<longleftrightarrow> x \<le> 0" 555 by (simp add: ceiling_le_iff) 556 557lemma ceiling_le_one [simp]: "\<lceil>x\<rceil> \<le> 1 \<longleftrightarrow> x \<le> 1" 558 by (simp add: ceiling_le_iff) 559 560lemma ceiling_le_numeral [simp]: "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v" 561 by (simp add: ceiling_le_iff) 562 563lemma ceiling_le_neg_numeral [simp]: "\<lceil>x\<rceil> \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v" 564 by (simp add: ceiling_le_iff) 565 566lemma ceiling_less_zero [simp]: "\<lceil>x\<rceil> < 0 \<longleftrightarrow> x \<le> -1" 567 by (simp add: ceiling_less_iff) 568 569lemma ceiling_less_one [simp]: "\<lceil>x\<rceil> < 1 \<longleftrightarrow> x \<le> 0" 570 by (simp add: ceiling_less_iff) 571 572lemma ceiling_less_numeral [simp]: "\<lceil>x\<rceil> < numeral v \<longleftrightarrow> x \<le> numeral v - 1" 573 by (simp add: ceiling_less_iff) 574 575lemma ceiling_less_neg_numeral [simp]: "\<lceil>x\<rceil> < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1" 576 by (simp add: ceiling_less_iff) 577 578lemma zero_le_ceiling [simp]: "0 \<le> \<lceil>x\<rceil> \<longleftrightarrow> -1 < x" 579 by (simp add: le_ceiling_iff) 580 581lemma one_le_ceiling [simp]: "1 \<le> \<lceil>x\<rceil> \<longleftrightarrow> 0 < x" 582 by (simp add: le_ceiling_iff) 583 584lemma numeral_le_ceiling [simp]: "numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> numeral v - 1 < x" 585 by (simp add: le_ceiling_iff) 586 587lemma neg_numeral_le_ceiling [simp]: "- numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> - numeral v - 1 < x" 588 by (simp add: le_ceiling_iff) 589 590lemma zero_less_ceiling [simp]: "0 < \<lceil>x\<rceil> \<longleftrightarrow> 0 < x" 591 by (simp add: less_ceiling_iff) 592 593lemma one_less_ceiling [simp]: "1 < \<lceil>x\<rceil> \<longleftrightarrow> 1 < x" 594 by (simp add: less_ceiling_iff) 595 596lemma numeral_less_ceiling [simp]: "numeral v < \<lceil>x\<rceil> \<longleftrightarrow> numeral v < x" 597 by (simp add: less_ceiling_iff) 598 599lemma neg_numeral_less_ceiling [simp]: "- numeral v < \<lceil>x\<rceil> \<longleftrightarrow> - numeral v < x" 600 by (simp add: less_ceiling_iff) 601 602lemma ceiling_altdef: "\<lceil>x\<rceil> = (if x = of_int \<lfloor>x\<rfloor> then \<lfloor>x\<rfloor> else \<lfloor>x\<rfloor> + 1)" 603 by (intro ceiling_unique; simp, linarith?) 604 605lemma floor_le_ceiling [simp]: "\<lfloor>x\<rfloor> \<le> \<lceil>x\<rceil>" 606 by (simp add: ceiling_altdef) 607 608 609subsubsection \<open>Addition and subtraction of integers.\<close> 610 611lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z" 612 using ceiling_correct [of x] by (simp add: ceiling_def) 613 614lemma ceiling_add_numeral [simp]: "\<lceil>x + numeral v\<rceil> = \<lceil>x\<rceil> + numeral v" 615 using ceiling_add_of_int [of x "numeral v"] by simp 616 617lemma ceiling_add_one [simp]: "\<lceil>x + 1\<rceil> = \<lceil>x\<rceil> + 1" 618 using ceiling_add_of_int [of x 1] by simp 619 620lemma ceiling_diff_of_int [simp]: "\<lceil>x - of_int z\<rceil> = \<lceil>x\<rceil> - z" 621 using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps) 622 623lemma ceiling_diff_numeral [simp]: "\<lceil>x - numeral v\<rceil> = \<lceil>x\<rceil> - numeral v" 624 using ceiling_diff_of_int [of x "numeral v"] by simp 625 626lemma ceiling_diff_one [simp]: "\<lceil>x - 1\<rceil> = \<lceil>x\<rceil> - 1" 627 using ceiling_diff_of_int [of x 1] by simp 628 629lemma 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)" 630 by (auto simp add: ceiling_unique ceiling_correct) 631 632lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1" 633proof - 634 have "of_int \<lceil>x\<rceil> - 1 < x" 635 using ceiling_correct[of x] by simp 636 also have "x < of_int \<lfloor>x\<rfloor> + 1" 637 using floor_correct[of x] by simp_all 638 finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)" 639 by simp 640 then show ?thesis 641 unfolding of_int_less_iff by simp 642qed 643 644lemma nat_approx_posE: 645 fixes e:: "'a::{archimedean_field,floor_ceiling}" 646 assumes "0 < e" 647 obtains n :: nat where "1 / of_nat(Suc n) < e" 648proof 649 have "(1::'a) / of_nat (Suc (nat \<lceil>1/e\<rceil>)) < 1 / of_int (\<lceil>1/e\<rceil>)" 650 proof (rule divide_strict_left_mono) 651 show "(of_int \<lceil>1 / e\<rceil>::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>))" 652 using assms by (simp add: field_simps) 653 show "(0::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>)) * of_int \<lceil>1 / e\<rceil>" 654 using assms by (auto simp: zero_less_mult_iff pos_add_strict) 655 qed auto 656 also have "1 / of_int (\<lceil>1/e\<rceil>) \<le> 1 / (1/e)" 657 by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct) 658 also have "\<dots> = e" by simp 659 finally show "1 / of_nat (Suc (nat \<lceil>1 / e\<rceil>)) < e" 660 by metis 661qed 662 663lemma ceiling_divide_upper: 664 fixes q :: "'a::floor_ceiling" 665 shows "q > 0 \<Longrightarrow> p \<le> of_int (ceiling (p / q)) * q" 666 by (meson divide_le_eq le_of_int_ceiling) 667 668lemma ceiling_divide_lower: 669 fixes q :: "'a::floor_ceiling" 670 shows "q > 0 \<Longrightarrow> (of_int \<lceil>p / q\<rceil> - 1) * q < p" 671 by (meson ceiling_eq_iff pos_less_divide_eq) 672 673subsection \<open>Negation\<close> 674 675lemma floor_minus: "\<lfloor>- x\<rfloor> = - \<lceil>x\<rceil>" 676 unfolding ceiling_def by simp 677 678lemma ceiling_minus: "\<lceil>- x\<rceil> = - \<lfloor>x\<rfloor>" 679 unfolding ceiling_def by simp 680 681subsection \<open>Natural numbers\<close> 682 683lemma of_nat_floor: "r\<ge>0 \<Longrightarrow> of_nat (nat \<lfloor>r\<rfloor>) \<le> r" 684 by simp 685 686lemma of_nat_ceiling: "of_nat (nat \<lceil>r\<rceil>) \<ge> r" 687 by (cases "r\<ge>0") auto 688 689 690subsection \<open>Frac Function\<close> 691 692definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" 693 where "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>" 694 695lemma frac_lt_1: "frac x < 1" 696 by (simp add: frac_def) linarith 697 698lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>" 699 by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int ) 700 701lemma frac_ge_0 [simp]: "frac x \<ge> 0" 702 unfolding frac_def by linarith 703 704lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>" 705 by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl) 706 707lemma frac_of_int [simp]: "frac (of_int z) = 0" 708 by (simp add: frac_def) 709 710lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)" 711proof - 712 have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" 713 by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add) 714 moreover 715 have "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)" 716 apply (simp add: floor_eq_iff) 717 apply (auto simp add: algebra_simps) 718 apply linarith 719 done 720 ultimately show ?thesis by (auto simp add: frac_def algebra_simps) 721qed 722 723lemma floor_add2[simp]: "x \<in> \<int> \<or> y \<in> \<int> \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" 724by (metis add.commute add.left_neutral frac_lt_1 floor_add frac_eq_0_iff) 725 726lemma frac_add: 727 "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)" 728 by (simp add: frac_def floor_add) 729 730lemma frac_unique_iff: "frac x = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1" 731 for x :: "'a::floor_ceiling" 732 apply (auto simp: Ints_def frac_def algebra_simps floor_unique) 733 apply linarith+ 734 done 735 736lemma frac_eq: "frac x = x \<longleftrightarrow> 0 \<le> x \<and> x < 1" 737 by (simp add: frac_unique_iff) 738 739lemma frac_neg: "frac (- x) = (if x \<in> \<int> then 0 else 1 - frac x)" 740 for x :: "'a::floor_ceiling" 741 apply (auto simp add: frac_unique_iff) 742 apply (simp add: frac_def) 743 apply (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq) 744 done 745 746 747subsection \<open>Rounding to the nearest integer\<close> 748 749definition round :: "'a::floor_ceiling \<Rightarrow> int" 750 where "round x = \<lfloor>x + 1/2\<rfloor>" 751 752lemma of_int_round_ge: "of_int (round x) \<ge> x - 1/2" 753 and of_int_round_le: "of_int (round x) \<le> x + 1/2" 754 and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2" 755 and of_int_round_gt: "of_int (round x) > x - 1/2" 756proof - 757 from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" 758 by (simp add: round_def) 759 from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" 760 by simp 761 then show "of_int (round x) \<ge> x - 1/2" 762 by simp 763 from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" 764 by (simp add: round_def) 765 with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" 766 by linarith 767qed 768 769lemma round_of_int [simp]: "round (of_int n) = n" 770 unfolding round_def by (subst floor_eq_iff) force 771 772lemma round_0 [simp]: "round 0 = 0" 773 using round_of_int[of 0] by simp 774 775lemma round_1 [simp]: "round 1 = 1" 776 using round_of_int[of 1] by simp 777 778lemma round_numeral [simp]: "round (numeral n) = numeral n" 779 using round_of_int[of "numeral n"] by simp 780 781lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n" 782 using round_of_int[of "-numeral n"] by simp 783 784lemma round_of_nat [simp]: "round (of_nat n) = of_nat n" 785 using round_of_int[of "int n"] by simp 786 787lemma round_mono: "x \<le> y \<Longrightarrow> round x \<le> round y" 788 unfolding round_def by (intro floor_mono) simp 789 790lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y" 791 unfolding round_def 792proof (rule floor_unique) 793 assume "x - 1 / 2 < of_int y" 794 from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" 795 by simp 796qed 797 798lemma round_unique': "\<bar>x - of_int n\<bar> < 1/2 \<Longrightarrow> round x = n" 799 by (subst (asm) abs_less_iff, rule round_unique) (simp_all add: field_simps) 800 801lemma round_altdef: "round x = (if frac x \<ge> 1/2 then \<lceil>x\<rceil> else \<lfloor>x\<rfloor>)" 802 by (cases "frac x \<ge> 1/2") 803 (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef; linarith)+)[2])+ 804 805lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x" 806 unfolding round_def by (intro floor_mono) simp 807 808lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" 809 unfolding round_altdef by simp 810 811lemma round_diff_minimal: "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>" 812 for z :: "'a::floor_ceiling" 813proof (cases "of_int m \<ge> z") 814 case True 815 then have "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>" 816 unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith 817 also have "of_int \<lceil>z\<rceil> - z \<ge> 0" 818 by linarith 819 with True have "\<bar>of_int \<lceil>z\<rceil> - z\<bar> \<le> \<bar>z - of_int m\<bar>" 820 by (simp add: ceiling_le_iff) 821 finally show ?thesis . 822next 823 case False 824 then have "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lfloor>z\<rfloor> - z\<bar>" 825 unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith 826 also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" 827 by linarith 828 with False have "\<bar>of_int \<lfloor>z\<rfloor> - z\<bar> \<le> \<bar>z - of_int m\<bar>" 829 by (simp add: le_floor_iff) 830 finally show ?thesis . 831qed 832 833end 834