author | haftmann |
Thu, 09 Apr 2015 09:12:47 +0200 | |
changeset 59984 | 4f1eccec320c |
parent 59613 | 7103019278f0 |
child 60128 | 3d696ccb7fa6 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Archimedean_Field.thy |
2 |
Author: Brian Huffman |
|
30096 | 3 |
*) |
4 |
||
58889 | 5 |
section {* Archimedean Fields, Floor and Ceiling Functions *} |
30096 | 6 |
|
7 |
theory Archimedean_Field |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
11 |
subsection {* Class of Archimedean fields *} |
|
12 |
||
13 |
text {* Archimedean fields have no infinite elements. *} |
|
14 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
15 |
class archimedean_field = linordered_field + |
30096 | 16 |
assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" |
17 |
||
18 |
lemma ex_less_of_int: |
|
19 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z" |
|
20 |
proof - |
|
21 |
from ex_le_of_int obtain z where "x \<le> of_int z" .. |
|
22 |
then have "x < of_int (z + 1)" by simp |
|
23 |
then show ?thesis .. |
|
24 |
qed |
|
25 |
||
26 |
lemma ex_of_int_less: |
|
27 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x" |
|
28 |
proof - |
|
29 |
from ex_less_of_int obtain z where "- x < of_int z" .. |
|
30 |
then have "of_int (- z) < x" by simp |
|
31 |
then show ?thesis .. |
|
32 |
qed |
|
33 |
||
34 |
lemma ex_less_of_nat: |
|
35 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n" |
|
36 |
proof - |
|
37 |
obtain z where "x < of_int z" using ex_less_of_int .. |
|
38 |
also have "\<dots> \<le> of_int (int (nat z))" by simp |
|
39 |
also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq) |
|
40 |
finally show ?thesis .. |
|
41 |
qed |
|
42 |
||
43 |
lemma ex_le_of_nat: |
|
44 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n" |
|
45 |
proof - |
|
46 |
obtain n where "x < of_nat n" using ex_less_of_nat .. |
|
47 |
then have "x \<le> of_nat n" by simp |
|
48 |
then show ?thesis .. |
|
49 |
qed |
|
50 |
||
51 |
text {* Archimedean fields have no infinitesimal elements. *} |
|
52 |
||
53 |
lemma ex_inverse_of_nat_Suc_less: |
|
54 |
fixes x :: "'a::archimedean_field" |
|
55 |
assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x" |
|
56 |
proof - |
|
57 |
from `0 < x` have "0 < inverse x" |
|
58 |
by (rule positive_imp_inverse_positive) |
|
59 |
obtain n where "inverse x < of_nat n" |
|
60 |
using ex_less_of_nat .. |
|
61 |
then obtain m where "inverse x < of_nat (Suc m)" |
|
62 |
using `0 < inverse x` by (cases n) (simp_all del: of_nat_Suc) |
|
63 |
then have "inverse (of_nat (Suc m)) < inverse (inverse x)" |
|
64 |
using `0 < inverse x` by (rule less_imp_inverse_less) |
|
65 |
then have "inverse (of_nat (Suc m)) < x" |
|
66 |
using `0 < x` by (simp add: nonzero_inverse_inverse_eq) |
|
67 |
then show ?thesis .. |
|
68 |
qed |
|
69 |
||
70 |
lemma ex_inverse_of_nat_less: |
|
71 |
fixes x :: "'a::archimedean_field" |
|
72 |
assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x" |
|
73 |
using ex_inverse_of_nat_Suc_less [OF `0 < x`] by auto |
|
74 |
||
75 |
lemma ex_less_of_nat_mult: |
|
76 |
fixes x :: "'a::archimedean_field" |
|
77 |
assumes "0 < x" shows "\<exists>n. y < of_nat n * x" |
|
78 |
proof - |
|
79 |
obtain n where "y / x < of_nat n" using ex_less_of_nat .. |
|
80 |
with `0 < x` have "y < of_nat n * x" by (simp add: pos_divide_less_eq) |
|
81 |
then show ?thesis .. |
|
82 |
qed |
|
83 |
||
84 |
||
85 |
subsection {* Existence and uniqueness of floor function *} |
|
86 |
||
87 |
lemma exists_least_lemma: |
|
88 |
assumes "\<not> P 0" and "\<exists>n. P n" |
|
89 |
shows "\<exists>n. \<not> P n \<and> P (Suc n)" |
|
90 |
proof - |
|
91 |
from `\<exists>n. P n` have "P (Least P)" by (rule LeastI_ex) |
|
92 |
with `\<not> P 0` obtain n where "Least P = Suc n" |
|
93 |
by (cases "Least P") auto |
|
94 |
then have "n < Least P" by simp |
|
95 |
then have "\<not> P n" by (rule not_less_Least) |
|
96 |
then have "\<not> P n \<and> P (Suc n)" |
|
97 |
using `P (Least P)` `Least P = Suc n` by simp |
|
98 |
then show ?thesis .. |
|
99 |
qed |
|
100 |
||
101 |
lemma floor_exists: |
|
102 |
fixes x :: "'a::archimedean_field" |
|
103 |
shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
104 |
proof (cases) |
|
105 |
assume "0 \<le> x" |
|
106 |
then have "\<not> x < of_nat 0" by simp |
|
107 |
then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)" |
|
108 |
using ex_less_of_nat by (rule exists_least_lemma) |
|
109 |
then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" .. |
|
110 |
then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp |
|
111 |
then show ?thesis .. |
|
112 |
next |
|
113 |
assume "\<not> 0 \<le> x" |
|
114 |
then have "\<not> - x \<le> of_nat 0" by simp |
|
115 |
then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" |
|
116 |
using ex_le_of_nat by (rule exists_least_lemma) |
|
117 |
then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" .. |
|
118 |
then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp |
|
119 |
then show ?thesis .. |
|
120 |
qed |
|
121 |
||
122 |
lemma floor_exists1: |
|
123 |
fixes x :: "'a::archimedean_field" |
|
124 |
shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
125 |
proof (rule ex_ex1I) |
|
126 |
show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
127 |
by (rule floor_exists) |
|
128 |
next |
|
129 |
fix y z assume |
|
130 |
"of_int y \<le> x \<and> x < of_int (y + 1)" |
|
131 |
"of_int z \<le> x \<and> x < of_int (z + 1)" |
|
54281 | 132 |
with le_less_trans [of "of_int y" "x" "of_int (z + 1)"] |
133 |
le_less_trans [of "of_int z" "x" "of_int (y + 1)"] |
|
30096 | 134 |
show "y = z" by (simp del: of_int_add) |
135 |
qed |
|
136 |
||
137 |
||
138 |
subsection {* Floor function *} |
|
139 |
||
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
140 |
class floor_ceiling = archimedean_field + |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
141 |
fixes floor :: "'a \<Rightarrow> int" |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
142 |
assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" |
30096 | 143 |
|
144 |
notation (xsymbols) |
|
145 |
floor ("\<lfloor>_\<rfloor>") |
|
146 |
||
147 |
notation (HTML output) |
|
148 |
floor ("\<lfloor>_\<rfloor>") |
|
149 |
||
150 |
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z" |
|
151 |
using floor_correct [of x] floor_exists1 [of x] by auto |
|
152 |
||
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
153 |
lemma floor_unique_iff: |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
154 |
fixes x :: "'a::floor_ceiling" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
155 |
shows "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
156 |
using floor_correct floor_unique by auto |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
157 |
|
30096 | 158 |
lemma of_int_floor_le: "of_int (floor x) \<le> x" |
159 |
using floor_correct .. |
|
160 |
||
161 |
lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x" |
|
162 |
proof |
|
163 |
assume "z \<le> floor x" |
|
164 |
then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp |
|
165 |
also have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
|
166 |
finally show "of_int z \<le> x" . |
|
167 |
next |
|
168 |
assume "of_int z \<le> x" |
|
169 |
also have "x < of_int (floor x + 1)" using floor_correct .. |
|
170 |
finally show "z \<le> floor x" by (simp del: of_int_add) |
|
171 |
qed |
|
172 |
||
173 |
lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z" |
|
174 |
by (simp add: not_le [symmetric] le_floor_iff) |
|
175 |
||
176 |
lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x" |
|
177 |
using le_floor_iff [of "z + 1" x] by auto |
|
178 |
||
179 |
lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1" |
|
180 |
by (simp add: not_less [symmetric] less_floor_iff) |
|
181 |
||
58040
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
182 |
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)" |
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
183 |
by (metis floor_correct floor_unique less_floor_iff not_le order_refl) |
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
184 |
|
30096 | 185 |
lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y" |
186 |
proof - |
|
187 |
have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
|
188 |
also note `x \<le> y` |
|
189 |
finally show ?thesis by (simp add: le_floor_iff) |
|
190 |
qed |
|
191 |
||
192 |
lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y" |
|
193 |
by (auto simp add: not_le [symmetric] floor_mono) |
|
194 |
||
195 |
lemma floor_of_int [simp]: "floor (of_int z) = z" |
|
196 |
by (rule floor_unique) simp_all |
|
197 |
||
198 |
lemma floor_of_nat [simp]: "floor (of_nat n) = int n" |
|
199 |
using floor_of_int [of "of_nat n"] by simp |
|
200 |
||
47307
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
201 |
lemma le_floor_add: "floor x + floor y \<le> floor (x + y)" |
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
202 |
by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le) |
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
203 |
|
30096 | 204 |
text {* Floor with numerals *} |
205 |
||
206 |
lemma floor_zero [simp]: "floor 0 = 0" |
|
207 |
using floor_of_int [of 0] by simp |
|
208 |
||
209 |
lemma floor_one [simp]: "floor 1 = 1" |
|
210 |
using floor_of_int [of 1] by simp |
|
211 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
212 |
lemma floor_numeral [simp]: "floor (numeral v) = numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
213 |
using floor_of_int [of "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
214 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
215 |
lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
216 |
using floor_of_int [of "- numeral v"] by simp |
30096 | 217 |
|
218 |
lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x" |
|
219 |
by (simp add: le_floor_iff) |
|
220 |
||
221 |
lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x" |
|
222 |
by (simp add: le_floor_iff) |
|
223 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
224 |
lemma numeral_le_floor [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
225 |
"numeral v \<le> floor x \<longleftrightarrow> numeral v \<le> x" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
226 |
by (simp add: le_floor_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
227 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
228 |
lemma neg_numeral_le_floor [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
229 |
"- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x" |
30096 | 230 |
by (simp add: le_floor_iff) |
231 |
||
232 |
lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x" |
|
233 |
by (simp add: less_floor_iff) |
|
234 |
||
235 |
lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x" |
|
236 |
by (simp add: less_floor_iff) |
|
237 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
238 |
lemma numeral_less_floor [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
239 |
"numeral v < floor x \<longleftrightarrow> numeral v + 1 \<le> x" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
240 |
by (simp add: less_floor_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
241 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
242 |
lemma neg_numeral_less_floor [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
243 |
"- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x" |
30096 | 244 |
by (simp add: less_floor_iff) |
245 |
||
246 |
lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1" |
|
247 |
by (simp add: floor_le_iff) |
|
248 |
||
249 |
lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2" |
|
250 |
by (simp add: floor_le_iff) |
|
251 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
252 |
lemma floor_le_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
253 |
"floor x \<le> numeral v \<longleftrightarrow> x < numeral v + 1" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
254 |
by (simp add: floor_le_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
255 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
256 |
lemma floor_le_neg_numeral [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
257 |
"floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1" |
30096 | 258 |
by (simp add: floor_le_iff) |
259 |
||
260 |
lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0" |
|
261 |
by (simp add: floor_less_iff) |
|
262 |
||
263 |
lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1" |
|
264 |
by (simp add: floor_less_iff) |
|
265 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
266 |
lemma floor_less_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
267 |
"floor x < numeral v \<longleftrightarrow> x < numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
268 |
by (simp add: floor_less_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
269 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
270 |
lemma floor_less_neg_numeral [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
271 |
"floor x < - numeral v \<longleftrightarrow> x < - numeral v" |
30096 | 272 |
by (simp add: floor_less_iff) |
273 |
||
274 |
text {* Addition and subtraction of integers *} |
|
275 |
||
276 |
lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z" |
|
277 |
using floor_correct [of x] by (simp add: floor_unique) |
|
278 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
279 |
lemma floor_add_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
280 |
"floor (x + numeral v) = floor x + numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
281 |
using floor_add_of_int [of x "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
282 |
|
30096 | 283 |
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" |
284 |
using floor_add_of_int [of x 1] by simp |
|
285 |
||
286 |
lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z" |
|
287 |
using floor_add_of_int [of x "- z"] by (simp add: algebra_simps) |
|
288 |
||
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
289 |
lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
290 |
by (metis floor_diff_of_int [of 0] diff_0 floor_zero) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
291 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
292 |
lemma floor_diff_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
293 |
"floor (x - numeral v) = floor x - numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
294 |
using floor_diff_of_int [of x "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
295 |
|
30096 | 296 |
lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1" |
297 |
using floor_diff_of_int [of x 1] by simp |
|
298 |
||
58097
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
299 |
lemma le_mult_floor: |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
300 |
assumes "0 \<le> a" and "0 \<le> b" |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
301 |
shows "floor a * floor b \<le> floor (a * b)" |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
302 |
proof - |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
303 |
have "of_int (floor a) \<le> a" |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
304 |
and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le) |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
305 |
hence "of_int (floor a * floor b) \<le> a * b" |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
306 |
using assms by (auto intro!: mult_mono) |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
307 |
also have "a * b < of_int (floor (a * b) + 1)" |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
308 |
using floor_correct[of "a * b"] by auto |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
309 |
finally show ?thesis unfolding of_int_less_iff by simp |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
310 |
qed |
cfd3cff9387b
add simp rules for divisions of numerals in floor and ceiling.
hoelzl
parents:
58040
diff
changeset
|
311 |
|
59984
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
312 |
lemma floor_divide_of_int_eq: |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
313 |
fixes k l :: int |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
314 |
shows "\<lfloor>of_int k / of_int l\<rfloor> = of_int (k div l)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
315 |
proof (cases "l = 0") |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
316 |
case True then show ?thesis by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
317 |
next |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
318 |
case False |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
319 |
have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
320 |
proof (cases "l > 0") |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
321 |
case True then show ?thesis |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
322 |
by (auto intro: floor_unique) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
323 |
next |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
324 |
case False |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
325 |
obtain r where "r = - l" by blast |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
326 |
then have l: "l = - r" by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
327 |
moreover with `l \<noteq> 0` False have "r > 0" by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
328 |
ultimately show ?thesis using pos_mod_bound [of r] |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
329 |
by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
330 |
qed |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
331 |
have "(of_int k :: 'a) = of_int (k div l * l + k mod l)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
332 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
333 |
also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
334 |
using False by (simp only: of_int_add) (simp add: field_simps) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
335 |
finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
336 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
337 |
then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
338 |
using False by (simp only:) (simp add: field_simps) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
339 |
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>" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
340 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
341 |
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>" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
342 |
by (simp add: ac_simps) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
343 |
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + of_int (k div l)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
344 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
345 |
with * show ?thesis by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
346 |
qed |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
347 |
|
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
348 |
lemma floor_divide_of_nat_eq: |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
349 |
fixes m n :: nat |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
350 |
shows "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
351 |
proof (cases "n = 0") |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
352 |
case True then show ?thesis by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
353 |
next |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
354 |
case False |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
355 |
then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
356 |
by (auto intro: floor_unique) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
357 |
have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
358 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
359 |
also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
360 |
using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
361 |
finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
362 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
363 |
then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
364 |
using False by (simp only:) simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
365 |
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>" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
366 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
367 |
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>" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
368 |
by (simp add: ac_simps) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
369 |
moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
370 |
by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
371 |
ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)" |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
372 |
by (simp only: floor_add_of_int) |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
373 |
with * show ?thesis by simp |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
374 |
qed |
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
375 |
|
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59613
diff
changeset
|
376 |
|
30096 | 377 |
subsection {* Ceiling function *} |
378 |
||
379 |
definition |
|
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
380 |
ceiling :: "'a::floor_ceiling \<Rightarrow> int" where |
43733
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
381 |
"ceiling x = - floor (- x)" |
30096 | 382 |
|
383 |
notation (xsymbols) |
|
384 |
ceiling ("\<lceil>_\<rceil>") |
|
385 |
||
386 |
notation (HTML output) |
|
387 |
ceiling ("\<lceil>_\<rceil>") |
|
388 |
||
389 |
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)" |
|
390 |
unfolding ceiling_def using floor_correct [of "- x"] by simp |
|
391 |
||
392 |
lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z" |
|
393 |
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp |
|
394 |
||
395 |
lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)" |
|
396 |
using ceiling_correct .. |
|
397 |
||
398 |
lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z" |
|
399 |
unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto |
|
400 |
||
401 |
lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x" |
|
402 |
by (simp add: not_le [symmetric] ceiling_le_iff) |
|
403 |
||
404 |
lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1" |
|
405 |
using ceiling_le_iff [of x "z - 1"] by simp |
|
406 |
||
407 |
lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x" |
|
408 |
by (simp add: not_less [symmetric] ceiling_less_iff) |
|
409 |
||
410 |
lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y" |
|
411 |
unfolding ceiling_def by (simp add: floor_mono) |
|
412 |
||
413 |
lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y" |
|
414 |
by (auto simp add: not_le [symmetric] ceiling_mono) |
|
415 |
||
416 |
lemma ceiling_of_int [simp]: "ceiling (of_int z) = z" |
|
417 |
by (rule ceiling_unique) simp_all |
|
418 |
||
419 |
lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n" |
|
420 |
using ceiling_of_int [of "of_nat n"] by simp |
|
421 |
||
47307
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
422 |
lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y" |
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
423 |
by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling) |
5e5ca36692b3
add floor/ceiling lemmas suggested by René Thiemann
huffman
parents:
47108
diff
changeset
|
424 |
|
30096 | 425 |
text {* Ceiling with numerals *} |
426 |
||
427 |
lemma ceiling_zero [simp]: "ceiling 0 = 0" |
|
428 |
using ceiling_of_int [of 0] by simp |
|
429 |
||
430 |
lemma ceiling_one [simp]: "ceiling 1 = 1" |
|
431 |
using ceiling_of_int [of 1] by simp |
|
432 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
433 |
lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
434 |
using ceiling_of_int [of "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
435 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
436 |
lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
437 |
using ceiling_of_int [of "- numeral v"] by simp |
30096 | 438 |
|
439 |
lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0" |
|
440 |
by (simp add: ceiling_le_iff) |
|
441 |
||
442 |
lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1" |
|
443 |
by (simp add: ceiling_le_iff) |
|
444 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
445 |
lemma ceiling_le_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
446 |
"ceiling x \<le> numeral v \<longleftrightarrow> x \<le> numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
447 |
by (simp add: ceiling_le_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
448 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
449 |
lemma ceiling_le_neg_numeral [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
450 |
"ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v" |
30096 | 451 |
by (simp add: ceiling_le_iff) |
452 |
||
453 |
lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1" |
|
454 |
by (simp add: ceiling_less_iff) |
|
455 |
||
456 |
lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0" |
|
457 |
by (simp add: ceiling_less_iff) |
|
458 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
459 |
lemma ceiling_less_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
460 |
"ceiling x < numeral v \<longleftrightarrow> x \<le> numeral v - 1" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
461 |
by (simp add: ceiling_less_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
462 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
463 |
lemma ceiling_less_neg_numeral [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
464 |
"ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1" |
30096 | 465 |
by (simp add: ceiling_less_iff) |
466 |
||
467 |
lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x" |
|
468 |
by (simp add: le_ceiling_iff) |
|
469 |
||
470 |
lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x" |
|
471 |
by (simp add: le_ceiling_iff) |
|
472 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
473 |
lemma numeral_le_ceiling [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
474 |
"numeral v \<le> ceiling x \<longleftrightarrow> numeral v - 1 < x" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
475 |
by (simp add: le_ceiling_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
476 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
477 |
lemma neg_numeral_le_ceiling [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
478 |
"- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x" |
30096 | 479 |
by (simp add: le_ceiling_iff) |
480 |
||
481 |
lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x" |
|
482 |
by (simp add: less_ceiling_iff) |
|
483 |
||
484 |
lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x" |
|
485 |
by (simp add: less_ceiling_iff) |
|
486 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
487 |
lemma numeral_less_ceiling [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
488 |
"numeral v < ceiling x \<longleftrightarrow> numeral v < x" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
489 |
by (simp add: less_ceiling_iff) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
490 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
491 |
lemma neg_numeral_less_ceiling [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54281
diff
changeset
|
492 |
"- numeral v < ceiling x \<longleftrightarrow> - numeral v < x" |
30096 | 493 |
by (simp add: less_ceiling_iff) |
494 |
||
495 |
text {* Addition and subtraction of integers *} |
|
496 |
||
497 |
lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z" |
|
498 |
using ceiling_correct [of x] by (simp add: ceiling_unique) |
|
499 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
500 |
lemma ceiling_add_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
501 |
"ceiling (x + numeral v) = ceiling x + numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
502 |
using ceiling_add_of_int [of x "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
503 |
|
30096 | 504 |
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" |
505 |
using ceiling_add_of_int [of x 1] by simp |
|
506 |
||
507 |
lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z" |
|
508 |
using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps) |
|
509 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
510 |
lemma ceiling_diff_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
511 |
"ceiling (x - numeral v) = ceiling x - numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
512 |
using ceiling_diff_of_int [of x "numeral v"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
43733
diff
changeset
|
513 |
|
30096 | 514 |
lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1" |
515 |
using ceiling_diff_of_int [of x 1] by simp |
|
516 |
||
58040
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
517 |
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)" |
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
518 |
by (auto simp add: ceiling_unique ceiling_correct) |
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
54489
diff
changeset
|
519 |
|
47592 | 520 |
lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1" |
521 |
proof - |
|
522 |
have "of_int \<lceil>x\<rceil> - 1 < x" |
|
523 |
using ceiling_correct[of x] by simp |
|
524 |
also have "x < of_int \<lfloor>x\<rfloor> + 1" |
|
525 |
using floor_correct[of x] by simp_all |
|
526 |
finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)" |
|
527 |
by simp |
|
528 |
then show ?thesis |
|
529 |
unfolding of_int_less_iff by simp |
|
530 |
qed |
|
30096 | 531 |
|
532 |
subsection {* Negation *} |
|
533 |
||
30102 | 534 |
lemma floor_minus: "floor (- x) = - ceiling x" |
30096 | 535 |
unfolding ceiling_def by simp |
536 |
||
30102 | 537 |
lemma ceiling_minus: "ceiling (- x) = - floor x" |
30096 | 538 |
unfolding ceiling_def by simp |
539 |
||
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
540 |
subsection {* Frac Function *} |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
541 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
542 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
543 |
definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
544 |
"frac x \<equiv> x - of_int \<lfloor>x\<rfloor>" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
545 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
546 |
lemma frac_lt_1: "frac x < 1" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
547 |
by (simp add: frac_def) linarith |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
548 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
549 |
lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
550 |
by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int ) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
551 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
552 |
lemma frac_ge_0 [simp]: "frac x \<ge> 0" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
553 |
unfolding frac_def |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
554 |
by linarith |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
555 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
556 |
lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
557 |
by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
558 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
559 |
lemma frac_of_int [simp]: "frac (of_int z) = 0" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
560 |
by (simp add: frac_def) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
561 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
562 |
lemma 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)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
563 |
proof - |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
564 |
{assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
565 |
then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
566 |
by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
567 |
} |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
568 |
moreover |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
569 |
{ assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
570 |
then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
571 |
apply (simp add: floor_unique_iff) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
572 |
apply (auto simp add: algebra_simps) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
573 |
by linarith |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
574 |
} |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
575 |
ultimately show ?thesis |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
576 |
by (auto simp add: frac_def algebra_simps) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
577 |
qed |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
578 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
579 |
lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
580 |
else (frac x + frac y) - 1)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
581 |
by (simp add: frac_def floor_add) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
582 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
583 |
lemma frac_unique_iff: |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
584 |
fixes x :: "'a::floor_ceiling" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
585 |
shows "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
586 |
apply (auto simp: Ints_def frac_def) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
587 |
apply linarith |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
588 |
apply linarith |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
589 |
by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
590 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
591 |
lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
592 |
by (simp add: frac_unique_iff) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
593 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
594 |
lemma frac_neg: |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
595 |
fixes x :: "'a::floor_ceiling" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
596 |
shows "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)" |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
597 |
apply (auto simp add: frac_unique_iff) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
598 |
apply (simp add: frac_def) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
599 |
by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq) |
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
600 |
|
30096 | 601 |
end |