author | bulwahn |
Thu, 07 Jul 2011 23:33:14 +0200 | |
changeset 44566 | 47b0be18ccbe |
parent 42830 | b460124855b8 |
child 44585 | 6b2bdc57155b |
permissions | -rw-r--r-- |
wenzelm@42830 | 1 |
(* Title: HOL/Archimedean_Field.thy |
wenzelm@42830 | 2 |
Author: Brian Huffman |
huffman@30033 | 3 |
*) |
huffman@30033 | 4 |
|
huffman@30033 | 5 |
header {* Archimedean Fields, Floor and Ceiling Functions *} |
huffman@30033 | 6 |
|
huffman@30033 | 7 |
theory Archimedean_Field |
huffman@30033 | 8 |
imports Main |
huffman@30033 | 9 |
begin |
huffman@30033 | 10 |
|
huffman@30033 | 11 |
subsection {* Class of Archimedean fields *} |
huffman@30033 | 12 |
|
huffman@30033 | 13 |
text {* Archimedean fields have no infinite elements. *} |
huffman@30033 | 14 |
|
haftmann@35028 | 15 |
class archimedean_field = linordered_field + number_ring + |
huffman@30033 | 16 |
assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" |
huffman@30033 | 17 |
|
huffman@30033 | 18 |
lemma ex_less_of_int: |
huffman@30033 | 19 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z" |
huffman@30033 | 20 |
proof - |
huffman@30033 | 21 |
from ex_le_of_int obtain z where "x \<le> of_int z" .. |
huffman@30033 | 22 |
then have "x < of_int (z + 1)" by simp |
huffman@30033 | 23 |
then show ?thesis .. |
huffman@30033 | 24 |
qed |
huffman@30033 | 25 |
|
huffman@30033 | 26 |
lemma ex_of_int_less: |
huffman@30033 | 27 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x" |
huffman@30033 | 28 |
proof - |
huffman@30033 | 29 |
from ex_less_of_int obtain z where "- x < of_int z" .. |
huffman@30033 | 30 |
then have "of_int (- z) < x" by simp |
huffman@30033 | 31 |
then show ?thesis .. |
huffman@30033 | 32 |
qed |
huffman@30033 | 33 |
|
huffman@30033 | 34 |
lemma ex_less_of_nat: |
huffman@30033 | 35 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n" |
huffman@30033 | 36 |
proof - |
huffman@30033 | 37 |
obtain z where "x < of_int z" using ex_less_of_int .. |
huffman@30033 | 38 |
also have "\<dots> \<le> of_int (int (nat z))" by simp |
huffman@30033 | 39 |
also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq) |
huffman@30033 | 40 |
finally show ?thesis .. |
huffman@30033 | 41 |
qed |
huffman@30033 | 42 |
|
huffman@30033 | 43 |
lemma ex_le_of_nat: |
huffman@30033 | 44 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n" |
huffman@30033 | 45 |
proof - |
huffman@30033 | 46 |
obtain n where "x < of_nat n" using ex_less_of_nat .. |
huffman@30033 | 47 |
then have "x \<le> of_nat n" by simp |
huffman@30033 | 48 |
then show ?thesis .. |
huffman@30033 | 49 |
qed |
huffman@30033 | 50 |
|
huffman@30033 | 51 |
text {* Archimedean fields have no infinitesimal elements. *} |
huffman@30033 | 52 |
|
huffman@30033 | 53 |
lemma ex_inverse_of_nat_Suc_less: |
huffman@30033 | 54 |
fixes x :: "'a::archimedean_field" |
huffman@30033 | 55 |
assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x" |
huffman@30033 | 56 |
proof - |
huffman@30033 | 57 |
from `0 < x` have "0 < inverse x" |
huffman@30033 | 58 |
by (rule positive_imp_inverse_positive) |
huffman@30033 | 59 |
obtain n where "inverse x < of_nat n" |
huffman@30033 | 60 |
using ex_less_of_nat .. |
huffman@30033 | 61 |
then obtain m where "inverse x < of_nat (Suc m)" |
huffman@30033 | 62 |
using `0 < inverse x` by (cases n) (simp_all del: of_nat_Suc) |
huffman@30033 | 63 |
then have "inverse (of_nat (Suc m)) < inverse (inverse x)" |
huffman@30033 | 64 |
using `0 < inverse x` by (rule less_imp_inverse_less) |
huffman@30033 | 65 |
then have "inverse (of_nat (Suc m)) < x" |
huffman@30033 | 66 |
using `0 < x` by (simp add: nonzero_inverse_inverse_eq) |
huffman@30033 | 67 |
then show ?thesis .. |
huffman@30033 | 68 |
qed |
huffman@30033 | 69 |
|
huffman@30033 | 70 |
lemma ex_inverse_of_nat_less: |
huffman@30033 | 71 |
fixes x :: "'a::archimedean_field" |
huffman@30033 | 72 |
assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x" |
huffman@30033 | 73 |
using ex_inverse_of_nat_Suc_less [OF `0 < x`] by auto |
huffman@30033 | 74 |
|
huffman@30033 | 75 |
lemma ex_less_of_nat_mult: |
huffman@30033 | 76 |
fixes x :: "'a::archimedean_field" |
huffman@30033 | 77 |
assumes "0 < x" shows "\<exists>n. y < of_nat n * x" |
huffman@30033 | 78 |
proof - |
huffman@30033 | 79 |
obtain n where "y / x < of_nat n" using ex_less_of_nat .. |
huffman@30033 | 80 |
with `0 < x` have "y < of_nat n * x" by (simp add: pos_divide_less_eq) |
huffman@30033 | 81 |
then show ?thesis .. |
huffman@30033 | 82 |
qed |
huffman@30033 | 83 |
|
huffman@30033 | 84 |
|
huffman@30033 | 85 |
subsection {* Existence and uniqueness of floor function *} |
huffman@30033 | 86 |
|
huffman@30033 | 87 |
lemma exists_least_lemma: |
huffman@30033 | 88 |
assumes "\<not> P 0" and "\<exists>n. P n" |
huffman@30033 | 89 |
shows "\<exists>n. \<not> P n \<and> P (Suc n)" |
huffman@30033 | 90 |
proof - |
huffman@30033 | 91 |
from `\<exists>n. P n` have "P (Least P)" by (rule LeastI_ex) |
huffman@30033 | 92 |
with `\<not> P 0` obtain n where "Least P = Suc n" |
huffman@30033 | 93 |
by (cases "Least P") auto |
huffman@30033 | 94 |
then have "n < Least P" by simp |
huffman@30033 | 95 |
then have "\<not> P n" by (rule not_less_Least) |
huffman@30033 | 96 |
then have "\<not> P n \<and> P (Suc n)" |
huffman@30033 | 97 |
using `P (Least P)` `Least P = Suc n` by simp |
huffman@30033 | 98 |
then show ?thesis .. |
huffman@30033 | 99 |
qed |
huffman@30033 | 100 |
|
huffman@30033 | 101 |
lemma floor_exists: |
huffman@30033 | 102 |
fixes x :: "'a::archimedean_field" |
huffman@30033 | 103 |
shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
huffman@30033 | 104 |
proof (cases) |
huffman@30033 | 105 |
assume "0 \<le> x" |
huffman@30033 | 106 |
then have "\<not> x < of_nat 0" by simp |
huffman@30033 | 107 |
then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)" |
huffman@30033 | 108 |
using ex_less_of_nat by (rule exists_least_lemma) |
huffman@30033 | 109 |
then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" .. |
huffman@30033 | 110 |
then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp |
huffman@30033 | 111 |
then show ?thesis .. |
huffman@30033 | 112 |
next |
huffman@30033 | 113 |
assume "\<not> 0 \<le> x" |
huffman@30033 | 114 |
then have "\<not> - x \<le> of_nat 0" by simp |
huffman@30033 | 115 |
then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" |
huffman@30033 | 116 |
using ex_le_of_nat by (rule exists_least_lemma) |
huffman@30033 | 117 |
then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" .. |
huffman@30033 | 118 |
then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp |
huffman@30033 | 119 |
then show ?thesis .. |
huffman@30033 | 120 |
qed |
huffman@30033 | 121 |
|
huffman@30033 | 122 |
lemma floor_exists1: |
huffman@30033 | 123 |
fixes x :: "'a::archimedean_field" |
huffman@30033 | 124 |
shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)" |
huffman@30033 | 125 |
proof (rule ex_ex1I) |
huffman@30033 | 126 |
show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
huffman@30033 | 127 |
by (rule floor_exists) |
huffman@30033 | 128 |
next |
huffman@30033 | 129 |
fix y z assume |
huffman@30033 | 130 |
"of_int y \<le> x \<and> x < of_int (y + 1)" |
huffman@30033 | 131 |
"of_int z \<le> x \<and> x < of_int (z + 1)" |
huffman@30033 | 132 |
then have |
huffman@30033 | 133 |
"of_int y \<le> x" "x < of_int (y + 1)" |
huffman@30033 | 134 |
"of_int z \<le> x" "x < of_int (z + 1)" |
huffman@30033 | 135 |
by simp_all |
huffman@30033 | 136 |
from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`] |
huffman@30033 | 137 |
le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`] |
huffman@30033 | 138 |
show "y = z" by (simp del: of_int_add) |
huffman@30033 | 139 |
qed |
huffman@30033 | 140 |
|
huffman@30033 | 141 |
|
huffman@30033 | 142 |
subsection {* Floor function *} |
huffman@30033 | 143 |
|
huffman@30033 | 144 |
definition |
huffman@30033 | 145 |
floor :: "'a::archimedean_field \<Rightarrow> int" where |
bulwahn@44566 | 146 |
[code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" |
huffman@30033 | 147 |
|
huffman@30033 | 148 |
notation (xsymbols) |
huffman@30033 | 149 |
floor ("\<lfloor>_\<rfloor>") |
huffman@30033 | 150 |
|
huffman@30033 | 151 |
notation (HTML output) |
huffman@30033 | 152 |
floor ("\<lfloor>_\<rfloor>") |
huffman@30033 | 153 |
|
huffman@30033 | 154 |
lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" |
huffman@30033 | 155 |
unfolding floor_def using floor_exists1 by (rule theI') |
huffman@30033 | 156 |
|
huffman@30033 | 157 |
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z" |
huffman@30033 | 158 |
using floor_correct [of x] floor_exists1 [of x] by auto |
huffman@30033 | 159 |
|
huffman@30033 | 160 |
lemma of_int_floor_le: "of_int (floor x) \<le> x" |
huffman@30033 | 161 |
using floor_correct .. |
huffman@30033 | 162 |
|
huffman@30033 | 163 |
lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x" |
huffman@30033 | 164 |
proof |
huffman@30033 | 165 |
assume "z \<le> floor x" |
huffman@30033 | 166 |
then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp |
huffman@30033 | 167 |
also have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
huffman@30033 | 168 |
finally show "of_int z \<le> x" . |
huffman@30033 | 169 |
next |
huffman@30033 | 170 |
assume "of_int z \<le> x" |
huffman@30033 | 171 |
also have "x < of_int (floor x + 1)" using floor_correct .. |
huffman@30033 | 172 |
finally show "z \<le> floor x" by (simp del: of_int_add) |
huffman@30033 | 173 |
qed |
huffman@30033 | 174 |
|
huffman@30033 | 175 |
lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z" |
huffman@30033 | 176 |
by (simp add: not_le [symmetric] le_floor_iff) |
huffman@30033 | 177 |
|
huffman@30033 | 178 |
lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x" |
huffman@30033 | 179 |
using le_floor_iff [of "z + 1" x] by auto |
huffman@30033 | 180 |
|
huffman@30033 | 181 |
lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1" |
huffman@30033 | 182 |
by (simp add: not_less [symmetric] less_floor_iff) |
huffman@30033 | 183 |
|
huffman@30033 | 184 |
lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y" |
huffman@30033 | 185 |
proof - |
huffman@30033 | 186 |
have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
huffman@30033 | 187 |
also note `x \<le> y` |
huffman@30033 | 188 |
finally show ?thesis by (simp add: le_floor_iff) |
huffman@30033 | 189 |
qed |
huffman@30033 | 190 |
|
huffman@30033 | 191 |
lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y" |
huffman@30033 | 192 |
by (auto simp add: not_le [symmetric] floor_mono) |
huffman@30033 | 193 |
|
huffman@30033 | 194 |
lemma floor_of_int [simp]: "floor (of_int z) = z" |
huffman@30033 | 195 |
by (rule floor_unique) simp_all |
huffman@30033 | 196 |
|
huffman@30033 | 197 |
lemma floor_of_nat [simp]: "floor (of_nat n) = int n" |
huffman@30033 | 198 |
using floor_of_int [of "of_nat n"] by simp |
huffman@30033 | 199 |
|
huffman@30033 | 200 |
text {* Floor with numerals *} |
huffman@30033 | 201 |
|
huffman@30033 | 202 |
lemma floor_zero [simp]: "floor 0 = 0" |
huffman@30033 | 203 |
using floor_of_int [of 0] by simp |
huffman@30033 | 204 |
|
huffman@30033 | 205 |
lemma floor_one [simp]: "floor 1 = 1" |
huffman@30033 | 206 |
using floor_of_int [of 1] by simp |
huffman@30033 | 207 |
|
huffman@30033 | 208 |
lemma floor_number_of [simp]: "floor (number_of v) = number_of v" |
huffman@30033 | 209 |
using floor_of_int [of "number_of v"] by simp |
huffman@30033 | 210 |
|
huffman@30033 | 211 |
lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x" |
huffman@30033 | 212 |
by (simp add: le_floor_iff) |
huffman@30033 | 213 |
|
huffman@30033 | 214 |
lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x" |
huffman@30033 | 215 |
by (simp add: le_floor_iff) |
huffman@30033 | 216 |
|
huffman@30033 | 217 |
lemma number_of_le_floor [simp]: "number_of v \<le> floor x \<longleftrightarrow> number_of v \<le> x" |
huffman@30033 | 218 |
by (simp add: le_floor_iff) |
huffman@30033 | 219 |
|
huffman@30033 | 220 |
lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x" |
huffman@30033 | 221 |
by (simp add: less_floor_iff) |
huffman@30033 | 222 |
|
huffman@30033 | 223 |
lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x" |
huffman@30033 | 224 |
by (simp add: less_floor_iff) |
huffman@30033 | 225 |
|
huffman@30033 | 226 |
lemma number_of_less_floor [simp]: |
huffman@30033 | 227 |
"number_of v < floor x \<longleftrightarrow> number_of v + 1 \<le> x" |
huffman@30033 | 228 |
by (simp add: less_floor_iff) |
huffman@30033 | 229 |
|
huffman@30033 | 230 |
lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1" |
huffman@30033 | 231 |
by (simp add: floor_le_iff) |
huffman@30033 | 232 |
|
huffman@30033 | 233 |
lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2" |
huffman@30033 | 234 |
by (simp add: floor_le_iff) |
huffman@30033 | 235 |
|
huffman@30033 | 236 |
lemma floor_le_number_of [simp]: |
huffman@30033 | 237 |
"floor x \<le> number_of v \<longleftrightarrow> x < number_of v + 1" |
huffman@30033 | 238 |
by (simp add: floor_le_iff) |
huffman@30033 | 239 |
|
huffman@30033 | 240 |
lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0" |
huffman@30033 | 241 |
by (simp add: floor_less_iff) |
huffman@30033 | 242 |
|
huffman@30033 | 243 |
lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1" |
huffman@30033 | 244 |
by (simp add: floor_less_iff) |
huffman@30033 | 245 |
|
huffman@30033 | 246 |
lemma floor_less_number_of [simp]: |
huffman@30033 | 247 |
"floor x < number_of v \<longleftrightarrow> x < number_of v" |
huffman@30033 | 248 |
by (simp add: floor_less_iff) |
huffman@30033 | 249 |
|
huffman@30033 | 250 |
text {* Addition and subtraction of integers *} |
huffman@30033 | 251 |
|
huffman@30033 | 252 |
lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z" |
huffman@30033 | 253 |
using floor_correct [of x] by (simp add: floor_unique) |
huffman@30033 | 254 |
|
huffman@30033 | 255 |
lemma floor_add_number_of [simp]: |
huffman@30033 | 256 |
"floor (x + number_of v) = floor x + number_of v" |
huffman@30033 | 257 |
using floor_add_of_int [of x "number_of v"] by simp |
huffman@30033 | 258 |
|
huffman@30033 | 259 |
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" |
huffman@30033 | 260 |
using floor_add_of_int [of x 1] by simp |
huffman@30033 | 261 |
|
huffman@30033 | 262 |
lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z" |
huffman@30033 | 263 |
using floor_add_of_int [of x "- z"] by (simp add: algebra_simps) |
huffman@30033 | 264 |
|
huffman@30033 | 265 |
lemma floor_diff_number_of [simp]: |
huffman@30033 | 266 |
"floor (x - number_of v) = floor x - number_of v" |
huffman@30033 | 267 |
using floor_diff_of_int [of x "number_of v"] by simp |
huffman@30033 | 268 |
|
huffman@30033 | 269 |
lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1" |
huffman@30033 | 270 |
using floor_diff_of_int [of x 1] by simp |
huffman@30033 | 271 |
|
huffman@30033 | 272 |
|
huffman@30033 | 273 |
subsection {* Ceiling function *} |
huffman@30033 | 274 |
|
huffman@30033 | 275 |
definition |
huffman@30033 | 276 |
ceiling :: "'a::archimedean_field \<Rightarrow> int" where |
bulwahn@44566 | 277 |
[code del]: "ceiling x = - floor (- x)" |
huffman@30033 | 278 |
|
huffman@30033 | 279 |
notation (xsymbols) |
huffman@30033 | 280 |
ceiling ("\<lceil>_\<rceil>") |
huffman@30033 | 281 |
|
huffman@30033 | 282 |
notation (HTML output) |
huffman@30033 | 283 |
ceiling ("\<lceil>_\<rceil>") |
huffman@30033 | 284 |
|
huffman@30033 | 285 |
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)" |
huffman@30033 | 286 |
unfolding ceiling_def using floor_correct [of "- x"] by simp |
huffman@30033 | 287 |
|
huffman@30033 | 288 |
lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z" |
huffman@30033 | 289 |
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp |
huffman@30033 | 290 |
|
huffman@30033 | 291 |
lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)" |
huffman@30033 | 292 |
using ceiling_correct .. |
huffman@30033 | 293 |
|
huffman@30033 | 294 |
lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z" |
huffman@30033 | 295 |
unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto |
huffman@30033 | 296 |
|
huffman@30033 | 297 |
lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x" |
huffman@30033 | 298 |
by (simp add: not_le [symmetric] ceiling_le_iff) |
huffman@30033 | 299 |
|
huffman@30033 | 300 |
lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1" |
huffman@30033 | 301 |
using ceiling_le_iff [of x "z - 1"] by simp |
huffman@30033 | 302 |
|
huffman@30033 | 303 |
lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x" |
huffman@30033 | 304 |
by (simp add: not_less [symmetric] ceiling_less_iff) |
huffman@30033 | 305 |
|
huffman@30033 | 306 |
lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y" |
huffman@30033 | 307 |
unfolding ceiling_def by (simp add: floor_mono) |
huffman@30033 | 308 |
|
huffman@30033 | 309 |
lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y" |
huffman@30033 | 310 |
by (auto simp add: not_le [symmetric] ceiling_mono) |
huffman@30033 | 311 |
|
huffman@30033 | 312 |
lemma ceiling_of_int [simp]: "ceiling (of_int z) = z" |
huffman@30033 | 313 |
by (rule ceiling_unique) simp_all |
huffman@30033 | 314 |
|
huffman@30033 | 315 |
lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n" |
huffman@30033 | 316 |
using ceiling_of_int [of "of_nat n"] by simp |
huffman@30033 | 317 |
|
huffman@30033 | 318 |
text {* Ceiling with numerals *} |
huffman@30033 | 319 |
|
huffman@30033 | 320 |
lemma ceiling_zero [simp]: "ceiling 0 = 0" |
huffman@30033 | 321 |
using ceiling_of_int [of 0] by simp |
huffman@30033 | 322 |
|
huffman@30033 | 323 |
lemma ceiling_one [simp]: "ceiling 1 = 1" |
huffman@30033 | 324 |
using ceiling_of_int [of 1] by simp |
huffman@30033 | 325 |
|
huffman@30033 | 326 |
lemma ceiling_number_of [simp]: "ceiling (number_of v) = number_of v" |
huffman@30033 | 327 |
using ceiling_of_int [of "number_of v"] by simp |
huffman@30033 | 328 |
|
huffman@30033 | 329 |
lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0" |
huffman@30033 | 330 |
by (simp add: ceiling_le_iff) |
huffman@30033 | 331 |
|
huffman@30033 | 332 |
lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1" |
huffman@30033 | 333 |
by (simp add: ceiling_le_iff) |
huffman@30033 | 334 |
|
huffman@30033 | 335 |
lemma ceiling_le_number_of [simp]: |
huffman@30033 | 336 |
"ceiling x \<le> number_of v \<longleftrightarrow> x \<le> number_of v" |
huffman@30033 | 337 |
by (simp add: ceiling_le_iff) |
huffman@30033 | 338 |
|
huffman@30033 | 339 |
lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1" |
huffman@30033 | 340 |
by (simp add: ceiling_less_iff) |
huffman@30033 | 341 |
|
huffman@30033 | 342 |
lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0" |
huffman@30033 | 343 |
by (simp add: ceiling_less_iff) |
huffman@30033 | 344 |
|
huffman@30033 | 345 |
lemma ceiling_less_number_of [simp]: |
huffman@30033 | 346 |
"ceiling x < number_of v \<longleftrightarrow> x \<le> number_of v - 1" |
huffman@30033 | 347 |
by (simp add: ceiling_less_iff) |
huffman@30033 | 348 |
|
huffman@30033 | 349 |
lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x" |
huffman@30033 | 350 |
by (simp add: le_ceiling_iff) |
huffman@30033 | 351 |
|
huffman@30033 | 352 |
lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x" |
huffman@30033 | 353 |
by (simp add: le_ceiling_iff) |
huffman@30033 | 354 |
|
huffman@30033 | 355 |
lemma number_of_le_ceiling [simp]: |
huffman@30033 | 356 |
"number_of v \<le> ceiling x\<longleftrightarrow> number_of v - 1 < x" |
huffman@30033 | 357 |
by (simp add: le_ceiling_iff) |
huffman@30033 | 358 |
|
huffman@30033 | 359 |
lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x" |
huffman@30033 | 360 |
by (simp add: less_ceiling_iff) |
huffman@30033 | 361 |
|
huffman@30033 | 362 |
lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x" |
huffman@30033 | 363 |
by (simp add: less_ceiling_iff) |
huffman@30033 | 364 |
|
huffman@30033 | 365 |
lemma number_of_less_ceiling [simp]: |
huffman@30033 | 366 |
"number_of v < ceiling x \<longleftrightarrow> number_of v < x" |
huffman@30033 | 367 |
by (simp add: less_ceiling_iff) |
huffman@30033 | 368 |
|
huffman@30033 | 369 |
text {* Addition and subtraction of integers *} |
huffman@30033 | 370 |
|
huffman@30033 | 371 |
lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z" |
huffman@30033 | 372 |
using ceiling_correct [of x] by (simp add: ceiling_unique) |
huffman@30033 | 373 |
|
huffman@30033 | 374 |
lemma ceiling_add_number_of [simp]: |
huffman@30033 | 375 |
"ceiling (x + number_of v) = ceiling x + number_of v" |
huffman@30033 | 376 |
using ceiling_add_of_int [of x "number_of v"] by simp |
huffman@30033 | 377 |
|
huffman@30033 | 378 |
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" |
huffman@30033 | 379 |
using ceiling_add_of_int [of x 1] by simp |
huffman@30033 | 380 |
|
huffman@30033 | 381 |
lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z" |
huffman@30033 | 382 |
using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps) |
huffman@30033 | 383 |
|
huffman@30033 | 384 |
lemma ceiling_diff_number_of [simp]: |
huffman@30033 | 385 |
"ceiling (x - number_of v) = ceiling x - number_of v" |
huffman@30033 | 386 |
using ceiling_diff_of_int [of x "number_of v"] by simp |
huffman@30033 | 387 |
|
huffman@30033 | 388 |
lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1" |
huffman@30033 | 389 |
using ceiling_diff_of_int [of x 1] by simp |
huffman@30033 | 390 |
|
huffman@30033 | 391 |
|
huffman@30033 | 392 |
subsection {* Negation *} |
huffman@30033 | 393 |
|
huffman@30038 | 394 |
lemma floor_minus: "floor (- x) = - ceiling x" |
huffman@30033 | 395 |
unfolding ceiling_def by simp |
huffman@30033 | 396 |
|
huffman@30038 | 397 |
lemma ceiling_minus: "ceiling (- x) = - floor x" |
huffman@30033 | 398 |
unfolding ceiling_def by simp |
huffman@30033 | 399 |
|
huffman@30033 | 400 |
end |