51523
|
1 |
(* Title: HOL/Real.thy
|
|
2 |
Author: Jacques D. Fleuriot, University of Edinburgh, 1998
|
|
3 |
Author: Larry Paulson, University of Cambridge
|
|
4 |
Author: Jeremy Avigad, Carnegie Mellon University
|
|
5 |
Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
|
|
6 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
|
|
7 |
Construction of Cauchy Reals by Brian Huffman, 2010
|
|
8 |
*)
|
|
9 |
|
|
10 |
header {* Development of the Reals using Cauchy Sequences *}
|
|
11 |
|
|
12 |
theory Real
|
|
13 |
imports Rat Conditional_Complete_Lattices
|
|
14 |
begin
|
|
15 |
|
|
16 |
text {*
|
|
17 |
This theory contains a formalization of the real numbers as
|
|
18 |
equivalence classes of Cauchy sequences of rationals. See
|
|
19 |
@{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
|
|
20 |
construction using Dedekind cuts.
|
|
21 |
*}
|
|
22 |
|
|
23 |
subsection {* Preliminary lemmas *}
|
|
24 |
|
|
25 |
lemma add_diff_add:
|
|
26 |
fixes a b c d :: "'a::ab_group_add"
|
|
27 |
shows "(a + c) - (b + d) = (a - b) + (c - d)"
|
|
28 |
by simp
|
|
29 |
|
|
30 |
lemma minus_diff_minus:
|
|
31 |
fixes a b :: "'a::ab_group_add"
|
|
32 |
shows "- a - - b = - (a - b)"
|
|
33 |
by simp
|
|
34 |
|
|
35 |
lemma mult_diff_mult:
|
|
36 |
fixes x y a b :: "'a::ring"
|
|
37 |
shows "(x * y - a * b) = x * (y - b) + (x - a) * b"
|
|
38 |
by (simp add: algebra_simps)
|
|
39 |
|
|
40 |
lemma inverse_diff_inverse:
|
|
41 |
fixes a b :: "'a::division_ring"
|
|
42 |
assumes "a \<noteq> 0" and "b \<noteq> 0"
|
|
43 |
shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
|
|
44 |
using assms by (simp add: algebra_simps)
|
|
45 |
|
|
46 |
lemma obtain_pos_sum:
|
|
47 |
fixes r :: rat assumes r: "0 < r"
|
|
48 |
obtains s t where "0 < s" and "0 < t" and "r = s + t"
|
|
49 |
proof
|
|
50 |
from r show "0 < r/2" by simp
|
|
51 |
from r show "0 < r/2" by simp
|
|
52 |
show "r = r/2 + r/2" by simp
|
|
53 |
qed
|
|
54 |
|
|
55 |
subsection {* Sequences that converge to zero *}
|
|
56 |
|
|
57 |
definition
|
|
58 |
vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
|
|
59 |
where
|
|
60 |
"vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
|
|
61 |
|
|
62 |
lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"
|
|
63 |
unfolding vanishes_def by simp
|
|
64 |
|
|
65 |
lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
|
|
66 |
unfolding vanishes_def by simp
|
|
67 |
|
|
68 |
lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
|
|
69 |
unfolding vanishes_def
|
|
70 |
apply (cases "c = 0", auto)
|
|
71 |
apply (rule exI [where x="\<bar>c\<bar>"], auto)
|
|
72 |
done
|
|
73 |
|
|
74 |
lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
|
|
75 |
unfolding vanishes_def by simp
|
|
76 |
|
|
77 |
lemma vanishes_add:
|
|
78 |
assumes X: "vanishes X" and Y: "vanishes Y"
|
|
79 |
shows "vanishes (\<lambda>n. X n + Y n)"
|
|
80 |
proof (rule vanishesI)
|
|
81 |
fix r :: rat assume "0 < r"
|
|
82 |
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
|
|
83 |
by (rule obtain_pos_sum)
|
|
84 |
obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"
|
|
85 |
using vanishesD [OF X s] ..
|
|
86 |
obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"
|
|
87 |
using vanishesD [OF Y t] ..
|
|
88 |
have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"
|
|
89 |
proof (clarsimp)
|
|
90 |
fix n assume n: "i \<le> n" "j \<le> n"
|
|
91 |
have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
|
|
92 |
also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
|
|
93 |
finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
|
|
94 |
qed
|
|
95 |
thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
|
|
96 |
qed
|
|
97 |
|
|
98 |
lemma vanishes_diff:
|
|
99 |
assumes X: "vanishes X" and Y: "vanishes Y"
|
|
100 |
shows "vanishes (\<lambda>n. X n - Y n)"
|
|
101 |
unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
|
|
102 |
|
|
103 |
lemma vanishes_mult_bounded:
|
|
104 |
assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
|
|
105 |
assumes Y: "vanishes (\<lambda>n. Y n)"
|
|
106 |
shows "vanishes (\<lambda>n. X n * Y n)"
|
|
107 |
proof (rule vanishesI)
|
|
108 |
fix r :: rat assume r: "0 < r"
|
|
109 |
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
|
|
110 |
using X by fast
|
|
111 |
obtain b where b: "0 < b" "r = a * b"
|
|
112 |
proof
|
|
113 |
show "0 < r / a" using r a by (simp add: divide_pos_pos)
|
|
114 |
show "r = a * (r / a)" using a by simp
|
|
115 |
qed
|
|
116 |
obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
|
|
117 |
using vanishesD [OF Y b(1)] ..
|
|
118 |
have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"
|
|
119 |
by (simp add: b(2) abs_mult mult_strict_mono' a k)
|
|
120 |
thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
|
|
121 |
qed
|
|
122 |
|
|
123 |
subsection {* Cauchy sequences *}
|
|
124 |
|
|
125 |
definition
|
|
126 |
cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
|
|
127 |
where
|
|
128 |
"cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
|
|
129 |
|
|
130 |
lemma cauchyI:
|
|
131 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X"
|
|
132 |
unfolding cauchy_def by simp
|
|
133 |
|
|
134 |
lemma cauchyD:
|
|
135 |
"\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
|
|
136 |
unfolding cauchy_def by simp
|
|
137 |
|
|
138 |
lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"
|
|
139 |
unfolding cauchy_def by simp
|
|
140 |
|
|
141 |
lemma cauchy_add [simp]:
|
|
142 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
143 |
shows "cauchy (\<lambda>n. X n + Y n)"
|
|
144 |
proof (rule cauchyI)
|
|
145 |
fix r :: rat assume "0 < r"
|
|
146 |
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
|
|
147 |
by (rule obtain_pos_sum)
|
|
148 |
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
|
|
149 |
using cauchyD [OF X s] ..
|
|
150 |
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
|
|
151 |
using cauchyD [OF Y t] ..
|
|
152 |
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"
|
|
153 |
proof (clarsimp)
|
|
154 |
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
|
|
155 |
have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"
|
|
156 |
unfolding add_diff_add by (rule abs_triangle_ineq)
|
|
157 |
also have "\<dots> < s + t"
|
|
158 |
by (rule add_strict_mono, simp_all add: i j *)
|
|
159 |
finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .
|
|
160 |
qed
|
|
161 |
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
|
|
162 |
qed
|
|
163 |
|
|
164 |
lemma cauchy_minus [simp]:
|
|
165 |
assumes X: "cauchy X"
|
|
166 |
shows "cauchy (\<lambda>n. - X n)"
|
|
167 |
using assms unfolding cauchy_def
|
|
168 |
unfolding minus_diff_minus abs_minus_cancel .
|
|
169 |
|
|
170 |
lemma cauchy_diff [simp]:
|
|
171 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
172 |
shows "cauchy (\<lambda>n. X n - Y n)"
|
|
173 |
using assms unfolding diff_minus by simp
|
|
174 |
|
|
175 |
lemma cauchy_imp_bounded:
|
|
176 |
assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
|
|
177 |
proof -
|
|
178 |
obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"
|
|
179 |
using cauchyD [OF assms zero_less_one] ..
|
|
180 |
show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
|
|
181 |
proof (intro exI conjI allI)
|
|
182 |
have "0 \<le> \<bar>X 0\<bar>" by simp
|
|
183 |
also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp
|
|
184 |
finally have "0 \<le> Max (abs ` X ` {..k})" .
|
|
185 |
thus "0 < Max (abs ` X ` {..k}) + 1" by simp
|
|
186 |
next
|
|
187 |
fix n :: nat
|
|
188 |
show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"
|
|
189 |
proof (rule linorder_le_cases)
|
|
190 |
assume "n \<le> k"
|
|
191 |
hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
|
|
192 |
thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
|
|
193 |
next
|
|
194 |
assume "k \<le> n"
|
|
195 |
have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp
|
|
196 |
also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"
|
|
197 |
by (rule abs_triangle_ineq)
|
|
198 |
also have "\<dots> < Max (abs ` X ` {..k}) + 1"
|
|
199 |
by (rule add_le_less_mono, simp, simp add: k `k \<le> n`)
|
|
200 |
finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .
|
|
201 |
qed
|
|
202 |
qed
|
|
203 |
qed
|
|
204 |
|
|
205 |
lemma cauchy_mult [simp]:
|
|
206 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
207 |
shows "cauchy (\<lambda>n. X n * Y n)"
|
|
208 |
proof (rule cauchyI)
|
|
209 |
fix r :: rat assume "0 < r"
|
|
210 |
then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
|
|
211 |
by (rule obtain_pos_sum)
|
|
212 |
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
|
|
213 |
using cauchy_imp_bounded [OF X] by fast
|
|
214 |
obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
|
|
215 |
using cauchy_imp_bounded [OF Y] by fast
|
|
216 |
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
|
|
217 |
proof
|
|
218 |
show "0 < v/b" using v b(1) by (rule divide_pos_pos)
|
|
219 |
show "0 < u/a" using u a(1) by (rule divide_pos_pos)
|
|
220 |
show "r = a * (u/a) + (v/b) * b"
|
|
221 |
using a(1) b(1) `r = u + v` by simp
|
|
222 |
qed
|
|
223 |
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
|
|
224 |
using cauchyD [OF X s] ..
|
|
225 |
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
|
|
226 |
using cauchyD [OF Y t] ..
|
|
227 |
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"
|
|
228 |
proof (clarsimp)
|
|
229 |
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
|
|
230 |
have "\<bar>X m * Y m - X n * Y n\<bar> = \<bar>X m * (Y m - Y n) + (X m - X n) * Y n\<bar>"
|
|
231 |
unfolding mult_diff_mult ..
|
|
232 |
also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"
|
|
233 |
by (rule abs_triangle_ineq)
|
|
234 |
also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>"
|
|
235 |
unfolding abs_mult ..
|
|
236 |
also have "\<dots> < a * t + s * b"
|
|
237 |
by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
|
|
238 |
finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .
|
|
239 |
qed
|
|
240 |
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
|
|
241 |
qed
|
|
242 |
|
|
243 |
lemma cauchy_not_vanishes_cases:
|
|
244 |
assumes X: "cauchy X"
|
|
245 |
assumes nz: "\<not> vanishes X"
|
|
246 |
shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)"
|
|
247 |
proof -
|
|
248 |
obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>"
|
|
249 |
using nz unfolding vanishes_def by (auto simp add: not_less)
|
|
250 |
obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"
|
|
251 |
using `0 < r` by (rule obtain_pos_sum)
|
|
252 |
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
|
|
253 |
using cauchyD [OF X s] ..
|
|
254 |
obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
|
|
255 |
using r by fast
|
|
256 |
have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
|
|
257 |
using i `i \<le> k` by auto
|
|
258 |
have "X k \<le> - r \<or> r \<le> X k"
|
|
259 |
using `r \<le> \<bar>X k\<bar>` by auto
|
|
260 |
hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
|
|
261 |
unfolding `r = s + t` using k by auto
|
|
262 |
hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
|
|
263 |
thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
|
|
264 |
using t by auto
|
|
265 |
qed
|
|
266 |
|
|
267 |
lemma cauchy_not_vanishes:
|
|
268 |
assumes X: "cauchy X"
|
|
269 |
assumes nz: "\<not> vanishes X"
|
|
270 |
shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
|
|
271 |
using cauchy_not_vanishes_cases [OF assms]
|
|
272 |
by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)
|
|
273 |
|
|
274 |
lemma cauchy_inverse [simp]:
|
|
275 |
assumes X: "cauchy X"
|
|
276 |
assumes nz: "\<not> vanishes X"
|
|
277 |
shows "cauchy (\<lambda>n. inverse (X n))"
|
|
278 |
proof (rule cauchyI)
|
|
279 |
fix r :: rat assume "0 < r"
|
|
280 |
obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
|
|
281 |
using cauchy_not_vanishes [OF X nz] by fast
|
|
282 |
from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
|
|
283 |
obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
|
|
284 |
proof
|
|
285 |
show "0 < b * r * b"
|
|
286 |
by (simp add: `0 < r` b mult_pos_pos)
|
|
287 |
show "r = inverse b * (b * r * b) * inverse b"
|
|
288 |
using b by simp
|
|
289 |
qed
|
|
290 |
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"
|
|
291 |
using cauchyD [OF X s] ..
|
|
292 |
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"
|
|
293 |
proof (clarsimp)
|
|
294 |
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
|
|
295 |
have "\<bar>inverse (X m) - inverse (X n)\<bar> =
|
|
296 |
inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
|
|
297 |
by (simp add: inverse_diff_inverse nz * abs_mult)
|
|
298 |
also have "\<dots> < inverse b * s * inverse b"
|
|
299 |
by (simp add: mult_strict_mono less_imp_inverse_less
|
|
300 |
mult_pos_pos i j b * s)
|
|
301 |
finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
|
|
302 |
qed
|
|
303 |
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
|
|
304 |
qed
|
|
305 |
|
|
306 |
lemma vanishes_diff_inverse:
|
|
307 |
assumes X: "cauchy X" "\<not> vanishes X"
|
|
308 |
assumes Y: "cauchy Y" "\<not> vanishes Y"
|
|
309 |
assumes XY: "vanishes (\<lambda>n. X n - Y n)"
|
|
310 |
shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
|
|
311 |
proof (rule vanishesI)
|
|
312 |
fix r :: rat assume r: "0 < r"
|
|
313 |
obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
|
|
314 |
using cauchy_not_vanishes [OF X] by fast
|
|
315 |
obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
|
|
316 |
using cauchy_not_vanishes [OF Y] by fast
|
|
317 |
obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
|
|
318 |
proof
|
|
319 |
show "0 < a * r * b"
|
|
320 |
using a r b by (simp add: mult_pos_pos)
|
|
321 |
show "inverse a * (a * r * b) * inverse b = r"
|
|
322 |
using a r b by simp
|
|
323 |
qed
|
|
324 |
obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
|
|
325 |
using vanishesD [OF XY s] ..
|
|
326 |
have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
|
|
327 |
proof (clarsimp)
|
|
328 |
fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
|
|
329 |
have "X n \<noteq> 0" and "Y n \<noteq> 0"
|
|
330 |
using i j a b n by auto
|
|
331 |
hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
|
|
332 |
inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
|
|
333 |
by (simp add: inverse_diff_inverse abs_mult)
|
|
334 |
also have "\<dots> < inverse a * s * inverse b"
|
|
335 |
apply (intro mult_strict_mono' less_imp_inverse_less)
|
|
336 |
apply (simp_all add: a b i j k n mult_nonneg_nonneg)
|
|
337 |
done
|
|
338 |
also note `inverse a * s * inverse b = r`
|
|
339 |
finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
|
|
340 |
qed
|
|
341 |
thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
|
|
342 |
qed
|
|
343 |
|
|
344 |
subsection {* Equivalence relation on Cauchy sequences *}
|
|
345 |
|
|
346 |
definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool"
|
|
347 |
where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))"
|
|
348 |
|
|
349 |
lemma realrelI [intro?]:
|
|
350 |
assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n - Y n)"
|
|
351 |
shows "realrel X Y"
|
|
352 |
using assms unfolding realrel_def by simp
|
|
353 |
|
|
354 |
lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X"
|
|
355 |
unfolding realrel_def by simp
|
|
356 |
|
|
357 |
lemma symp_realrel: "symp realrel"
|
|
358 |
unfolding realrel_def
|
|
359 |
by (rule sympI, clarify, drule vanishes_minus, simp)
|
|
360 |
|
|
361 |
lemma transp_realrel: "transp realrel"
|
|
362 |
unfolding realrel_def
|
|
363 |
apply (rule transpI, clarify)
|
|
364 |
apply (drule (1) vanishes_add)
|
|
365 |
apply (simp add: algebra_simps)
|
|
366 |
done
|
|
367 |
|
|
368 |
lemma part_equivp_realrel: "part_equivp realrel"
|
|
369 |
by (fast intro: part_equivpI symp_realrel transp_realrel
|
|
370 |
realrel_refl cauchy_const)
|
|
371 |
|
|
372 |
subsection {* The field of real numbers *}
|
|
373 |
|
|
374 |
quotient_type real = "nat \<Rightarrow> rat" / partial: realrel
|
|
375 |
morphisms rep_real Real
|
|
376 |
by (rule part_equivp_realrel)
|
|
377 |
|
|
378 |
lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
|
|
379 |
unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
|
|
380 |
|
|
381 |
lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
|
|
382 |
assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
|
|
383 |
proof (induct x)
|
|
384 |
case (1 X)
|
|
385 |
hence "cauchy X" by (simp add: realrel_def)
|
|
386 |
thus "P (Real X)" by (rule assms)
|
|
387 |
qed
|
|
388 |
|
|
389 |
lemma eq_Real:
|
|
390 |
"cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
|
|
391 |
using real.rel_eq_transfer
|
|
392 |
unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
|
|
393 |
|
|
394 |
declare real.forall_transfer [transfer_rule del]
|
|
395 |
|
|
396 |
lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
|
|
397 |
"(fun_rel (fun_rel pcr_real op =) op =)
|
|
398 |
(transfer_bforall cauchy) transfer_forall"
|
|
399 |
using real.forall_transfer
|
|
400 |
by (simp add: realrel_def)
|
|
401 |
|
|
402 |
instantiation real :: field_inverse_zero
|
|
403 |
begin
|
|
404 |
|
|
405 |
lift_definition zero_real :: "real" is "\<lambda>n. 0"
|
|
406 |
by (simp add: realrel_refl)
|
|
407 |
|
|
408 |
lift_definition one_real :: "real" is "\<lambda>n. 1"
|
|
409 |
by (simp add: realrel_refl)
|
|
410 |
|
|
411 |
lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n + Y n"
|
|
412 |
unfolding realrel_def add_diff_add
|
|
413 |
by (simp only: cauchy_add vanishes_add simp_thms)
|
|
414 |
|
|
415 |
lift_definition uminus_real :: "real \<Rightarrow> real" is "\<lambda>X n. - X n"
|
|
416 |
unfolding realrel_def minus_diff_minus
|
|
417 |
by (simp only: cauchy_minus vanishes_minus simp_thms)
|
|
418 |
|
|
419 |
lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
|
|
420 |
unfolding realrel_def mult_diff_mult
|
|
421 |
by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add
|
|
422 |
vanishes_mult_bounded cauchy_imp_bounded simp_thms)
|
|
423 |
|
|
424 |
lift_definition inverse_real :: "real \<Rightarrow> real"
|
|
425 |
is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
|
|
426 |
proof -
|
|
427 |
fix X Y assume "realrel X Y"
|
|
428 |
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
|
|
429 |
unfolding realrel_def by simp_all
|
|
430 |
have "vanishes X \<longleftrightarrow> vanishes Y"
|
|
431 |
proof
|
|
432 |
assume "vanishes X"
|
|
433 |
from vanishes_diff [OF this XY] show "vanishes Y" by simp
|
|
434 |
next
|
|
435 |
assume "vanishes Y"
|
|
436 |
from vanishes_add [OF this XY] show "vanishes X" by simp
|
|
437 |
qed
|
|
438 |
thus "?thesis X Y"
|
|
439 |
unfolding realrel_def
|
|
440 |
by (simp add: vanishes_diff_inverse X Y XY)
|
|
441 |
qed
|
|
442 |
|
|
443 |
definition
|
|
444 |
"x - y = (x::real) + - y"
|
|
445 |
|
|
446 |
definition
|
|
447 |
"x / y = (x::real) * inverse y"
|
|
448 |
|
|
449 |
lemma add_Real:
|
|
450 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
451 |
shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
|
|
452 |
using assms plus_real.transfer
|
|
453 |
unfolding cr_real_eq fun_rel_def by simp
|
|
454 |
|
|
455 |
lemma minus_Real:
|
|
456 |
assumes X: "cauchy X"
|
|
457 |
shows "- Real X = Real (\<lambda>n. - X n)"
|
|
458 |
using assms uminus_real.transfer
|
|
459 |
unfolding cr_real_eq fun_rel_def by simp
|
|
460 |
|
|
461 |
lemma diff_Real:
|
|
462 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
463 |
shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
|
|
464 |
unfolding minus_real_def diff_minus
|
|
465 |
by (simp add: minus_Real add_Real X Y)
|
|
466 |
|
|
467 |
lemma mult_Real:
|
|
468 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
469 |
shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
|
|
470 |
using assms times_real.transfer
|
|
471 |
unfolding cr_real_eq fun_rel_def by simp
|
|
472 |
|
|
473 |
lemma inverse_Real:
|
|
474 |
assumes X: "cauchy X"
|
|
475 |
shows "inverse (Real X) =
|
|
476 |
(if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
|
|
477 |
using assms inverse_real.transfer zero_real.transfer
|
|
478 |
unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
|
|
479 |
|
|
480 |
instance proof
|
|
481 |
fix a b c :: real
|
|
482 |
show "a + b = b + a"
|
|
483 |
by transfer (simp add: add_ac realrel_def)
|
|
484 |
show "(a + b) + c = a + (b + c)"
|
|
485 |
by transfer (simp add: add_ac realrel_def)
|
|
486 |
show "0 + a = a"
|
|
487 |
by transfer (simp add: realrel_def)
|
|
488 |
show "- a + a = 0"
|
|
489 |
by transfer (simp add: realrel_def)
|
|
490 |
show "a - b = a + - b"
|
|
491 |
by (rule minus_real_def)
|
|
492 |
show "(a * b) * c = a * (b * c)"
|
|
493 |
by transfer (simp add: mult_ac realrel_def)
|
|
494 |
show "a * b = b * a"
|
|
495 |
by transfer (simp add: mult_ac realrel_def)
|
|
496 |
show "1 * a = a"
|
|
497 |
by transfer (simp add: mult_ac realrel_def)
|
|
498 |
show "(a + b) * c = a * c + b * c"
|
|
499 |
by transfer (simp add: distrib_right realrel_def)
|
|
500 |
show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
|
|
501 |
by transfer (simp add: realrel_def)
|
|
502 |
show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
|
|
503 |
apply transfer
|
|
504 |
apply (simp add: realrel_def)
|
|
505 |
apply (rule vanishesI)
|
|
506 |
apply (frule (1) cauchy_not_vanishes, clarify)
|
|
507 |
apply (rule_tac x=k in exI, clarify)
|
|
508 |
apply (drule_tac x=n in spec, simp)
|
|
509 |
done
|
|
510 |
show "a / b = a * inverse b"
|
|
511 |
by (rule divide_real_def)
|
|
512 |
show "inverse (0::real) = 0"
|
|
513 |
by transfer (simp add: realrel_def)
|
|
514 |
qed
|
|
515 |
|
|
516 |
end
|
|
517 |
|
|
518 |
subsection {* Positive reals *}
|
|
519 |
|
|
520 |
lift_definition positive :: "real \<Rightarrow> bool"
|
|
521 |
is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
|
|
522 |
proof -
|
|
523 |
{ fix X Y
|
|
524 |
assume "realrel X Y"
|
|
525 |
hence XY: "vanishes (\<lambda>n. X n - Y n)"
|
|
526 |
unfolding realrel_def by simp_all
|
|
527 |
assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
|
|
528 |
then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
|
|
529 |
by fast
|
|
530 |
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
|
|
531 |
using `0 < r` by (rule obtain_pos_sum)
|
|
532 |
obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
|
|
533 |
using vanishesD [OF XY s] ..
|
|
534 |
have "\<forall>n\<ge>max i j. t < Y n"
|
|
535 |
proof (clarsimp)
|
|
536 |
fix n assume n: "i \<le> n" "j \<le> n"
|
|
537 |
have "\<bar>X n - Y n\<bar> < s" and "r < X n"
|
|
538 |
using i j n by simp_all
|
|
539 |
thus "t < Y n" unfolding r by simp
|
|
540 |
qed
|
|
541 |
hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
|
|
542 |
} note 1 = this
|
|
543 |
fix X Y assume "realrel X Y"
|
|
544 |
hence "realrel X Y" and "realrel Y X"
|
|
545 |
using symp_realrel unfolding symp_def by auto
|
|
546 |
thus "?thesis X Y"
|
|
547 |
by (safe elim!: 1)
|
|
548 |
qed
|
|
549 |
|
|
550 |
lemma positive_Real:
|
|
551 |
assumes X: "cauchy X"
|
|
552 |
shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
|
|
553 |
using assms positive.transfer
|
|
554 |
unfolding cr_real_eq fun_rel_def by simp
|
|
555 |
|
|
556 |
lemma positive_zero: "\<not> positive 0"
|
|
557 |
by transfer auto
|
|
558 |
|
|
559 |
lemma positive_add:
|
|
560 |
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
|
|
561 |
apply transfer
|
|
562 |
apply (clarify, rename_tac a b i j)
|
|
563 |
apply (rule_tac x="a + b" in exI, simp)
|
|
564 |
apply (rule_tac x="max i j" in exI, clarsimp)
|
|
565 |
apply (simp add: add_strict_mono)
|
|
566 |
done
|
|
567 |
|
|
568 |
lemma positive_mult:
|
|
569 |
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
|
|
570 |
apply transfer
|
|
571 |
apply (clarify, rename_tac a b i j)
|
|
572 |
apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
|
|
573 |
apply (rule_tac x="max i j" in exI, clarsimp)
|
|
574 |
apply (rule mult_strict_mono, auto)
|
|
575 |
done
|
|
576 |
|
|
577 |
lemma positive_minus:
|
|
578 |
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
|
|
579 |
apply transfer
|
|
580 |
apply (simp add: realrel_def)
|
|
581 |
apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
|
|
582 |
done
|
|
583 |
|
|
584 |
instantiation real :: linordered_field_inverse_zero
|
|
585 |
begin
|
|
586 |
|
|
587 |
definition
|
|
588 |
"x < y \<longleftrightarrow> positive (y - x)"
|
|
589 |
|
|
590 |
definition
|
|
591 |
"x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
|
|
592 |
|
|
593 |
definition
|
|
594 |
"abs (a::real) = (if a < 0 then - a else a)"
|
|
595 |
|
|
596 |
definition
|
|
597 |
"sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
|
|
598 |
|
|
599 |
instance proof
|
|
600 |
fix a b c :: real
|
|
601 |
show "\<bar>a\<bar> = (if a < 0 then - a else a)"
|
|
602 |
by (rule abs_real_def)
|
|
603 |
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
|
|
604 |
unfolding less_eq_real_def less_real_def
|
|
605 |
by (auto, drule (1) positive_add, simp_all add: positive_zero)
|
|
606 |
show "a \<le> a"
|
|
607 |
unfolding less_eq_real_def by simp
|
|
608 |
show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
|
|
609 |
unfolding less_eq_real_def less_real_def
|
|
610 |
by (auto, drule (1) positive_add, simp add: algebra_simps)
|
|
611 |
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
|
|
612 |
unfolding less_eq_real_def less_real_def
|
|
613 |
by (auto, drule (1) positive_add, simp add: positive_zero)
|
|
614 |
show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
|
|
615 |
unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
|
|
616 |
(* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
|
|
617 |
(* Should produce c + b - (c + a) \<equiv> b - a *)
|
|
618 |
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
|
|
619 |
by (rule sgn_real_def)
|
|
620 |
show "a \<le> b \<or> b \<le> a"
|
|
621 |
unfolding less_eq_real_def less_real_def
|
|
622 |
by (auto dest!: positive_minus)
|
|
623 |
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
|
|
624 |
unfolding less_real_def
|
|
625 |
by (drule (1) positive_mult, simp add: algebra_simps)
|
|
626 |
qed
|
|
627 |
|
|
628 |
end
|
|
629 |
|
|
630 |
instantiation real :: distrib_lattice
|
|
631 |
begin
|
|
632 |
|
|
633 |
definition
|
|
634 |
"(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
|
|
635 |
|
|
636 |
definition
|
|
637 |
"(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
|
|
638 |
|
|
639 |
instance proof
|
|
640 |
qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
|
|
641 |
|
|
642 |
end
|
|
643 |
|
|
644 |
lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"
|
|
645 |
apply (induct x)
|
|
646 |
apply (simp add: zero_real_def)
|
|
647 |
apply (simp add: one_real_def add_Real)
|
|
648 |
done
|
|
649 |
|
|
650 |
lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"
|
|
651 |
apply (cases x rule: int_diff_cases)
|
|
652 |
apply (simp add: of_nat_Real diff_Real)
|
|
653 |
done
|
|
654 |
|
|
655 |
lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
|
|
656 |
apply (induct x)
|
|
657 |
apply (simp add: Fract_of_int_quotient of_rat_divide)
|
|
658 |
apply (simp add: of_int_Real divide_inverse)
|
|
659 |
apply (simp add: inverse_Real mult_Real)
|
|
660 |
done
|
|
661 |
|
|
662 |
instance real :: archimedean_field
|
|
663 |
proof
|
|
664 |
fix x :: real
|
|
665 |
show "\<exists>z. x \<le> of_int z"
|
|
666 |
apply (induct x)
|
|
667 |
apply (frule cauchy_imp_bounded, clarify)
|
|
668 |
apply (rule_tac x="ceiling b + 1" in exI)
|
|
669 |
apply (rule less_imp_le)
|
|
670 |
apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
|
|
671 |
apply (rule_tac x=1 in exI, simp add: algebra_simps)
|
|
672 |
apply (rule_tac x=0 in exI, clarsimp)
|
|
673 |
apply (rule le_less_trans [OF abs_ge_self])
|
|
674 |
apply (rule less_le_trans [OF _ le_of_int_ceiling])
|
|
675 |
apply simp
|
|
676 |
done
|
|
677 |
qed
|
|
678 |
|
|
679 |
instantiation real :: floor_ceiling
|
|
680 |
begin
|
|
681 |
|
|
682 |
definition [code del]:
|
|
683 |
"floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
|
|
684 |
|
|
685 |
instance proof
|
|
686 |
fix x :: real
|
|
687 |
show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
|
|
688 |
unfolding floor_real_def using floor_exists1 by (rule theI')
|
|
689 |
qed
|
|
690 |
|
|
691 |
end
|
|
692 |
|
|
693 |
subsection {* Completeness *}
|
|
694 |
|
|
695 |
lemma not_positive_Real:
|
|
696 |
assumes X: "cauchy X"
|
|
697 |
shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
|
|
698 |
unfolding positive_Real [OF X]
|
|
699 |
apply (auto, unfold not_less)
|
|
700 |
apply (erule obtain_pos_sum)
|
|
701 |
apply (drule_tac x=s in spec, simp)
|
|
702 |
apply (drule_tac r=t in cauchyD [OF X], clarify)
|
|
703 |
apply (drule_tac x=k in spec, clarsimp)
|
|
704 |
apply (rule_tac x=n in exI, clarify, rename_tac m)
|
|
705 |
apply (drule_tac x=m in spec, simp)
|
|
706 |
apply (drule_tac x=n in spec, simp)
|
|
707 |
apply (drule spec, drule (1) mp, clarify, rename_tac i)
|
|
708 |
apply (rule_tac x="max i k" in exI, simp)
|
|
709 |
done
|
|
710 |
|
|
711 |
lemma le_Real:
|
|
712 |
assumes X: "cauchy X" and Y: "cauchy Y"
|
|
713 |
shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
|
|
714 |
unfolding not_less [symmetric, where 'a=real] less_real_def
|
|
715 |
apply (simp add: diff_Real not_positive_Real X Y)
|
|
716 |
apply (simp add: diff_le_eq add_ac)
|
|
717 |
done
|
|
718 |
|
|
719 |
lemma le_RealI:
|
|
720 |
assumes Y: "cauchy Y"
|
|
721 |
shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"
|
|
722 |
proof (induct x)
|
|
723 |
fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
|
|
724 |
hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
|
|
725 |
by (simp add: of_rat_Real le_Real)
|
|
726 |
{
|
|
727 |
fix r :: rat assume "0 < r"
|
|
728 |
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
|
|
729 |
by (rule obtain_pos_sum)
|
|
730 |
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"
|
|
731 |
using cauchyD [OF Y s] ..
|
|
732 |
obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"
|
|
733 |
using le [OF t] ..
|
|
734 |
have "\<forall>n\<ge>max i j. X n \<le> Y n + r"
|
|
735 |
proof (clarsimp)
|
|
736 |
fix n assume n: "i \<le> n" "j \<le> n"
|
|
737 |
have "X n \<le> Y i + t" using n j by simp
|
|
738 |
moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
|
|
739 |
ultimately show "X n \<le> Y n + r" unfolding r by simp
|
|
740 |
qed
|
|
741 |
hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..
|
|
742 |
}
|
|
743 |
thus "Real X \<le> Real Y"
|
|
744 |
by (simp add: of_rat_Real le_Real X Y)
|
|
745 |
qed
|
|
746 |
|
|
747 |
lemma Real_leI:
|
|
748 |
assumes X: "cauchy X"
|
|
749 |
assumes le: "\<forall>n. of_rat (X n) \<le> y"
|
|
750 |
shows "Real X \<le> y"
|
|
751 |
proof -
|
|
752 |
have "- y \<le> - Real X"
|
|
753 |
by (simp add: minus_Real X le_RealI of_rat_minus le)
|
|
754 |
thus ?thesis by simp
|
|
755 |
qed
|
|
756 |
|
|
757 |
lemma less_RealD:
|
|
758 |
assumes Y: "cauchy Y"
|
|
759 |
shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
|
|
760 |
by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])
|
|
761 |
|
|
762 |
lemma of_nat_less_two_power:
|
|
763 |
"of_nat n < (2::'a::linordered_idom) ^ n"
|
|
764 |
apply (induct n)
|
|
765 |
apply simp
|
|
766 |
apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
|
|
767 |
apply (drule (1) add_le_less_mono, simp)
|
|
768 |
apply simp
|
|
769 |
done
|
|
770 |
|
|
771 |
lemma complete_real:
|
|
772 |
fixes S :: "real set"
|
|
773 |
assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z"
|
|
774 |
shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
|
|
775 |
proof -
|
|
776 |
obtain x where x: "x \<in> S" using assms(1) ..
|
|
777 |
obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..
|
|
778 |
|
|
779 |
def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
|
|
780 |
obtain a where a: "\<not> P a"
|
|
781 |
proof
|
|
782 |
have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
|
|
783 |
also have "x - 1 < x" by simp
|
|
784 |
finally have "of_int (floor (x - 1)) < x" .
|
|
785 |
hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
|
|
786 |
then show "\<not> P (of_int (floor (x - 1)))"
|
|
787 |
unfolding P_def of_rat_of_int_eq using x by fast
|
|
788 |
qed
|
|
789 |
obtain b where b: "P b"
|
|
790 |
proof
|
|
791 |
show "P (of_int (ceiling z))"
|
|
792 |
unfolding P_def of_rat_of_int_eq
|
|
793 |
proof
|
|
794 |
fix y assume "y \<in> S"
|
|
795 |
hence "y \<le> z" using z by simp
|
|
796 |
also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
|
|
797 |
finally show "y \<le> of_int (ceiling z)" .
|
|
798 |
qed
|
|
799 |
qed
|
|
800 |
|
|
801 |
def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"
|
|
802 |
def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"
|
|
803 |
def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"
|
|
804 |
def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"
|
|
805 |
def C \<equiv> "\<lambda>n. avg (A n) (B n)"
|
|
806 |
have A_0 [simp]: "A 0 = a" unfolding A_def by simp
|
|
807 |
have B_0 [simp]: "B 0 = b" unfolding B_def by simp
|
|
808 |
have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)"
|
|
809 |
unfolding A_def B_def C_def bisect_def split_def by simp
|
|
810 |
have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)"
|
|
811 |
unfolding A_def B_def C_def bisect_def split_def by simp
|
|
812 |
|
|
813 |
have width: "\<And>n. B n - A n = (b - a) / 2^n"
|
|
814 |
apply (simp add: eq_divide_eq)
|
|
815 |
apply (induct_tac n, simp)
|
|
816 |
apply (simp add: C_def avg_def algebra_simps)
|
|
817 |
done
|
|
818 |
|
|
819 |
have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
|
|
820 |
apply (simp add: divide_less_eq)
|
|
821 |
apply (subst mult_commute)
|
|
822 |
apply (frule_tac y=y in ex_less_of_nat_mult)
|
|
823 |
apply clarify
|
|
824 |
apply (rule_tac x=n in exI)
|
|
825 |
apply (erule less_trans)
|
|
826 |
apply (rule mult_strict_right_mono)
|
|
827 |
apply (rule le_less_trans [OF _ of_nat_less_two_power])
|
|
828 |
apply simp
|
|
829 |
apply assumption
|
|
830 |
done
|
|
831 |
|
|
832 |
have PA: "\<And>n. \<not> P (A n)"
|
|
833 |
by (induct_tac n, simp_all add: a)
|
|
834 |
have PB: "\<And>n. P (B n)"
|
|
835 |
by (induct_tac n, simp_all add: b)
|
|
836 |
have ab: "a < b"
|
|
837 |
using a b unfolding P_def
|
|
838 |
apply (clarsimp simp add: not_le)
|
|
839 |
apply (drule (1) bspec)
|
|
840 |
apply (drule (1) less_le_trans)
|
|
841 |
apply (simp add: of_rat_less)
|
|
842 |
done
|
|
843 |
have AB: "\<And>n. A n < B n"
|
|
844 |
by (induct_tac n, simp add: ab, simp add: C_def avg_def)
|
|
845 |
have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
|
|
846 |
apply (auto simp add: le_less [where 'a=nat])
|
|
847 |
apply (erule less_Suc_induct)
|
|
848 |
apply (clarsimp simp add: C_def avg_def)
|
|
849 |
apply (simp add: add_divide_distrib [symmetric])
|
|
850 |
apply (rule AB [THEN less_imp_le])
|
|
851 |
apply simp
|
|
852 |
done
|
|
853 |
have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
|
|
854 |
apply (auto simp add: le_less [where 'a=nat])
|
|
855 |
apply (erule less_Suc_induct)
|
|
856 |
apply (clarsimp simp add: C_def avg_def)
|
|
857 |
apply (simp add: add_divide_distrib [symmetric])
|
|
858 |
apply (rule AB [THEN less_imp_le])
|
|
859 |
apply simp
|
|
860 |
done
|
|
861 |
have cauchy_lemma:
|
|
862 |
"\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
|
|
863 |
apply (rule cauchyI)
|
|
864 |
apply (drule twos [where y="b - a"])
|
|
865 |
apply (erule exE)
|
|
866 |
apply (rule_tac x=n in exI, clarify, rename_tac i j)
|
|
867 |
apply (rule_tac y="B n - A n" in le_less_trans) defer
|
|
868 |
apply (simp add: width)
|
|
869 |
apply (drule_tac x=n in spec)
|
|
870 |
apply (frule_tac x=i in spec, drule (1) mp)
|
|
871 |
apply (frule_tac x=j in spec, drule (1) mp)
|
|
872 |
apply (frule A_mono, drule B_mono)
|
|
873 |
apply (frule A_mono, drule B_mono)
|
|
874 |
apply arith
|
|
875 |
done
|
|
876 |
have "cauchy A"
|
|
877 |
apply (rule cauchy_lemma [rule_format])
|
|
878 |
apply (simp add: A_mono)
|
|
879 |
apply (erule order_trans [OF less_imp_le [OF AB] B_mono])
|
|
880 |
done
|
|
881 |
have "cauchy B"
|
|
882 |
apply (rule cauchy_lemma [rule_format])
|
|
883 |
apply (simp add: B_mono)
|
|
884 |
apply (erule order_trans [OF A_mono less_imp_le [OF AB]])
|
|
885 |
done
|
|
886 |
have 1: "\<forall>x\<in>S. x \<le> Real B"
|
|
887 |
proof
|
|
888 |
fix x assume "x \<in> S"
|
|
889 |
then show "x \<le> Real B"
|
|
890 |
using PB [unfolded P_def] `cauchy B`
|
|
891 |
by (simp add: le_RealI)
|
|
892 |
qed
|
|
893 |
have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
|
|
894 |
apply clarify
|
|
895 |
apply (erule contrapos_pp)
|
|
896 |
apply (simp add: not_le)
|
|
897 |
apply (drule less_RealD [OF `cauchy A`], clarify)
|
|
898 |
apply (subgoal_tac "\<not> P (A n)")
|
|
899 |
apply (simp add: P_def not_le, clarify)
|
|
900 |
apply (erule rev_bexI)
|
|
901 |
apply (erule (1) less_trans)
|
|
902 |
apply (simp add: PA)
|
|
903 |
done
|
|
904 |
have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
|
|
905 |
proof (rule vanishesI)
|
|
906 |
fix r :: rat assume "0 < r"
|
|
907 |
then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
|
|
908 |
using twos by fast
|
|
909 |
have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
|
|
910 |
proof (clarify)
|
|
911 |
fix n assume n: "k \<le> n"
|
|
912 |
have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
|
|
913 |
by simp
|
|
914 |
also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
|
|
915 |
using n by (simp add: divide_left_mono mult_pos_pos)
|
|
916 |
also note k
|
|
917 |
finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
|
|
918 |
qed
|
|
919 |
thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
|
|
920 |
qed
|
|
921 |
hence 3: "Real B = Real A"
|
|
922 |
by (simp add: eq_Real `cauchy A` `cauchy B` width)
|
|
923 |
show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
|
|
924 |
using 1 2 3 by (rule_tac x="Real B" in exI, simp)
|
|
925 |
qed
|
|
926 |
|
|
927 |
|
|
928 |
instantiation real :: conditional_complete_linorder
|
|
929 |
begin
|
|
930 |
|
|
931 |
subsection{*Supremum of a set of reals*}
|
|
932 |
|
|
933 |
definition
|
|
934 |
Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
|
|
935 |
|
|
936 |
definition
|
|
937 |
Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
|
|
938 |
|
|
939 |
instance
|
|
940 |
proof
|
|
941 |
{ fix z x :: real and X :: "real set"
|
|
942 |
assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
|
|
943 |
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
|
|
944 |
using complete_real[of X] by blast
|
|
945 |
then show "x \<le> Sup X"
|
|
946 |
unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
|
|
947 |
note Sup_upper = this
|
|
948 |
|
|
949 |
{ fix z :: real and X :: "real set"
|
|
950 |
assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
|
|
951 |
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
|
|
952 |
using complete_real[of X] by blast
|
|
953 |
then have "Sup X = s"
|
|
954 |
unfolding Sup_real_def by (best intro: Least_equality)
|
|
955 |
also with s z have "... \<le> z"
|
|
956 |
by blast
|
|
957 |
finally show "Sup X \<le> z" . }
|
|
958 |
note Sup_least = this
|
|
959 |
|
|
960 |
{ fix x z :: real and X :: "real set"
|
|
961 |
assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
|
|
962 |
have "-x \<le> Sup (uminus ` X)"
|
|
963 |
by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
|
|
964 |
then show "Inf X \<le> x"
|
|
965 |
by (auto simp add: Inf_real_def) }
|
|
966 |
|
|
967 |
{ fix z :: real and X :: "real set"
|
|
968 |
assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
|
|
969 |
have "Sup (uminus ` X) \<le> -z"
|
|
970 |
using x z by (force intro: Sup_least)
|
|
971 |
then show "z \<le> Inf X"
|
|
972 |
by (auto simp add: Inf_real_def) }
|
|
973 |
qed
|
|
974 |
end
|
|
975 |
|
|
976 |
text {*
|
|
977 |
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
|
|
978 |
*}
|
|
979 |
|
|
980 |
lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
|
|
981 |
by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
|
|
982 |
|
|
983 |
|
|
984 |
subsection {* Hiding implementation details *}
|
|
985 |
|
|
986 |
hide_const (open) vanishes cauchy positive Real
|
|
987 |
|
|
988 |
declare Real_induct [induct del]
|
|
989 |
declare Abs_real_induct [induct del]
|
|
990 |
declare Abs_real_cases [cases del]
|
|
991 |
|
|
992 |
lemmas [transfer_rule del] =
|
|
993 |
real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
|
|
994 |
zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
|
|
995 |
times_real.transfer inverse_real.transfer positive.transfer real.right_unique
|
|
996 |
real.right_total
|
|
997 |
|
|
998 |
subsection{*More Lemmas*}
|
|
999 |
|
|
1000 |
text {* BH: These lemmas should not be necessary; they should be
|
|
1001 |
covered by existing simp rules and simplification procedures. *}
|
|
1002 |
|
|
1003 |
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
|
|
1004 |
by simp (* redundant with mult_cancel_left *)
|
|
1005 |
|
|
1006 |
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
|
|
1007 |
by simp (* redundant with mult_cancel_right *)
|
|
1008 |
|
|
1009 |
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
|
|
1010 |
by simp (* solved by linordered_ring_less_cancel_factor simproc *)
|
|
1011 |
|
|
1012 |
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
|
|
1013 |
by simp (* solved by linordered_ring_le_cancel_factor simproc *)
|
|
1014 |
|
|
1015 |
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
|
|
1016 |
by simp (* solved by linordered_ring_le_cancel_factor simproc *)
|
|
1017 |
|
|
1018 |
|
|
1019 |
subsection {* Embedding numbers into the Reals *}
|
|
1020 |
|
|
1021 |
abbreviation
|
|
1022 |
real_of_nat :: "nat \<Rightarrow> real"
|
|
1023 |
where
|
|
1024 |
"real_of_nat \<equiv> of_nat"
|
|
1025 |
|
|
1026 |
abbreviation
|
|
1027 |
real_of_int :: "int \<Rightarrow> real"
|
|
1028 |
where
|
|
1029 |
"real_of_int \<equiv> of_int"
|
|
1030 |
|
|
1031 |
abbreviation
|
|
1032 |
real_of_rat :: "rat \<Rightarrow> real"
|
|
1033 |
where
|
|
1034 |
"real_of_rat \<equiv> of_rat"
|
|
1035 |
|
|
1036 |
consts
|
|
1037 |
(*overloaded constant for injecting other types into "real"*)
|
|
1038 |
real :: "'a => real"
|
|
1039 |
|
|
1040 |
defs (overloaded)
|
|
1041 |
real_of_nat_def [code_unfold]: "real == real_of_nat"
|
|
1042 |
real_of_int_def [code_unfold]: "real == real_of_int"
|
|
1043 |
|
|
1044 |
declare [[coercion_enabled]]
|
|
1045 |
declare [[coercion "real::nat\<Rightarrow>real"]]
|
|
1046 |
declare [[coercion "real::int\<Rightarrow>real"]]
|
|
1047 |
declare [[coercion "int"]]
|
|
1048 |
|
|
1049 |
declare [[coercion_map map]]
|
|
1050 |
declare [[coercion_map "% f g h x. g (h (f x))"]]
|
|
1051 |
declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
|
|
1052 |
|
|
1053 |
lemma real_eq_of_nat: "real = of_nat"
|
|
1054 |
unfolding real_of_nat_def ..
|
|
1055 |
|
|
1056 |
lemma real_eq_of_int: "real = of_int"
|
|
1057 |
unfolding real_of_int_def ..
|
|
1058 |
|
|
1059 |
lemma real_of_int_zero [simp]: "real (0::int) = 0"
|
|
1060 |
by (simp add: real_of_int_def)
|
|
1061 |
|
|
1062 |
lemma real_of_one [simp]: "real (1::int) = (1::real)"
|
|
1063 |
by (simp add: real_of_int_def)
|
|
1064 |
|
|
1065 |
lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
|
|
1066 |
by (simp add: real_of_int_def)
|
|
1067 |
|
|
1068 |
lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
|
|
1069 |
by (simp add: real_of_int_def)
|
|
1070 |
|
|
1071 |
lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
|
|
1072 |
by (simp add: real_of_int_def)
|
|
1073 |
|
|
1074 |
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
|
|
1075 |
by (simp add: real_of_int_def)
|
|
1076 |
|
|
1077 |
lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
|
|
1078 |
by (simp add: real_of_int_def of_int_power)
|
|
1079 |
|
|
1080 |
lemmas power_real_of_int = real_of_int_power [symmetric]
|
|
1081 |
|
|
1082 |
lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
|
|
1083 |
apply (subst real_eq_of_int)+
|
|
1084 |
apply (rule of_int_setsum)
|
|
1085 |
done
|
|
1086 |
|
|
1087 |
lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
|
|
1088 |
(PROD x:A. real(f x))"
|
|
1089 |
apply (subst real_eq_of_int)+
|
|
1090 |
apply (rule of_int_setprod)
|
|
1091 |
done
|
|
1092 |
|
|
1093 |
lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
|
|
1094 |
by (simp add: real_of_int_def)
|
|
1095 |
|
|
1096 |
lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
|
|
1097 |
by (simp add: real_of_int_def)
|
|
1098 |
|
|
1099 |
lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
|
|
1100 |
by (simp add: real_of_int_def)
|
|
1101 |
|
|
1102 |
lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
|
|
1103 |
by (simp add: real_of_int_def)
|
|
1104 |
|
|
1105 |
lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
|
|
1106 |
by (simp add: real_of_int_def)
|
|
1107 |
|
|
1108 |
lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
|
|
1109 |
by (simp add: real_of_int_def)
|
|
1110 |
|
|
1111 |
lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
|
|
1112 |
by (simp add: real_of_int_def)
|
|
1113 |
|
|
1114 |
lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
|
|
1115 |
by (simp add: real_of_int_def)
|
|
1116 |
|
|
1117 |
lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) \<longleftrightarrow> 1 < i"
|
|
1118 |
unfolding real_of_one[symmetric] real_of_int_less_iff ..
|
|
1119 |
|
|
1120 |
lemma one_le_real_of_int_cancel_iff: "1 \<le> real (i :: int) \<longleftrightarrow> 1 \<le> i"
|
|
1121 |
unfolding real_of_one[symmetric] real_of_int_le_iff ..
|
|
1122 |
|
|
1123 |
lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 \<longleftrightarrow> i < 1"
|
|
1124 |
unfolding real_of_one[symmetric] real_of_int_less_iff ..
|
|
1125 |
|
|
1126 |
lemma real_of_int_le_one_cancel_iff: "real (i :: int) \<le> 1 \<longleftrightarrow> i \<le> 1"
|
|
1127 |
unfolding real_of_one[symmetric] real_of_int_le_iff ..
|
|
1128 |
|
|
1129 |
lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
|
|
1130 |
by (auto simp add: abs_if)
|
|
1131 |
|
|
1132 |
lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
|
|
1133 |
apply (subgoal_tac "real n + 1 = real (n + 1)")
|
|
1134 |
apply (simp del: real_of_int_add)
|
|
1135 |
apply auto
|
|
1136 |
done
|
|
1137 |
|
|
1138 |
lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
|
|
1139 |
apply (subgoal_tac "real m + 1 = real (m + 1)")
|
|
1140 |
apply (simp del: real_of_int_add)
|
|
1141 |
apply simp
|
|
1142 |
done
|
|
1143 |
|
|
1144 |
lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
|
|
1145 |
real (x div d) + (real (x mod d)) / (real d)"
|
|
1146 |
proof -
|
|
1147 |
have "x = (x div d) * d + x mod d"
|
|
1148 |
by auto
|
|
1149 |
then have "real x = real (x div d) * real d + real(x mod d)"
|
|
1150 |
by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
|
|
1151 |
then have "real x / real d = ... / real d"
|
|
1152 |
by simp
|
|
1153 |
then show ?thesis
|
|
1154 |
by (auto simp add: add_divide_distrib algebra_simps)
|
|
1155 |
qed
|
|
1156 |
|
|
1157 |
lemma real_of_int_div: "(d :: int) dvd n ==>
|
|
1158 |
real(n div d) = real n / real d"
|
|
1159 |
apply (subst real_of_int_div_aux)
|
|
1160 |
apply simp
|
|
1161 |
apply (simp add: dvd_eq_mod_eq_0)
|
|
1162 |
done
|
|
1163 |
|
|
1164 |
lemma real_of_int_div2:
|
|
1165 |
"0 <= real (n::int) / real (x) - real (n div x)"
|
|
1166 |
apply (case_tac "x = 0")
|
|
1167 |
apply simp
|
|
1168 |
apply (case_tac "0 < x")
|
|
1169 |
apply (simp add: algebra_simps)
|
|
1170 |
apply (subst real_of_int_div_aux)
|
|
1171 |
apply simp
|
|
1172 |
apply (subst zero_le_divide_iff)
|
|
1173 |
apply auto
|
|
1174 |
apply (simp add: algebra_simps)
|
|
1175 |
apply (subst real_of_int_div_aux)
|
|
1176 |
apply simp
|
|
1177 |
apply (subst zero_le_divide_iff)
|
|
1178 |
apply auto
|
|
1179 |
done
|
|
1180 |
|
|
1181 |
lemma real_of_int_div3:
|
|
1182 |
"real (n::int) / real (x) - real (n div x) <= 1"
|
|
1183 |
apply (simp add: algebra_simps)
|
|
1184 |
apply (subst real_of_int_div_aux)
|
|
1185 |
apply (auto simp add: divide_le_eq intro: order_less_imp_le)
|
|
1186 |
done
|
|
1187 |
|
|
1188 |
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
|
|
1189 |
by (insert real_of_int_div2 [of n x], simp)
|
|
1190 |
|
|
1191 |
lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
|
|
1192 |
unfolding real_of_int_def by (rule Ints_of_int)
|
|
1193 |
|
|
1194 |
|
|
1195 |
subsection{*Embedding the Naturals into the Reals*}
|
|
1196 |
|
|
1197 |
lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
|
|
1198 |
by (simp add: real_of_nat_def)
|
|
1199 |
|
|
1200 |
lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
|
|
1201 |
by (simp add: real_of_nat_def)
|
|
1202 |
|
|
1203 |
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
|
|
1204 |
by (simp add: real_of_nat_def)
|
|
1205 |
|
|
1206 |
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
|
|
1207 |
by (simp add: real_of_nat_def)
|
|
1208 |
|
|
1209 |
(*Not for addsimps: often the LHS is used to represent a positive natural*)
|
|
1210 |
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
|
|
1211 |
by (simp add: real_of_nat_def)
|
|
1212 |
|
|
1213 |
lemma real_of_nat_less_iff [iff]:
|
|
1214 |
"(real (n::nat) < real m) = (n < m)"
|
|
1215 |
by (simp add: real_of_nat_def)
|
|
1216 |
|
|
1217 |
lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
|
|
1218 |
by (simp add: real_of_nat_def)
|
|
1219 |
|
|
1220 |
lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
|
|
1221 |
by (simp add: real_of_nat_def)
|
|
1222 |
|
|
1223 |
lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
|
|
1224 |
by (simp add: real_of_nat_def del: of_nat_Suc)
|
|
1225 |
|
|
1226 |
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
|
|
1227 |
by (simp add: real_of_nat_def of_nat_mult)
|
|
1228 |
|
|
1229 |
lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
|
|
1230 |
by (simp add: real_of_nat_def of_nat_power)
|
|
1231 |
|
|
1232 |
lemmas power_real_of_nat = real_of_nat_power [symmetric]
|
|
1233 |
|
|
1234 |
lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
|
|
1235 |
(SUM x:A. real(f x))"
|
|
1236 |
apply (subst real_eq_of_nat)+
|
|
1237 |
apply (rule of_nat_setsum)
|
|
1238 |
done
|
|
1239 |
|
|
1240 |
lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
|
|
1241 |
(PROD x:A. real(f x))"
|
|
1242 |
apply (subst real_eq_of_nat)+
|
|
1243 |
apply (rule of_nat_setprod)
|
|
1244 |
done
|
|
1245 |
|
|
1246 |
lemma real_of_card: "real (card A) = setsum (%x.1) A"
|
|
1247 |
apply (subst card_eq_setsum)
|
|
1248 |
apply (subst real_of_nat_setsum)
|
|
1249 |
apply simp
|
|
1250 |
done
|
|
1251 |
|
|
1252 |
lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
|
|
1253 |
by (simp add: real_of_nat_def)
|
|
1254 |
|
|
1255 |
lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)"
|
|
1256 |
by (simp add: real_of_nat_def)
|
|
1257 |
|
|
1258 |
lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
|
|
1259 |
by (simp add: add: real_of_nat_def of_nat_diff)
|
|
1260 |
|
|
1261 |
lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
|
|
1262 |
by (auto simp: real_of_nat_def)
|
|
1263 |
|
|
1264 |
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
|
|
1265 |
by (simp add: add: real_of_nat_def)
|
|
1266 |
|
|
1267 |
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
|
|
1268 |
by (simp add: add: real_of_nat_def)
|
|
1269 |
|
|
1270 |
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
|
|
1271 |
apply (subgoal_tac "real n + 1 = real (Suc n)")
|
|
1272 |
apply simp
|
|
1273 |
apply (auto simp add: real_of_nat_Suc)
|
|
1274 |
done
|
|
1275 |
|
|
1276 |
lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
|
|
1277 |
apply (subgoal_tac "real m + 1 = real (Suc m)")
|
|
1278 |
apply (simp add: less_Suc_eq_le)
|
|
1279 |
apply (simp add: real_of_nat_Suc)
|
|
1280 |
done
|
|
1281 |
|
|
1282 |
lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
|
|
1283 |
real (x div d) + (real (x mod d)) / (real d)"
|
|
1284 |
proof -
|
|
1285 |
have "x = (x div d) * d + x mod d"
|
|
1286 |
by auto
|
|
1287 |
then have "real x = real (x div d) * real d + real(x mod d)"
|
|
1288 |
by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])
|
|
1289 |
then have "real x / real d = \<dots> / real d"
|
|
1290 |
by simp
|
|
1291 |
then show ?thesis
|
|
1292 |
by (auto simp add: add_divide_distrib algebra_simps)
|
|
1293 |
qed
|
|
1294 |
|
|
1295 |
lemma real_of_nat_div: "(d :: nat) dvd n ==>
|
|
1296 |
real(n div d) = real n / real d"
|
|
1297 |
by (subst real_of_nat_div_aux)
|
|
1298 |
(auto simp add: dvd_eq_mod_eq_0 [symmetric])
|
|
1299 |
|
|
1300 |
lemma real_of_nat_div2:
|
|
1301 |
"0 <= real (n::nat) / real (x) - real (n div x)"
|
|
1302 |
apply (simp add: algebra_simps)
|
|
1303 |
apply (subst real_of_nat_div_aux)
|
|
1304 |
apply simp
|
|
1305 |
apply (subst zero_le_divide_iff)
|
|
1306 |
apply simp
|
|
1307 |
done
|
|
1308 |
|
|
1309 |
lemma real_of_nat_div3:
|
|
1310 |
"real (n::nat) / real (x) - real (n div x) <= 1"
|
|
1311 |
apply(case_tac "x = 0")
|
|
1312 |
apply (simp)
|
|
1313 |
apply (simp add: algebra_simps)
|
|
1314 |
apply (subst real_of_nat_div_aux)
|
|
1315 |
apply simp
|
|
1316 |
done
|
|
1317 |
|
|
1318 |
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
|
|
1319 |
by (insert real_of_nat_div2 [of n x], simp)
|
|
1320 |
|
|
1321 |
lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
|
|
1322 |
by (simp add: real_of_int_def real_of_nat_def)
|
|
1323 |
|
|
1324 |
lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
|
|
1325 |
apply (subgoal_tac "real(int(nat x)) = real(nat x)")
|
|
1326 |
apply force
|
|
1327 |
apply (simp only: real_of_int_of_nat_eq)
|
|
1328 |
done
|
|
1329 |
|
|
1330 |
lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
|
|
1331 |
unfolding real_of_nat_def by (rule of_nat_in_Nats)
|
|
1332 |
|
|
1333 |
lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
|
|
1334 |
unfolding real_of_nat_def by (rule Ints_of_nat)
|
|
1335 |
|
|
1336 |
subsection {* The Archimedean Property of the Reals *}
|
|
1337 |
|
|
1338 |
theorem reals_Archimedean:
|
|
1339 |
assumes x_pos: "0 < x"
|
|
1340 |
shows "\<exists>n. inverse (real (Suc n)) < x"
|
|
1341 |
unfolding real_of_nat_def using x_pos
|
|
1342 |
by (rule ex_inverse_of_nat_Suc_less)
|
|
1343 |
|
|
1344 |
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
|
|
1345 |
unfolding real_of_nat_def by (rule ex_less_of_nat)
|
|
1346 |
|
|
1347 |
lemma reals_Archimedean3:
|
|
1348 |
assumes x_greater_zero: "0 < x"
|
|
1349 |
shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
|
|
1350 |
unfolding real_of_nat_def using `0 < x`
|
|
1351 |
by (auto intro: ex_less_of_nat_mult)
|
|
1352 |
|
|
1353 |
|
|
1354 |
subsection{* Rationals *}
|
|
1355 |
|
|
1356 |
lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
|
|
1357 |
by (simp add: real_eq_of_nat)
|
|
1358 |
|
|
1359 |
|
|
1360 |
lemma Rats_eq_int_div_int:
|
|
1361 |
"\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
|
|
1362 |
proof
|
|
1363 |
show "\<rat> \<subseteq> ?S"
|
|
1364 |
proof
|
|
1365 |
fix x::real assume "x : \<rat>"
|
|
1366 |
then obtain r where "x = of_rat r" unfolding Rats_def ..
|
|
1367 |
have "of_rat r : ?S"
|
|
1368 |
by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
|
|
1369 |
thus "x : ?S" using `x = of_rat r` by simp
|
|
1370 |
qed
|
|
1371 |
next
|
|
1372 |
show "?S \<subseteq> \<rat>"
|
|
1373 |
proof(auto simp:Rats_def)
|
|
1374 |
fix i j :: int assume "j \<noteq> 0"
|
|
1375 |
hence "real i / real j = of_rat(Fract i j)"
|
|
1376 |
by (simp add:of_rat_rat real_eq_of_int)
|
|
1377 |
thus "real i / real j \<in> range of_rat" by blast
|
|
1378 |
qed
|
|
1379 |
qed
|
|
1380 |
|
|
1381 |
lemma Rats_eq_int_div_nat:
|
|
1382 |
"\<rat> = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
|
|
1383 |
proof(auto simp:Rats_eq_int_div_int)
|
|
1384 |
fix i j::int assume "j \<noteq> 0"
|
|
1385 |
show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
|
|
1386 |
proof cases
|
|
1387 |
assume "j>0"
|
|
1388 |
hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
|
|
1389 |
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
|
|
1390 |
thus ?thesis by blast
|
|
1391 |
next
|
|
1392 |
assume "~ j>0"
|
|
1393 |
hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
|
|
1394 |
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
|
|
1395 |
thus ?thesis by blast
|
|
1396 |
qed
|
|
1397 |
next
|
|
1398 |
fix i::int and n::nat assume "0 < n"
|
|
1399 |
hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
|
|
1400 |
thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
|
|
1401 |
qed
|
|
1402 |
|
|
1403 |
lemma Rats_abs_nat_div_natE:
|
|
1404 |
assumes "x \<in> \<rat>"
|
|
1405 |
obtains m n :: nat
|
|
1406 |
where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
|
|
1407 |
proof -
|
|
1408 |
from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
|
|
1409 |
by(auto simp add: Rats_eq_int_div_nat)
|
|
1410 |
hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
|
|
1411 |
then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
|
|
1412 |
let ?gcd = "gcd m n"
|
|
1413 |
from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp
|
|
1414 |
let ?k = "m div ?gcd"
|
|
1415 |
let ?l = "n div ?gcd"
|
|
1416 |
let ?gcd' = "gcd ?k ?l"
|
|
1417 |
have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
|
|
1418 |
by (rule dvd_mult_div_cancel)
|
|
1419 |
have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
|
|
1420 |
by (rule dvd_mult_div_cancel)
|
|
1421 |
from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
|
|
1422 |
moreover
|
|
1423 |
have "\<bar>x\<bar> = real ?k / real ?l"
|
|
1424 |
proof -
|
|
1425 |
from gcd have "real ?k / real ?l =
|
|
1426 |
real (?gcd * ?k) / real (?gcd * ?l)" by simp
|
|
1427 |
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
|
|
1428 |
also from x_rat have "\<dots> = \<bar>x\<bar>" ..
|
|
1429 |
finally show ?thesis ..
|
|
1430 |
qed
|
|
1431 |
moreover
|
|
1432 |
have "?gcd' = 1"
|
|
1433 |
proof -
|
|
1434 |
have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
|
|
1435 |
by (rule gcd_mult_distrib_nat)
|
|
1436 |
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
|
|
1437 |
with gcd show ?thesis by auto
|
|
1438 |
qed
|
|
1439 |
ultimately show ?thesis ..
|
|
1440 |
qed
|
|
1441 |
|
|
1442 |
subsection{*Density of the Rational Reals in the Reals*}
|
|
1443 |
|
|
1444 |
text{* This density proof is due to Stefan Richter and was ported by TN. The
|
|
1445 |
original source is \emph{Real Analysis} by H.L. Royden.
|
|
1446 |
It employs the Archimedean property of the reals. *}
|
|
1447 |
|
|
1448 |
lemma Rats_dense_in_real:
|
|
1449 |
fixes x :: real
|
|
1450 |
assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
|
|
1451 |
proof -
|
|
1452 |
from `x<y` have "0 < y-x" by simp
|
|
1453 |
with reals_Archimedean obtain q::nat
|
|
1454 |
where q: "inverse (real q) < y-x" and "0 < q" by auto
|
|
1455 |
def p \<equiv> "ceiling (y * real q) - 1"
|
|
1456 |
def r \<equiv> "of_int p / real q"
|
|
1457 |
from q have "x < y - inverse (real q)" by simp
|
|
1458 |
also have "y - inverse (real q) \<le> r"
|
|
1459 |
unfolding r_def p_def
|
|
1460 |
by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
|
|
1461 |
finally have "x < r" .
|
|
1462 |
moreover have "r < y"
|
|
1463 |
unfolding r_def p_def
|
|
1464 |
by (simp add: divide_less_eq diff_less_eq `0 < q`
|
|
1465 |
less_ceiling_iff [symmetric])
|
|
1466 |
moreover from r_def have "r \<in> \<rat>" by simp
|
|
1467 |
ultimately show ?thesis by fast
|
|
1468 |
qed
|
|
1469 |
|
|
1470 |
|
|
1471 |
|
|
1472 |
subsection{*Numerals and Arithmetic*}
|
|
1473 |
|
|
1474 |
lemma [code_abbrev]:
|
|
1475 |
"real_of_int (numeral k) = numeral k"
|
|
1476 |
"real_of_int (neg_numeral k) = neg_numeral k"
|
|
1477 |
by simp_all
|
|
1478 |
|
|
1479 |
text{*Collapse applications of @{term real} to @{term number_of}*}
|
|
1480 |
lemma real_numeral [simp]:
|
|
1481 |
"real (numeral v :: int) = numeral v"
|
|
1482 |
"real (neg_numeral v :: int) = neg_numeral v"
|
|
1483 |
by (simp_all add: real_of_int_def)
|
|
1484 |
|
|
1485 |
lemma real_of_nat_numeral [simp]:
|
|
1486 |
"real (numeral v :: nat) = numeral v"
|
|
1487 |
by (simp add: real_of_nat_def)
|
|
1488 |
|
|
1489 |
declaration {*
|
|
1490 |
K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
|
|
1491 |
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
|
|
1492 |
#> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
|
|
1493 |
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
|
|
1494 |
#> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
|
|
1495 |
@{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
|
|
1496 |
@{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
|
|
1497 |
@{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
|
|
1498 |
@{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}]
|
|
1499 |
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"})
|
|
1500 |
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}))
|
|
1501 |
*}
|
|
1502 |
|
|
1503 |
|
|
1504 |
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
|
|
1505 |
|
|
1506 |
lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
|
|
1507 |
by arith
|
|
1508 |
|
|
1509 |
text {* FIXME: redundant with @{text add_eq_0_iff} below *}
|
|
1510 |
lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
|
|
1511 |
by auto
|
|
1512 |
|
|
1513 |
lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
|
|
1514 |
by auto
|
|
1515 |
|
|
1516 |
lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
|
|
1517 |
by auto
|
|
1518 |
|
|
1519 |
lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
|
|
1520 |
by auto
|
|
1521 |
|
|
1522 |
lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
|
|
1523 |
by auto
|
|
1524 |
|
|
1525 |
subsection {* Lemmas about powers *}
|
|
1526 |
|
|
1527 |
text {* FIXME: declare this in Rings.thy or not at all *}
|
|
1528 |
declare abs_mult_self [simp]
|
|
1529 |
|
|
1530 |
(* used by Import/HOL/real.imp *)
|
|
1531 |
lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
|
|
1532 |
by simp
|
|
1533 |
|
|
1534 |
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
|
|
1535 |
apply (induct "n")
|
|
1536 |
apply (auto simp add: real_of_nat_Suc)
|
|
1537 |
apply (subst mult_2)
|
|
1538 |
apply (erule add_less_le_mono)
|
|
1539 |
apply (rule two_realpow_ge_one)
|
|
1540 |
done
|
|
1541 |
|
|
1542 |
text {* TODO: no longer real-specific; rename and move elsewhere *}
|
|
1543 |
lemma realpow_Suc_le_self:
|
|
1544 |
fixes r :: "'a::linordered_semidom"
|
|
1545 |
shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
|
|
1546 |
by (insert power_decreasing [of 1 "Suc n" r], simp)
|
|
1547 |
|
|
1548 |
text {* TODO: no longer real-specific; rename and move elsewhere *}
|
|
1549 |
lemma realpow_minus_mult:
|
|
1550 |
fixes x :: "'a::monoid_mult"
|
|
1551 |
shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
|
|
1552 |
by (simp add: power_commutes split add: nat_diff_split)
|
|
1553 |
|
|
1554 |
text {* FIXME: declare this [simp] for all types, or not at all *}
|
|
1555 |
lemma real_two_squares_add_zero_iff [simp]:
|
|
1556 |
"(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
|
|
1557 |
by (rule sum_squares_eq_zero_iff)
|
|
1558 |
|
|
1559 |
text {* FIXME: declare this [simp] for all types, or not at all *}
|
|
1560 |
lemma realpow_two_sum_zero_iff [simp]:
|
|
1561 |
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
|
|
1562 |
by (rule sum_power2_eq_zero_iff)
|
|
1563 |
|
|
1564 |
lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
|
|
1565 |
by (rule_tac y = 0 in order_trans, auto)
|
|
1566 |
|
|
1567 |
lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
|
|
1568 |
by (auto simp add: power2_eq_square)
|
|
1569 |
|
|
1570 |
|
|
1571 |
lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
|
|
1572 |
"(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
|
|
1573 |
unfolding real_of_nat_le_iff[symmetric] by simp
|
|
1574 |
|
|
1575 |
lemma real_of_nat_le_numeral_power_cancel_iff[simp]:
|
|
1576 |
"real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
|
|
1577 |
unfolding real_of_nat_le_iff[symmetric] by simp
|
|
1578 |
|
|
1579 |
lemma numeral_power_le_real_of_int_cancel_iff[simp]:
|
|
1580 |
"(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
|
|
1581 |
unfolding real_of_int_le_iff[symmetric] by simp
|
|
1582 |
|
|
1583 |
lemma real_of_int_le_numeral_power_cancel_iff[simp]:
|
|
1584 |
"real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
|
|
1585 |
unfolding real_of_int_le_iff[symmetric] by simp
|
|
1586 |
|
|
1587 |
lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
|
|
1588 |
"(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
|
|
1589 |
unfolding real_of_int_le_iff[symmetric] by simp
|
|
1590 |
|
|
1591 |
lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
|
|
1592 |
"real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
|
|
1593 |
unfolding real_of_int_le_iff[symmetric] by simp
|
|
1594 |
|
|
1595 |
subsection{*Density of the Reals*}
|
|
1596 |
|
|
1597 |
lemma real_lbound_gt_zero:
|
|
1598 |
"[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
|
|
1599 |
apply (rule_tac x = " (min d1 d2) /2" in exI)
|
|
1600 |
apply (simp add: min_def)
|
|
1601 |
done
|
|
1602 |
|
|
1603 |
|
|
1604 |
text{*Similar results are proved in @{text Fields}*}
|
|
1605 |
lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
|
|
1606 |
by auto
|
|
1607 |
|
|
1608 |
lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
|
|
1609 |
by auto
|
|
1610 |
|
|
1611 |
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
|
|
1612 |
by simp
|
|
1613 |
|
|
1614 |
subsection{*Absolute Value Function for the Reals*}
|
|
1615 |
|
|
1616 |
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
|
|
1617 |
by (simp add: abs_if)
|
|
1618 |
|
|
1619 |
(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
|
|
1620 |
lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
|
|
1621 |
by (force simp add: abs_le_iff)
|
|
1622 |
|
|
1623 |
lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
|
|
1624 |
by (simp add: abs_if)
|
|
1625 |
|
|
1626 |
lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
|
|
1627 |
by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
|
|
1628 |
|
|
1629 |
lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
|
|
1630 |
by simp
|
|
1631 |
|
|
1632 |
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
|
|
1633 |
by simp
|
|
1634 |
|
|
1635 |
|
|
1636 |
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
|
|
1637 |
|
|
1638 |
(* FIXME: theorems for negative numerals *)
|
|
1639 |
lemma numeral_less_real_of_int_iff [simp]:
|
|
1640 |
"((numeral n) < real (m::int)) = (numeral n < m)"
|
|
1641 |
apply auto
|
|
1642 |
apply (rule real_of_int_less_iff [THEN iffD1])
|
|
1643 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
|
|
1644 |
done
|
|
1645 |
|
|
1646 |
lemma numeral_less_real_of_int_iff2 [simp]:
|
|
1647 |
"(real (m::int) < (numeral n)) = (m < numeral n)"
|
|
1648 |
apply auto
|
|
1649 |
apply (rule real_of_int_less_iff [THEN iffD1])
|
|
1650 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
|
|
1651 |
done
|
|
1652 |
|
|
1653 |
lemma numeral_le_real_of_int_iff [simp]:
|
|
1654 |
"((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
|
|
1655 |
by (simp add: linorder_not_less [symmetric])
|
|
1656 |
|
|
1657 |
lemma numeral_le_real_of_int_iff2 [simp]:
|
|
1658 |
"(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
|
|
1659 |
by (simp add: linorder_not_less [symmetric])
|
|
1660 |
|
|
1661 |
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
|
|
1662 |
unfolding real_of_nat_def by simp
|
|
1663 |
|
|
1664 |
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
|
|
1665 |
unfolding real_of_nat_def by (simp add: floor_minus)
|
|
1666 |
|
|
1667 |
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
|
|
1668 |
unfolding real_of_int_def by simp
|
|
1669 |
|
|
1670 |
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
|
|
1671 |
unfolding real_of_int_def by (simp add: floor_minus)
|
|
1672 |
|
|
1673 |
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
|
|
1674 |
unfolding real_of_int_def by (rule floor_exists)
|
|
1675 |
|
|
1676 |
lemma lemma_floor:
|
|
1677 |
assumes a1: "real m \<le> r" and a2: "r < real n + 1"
|
|
1678 |
shows "m \<le> (n::int)"
|
|
1679 |
proof -
|
|
1680 |
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
|
|
1681 |
also have "... = real (n + 1)" by simp
|
|
1682 |
finally have "m < n + 1" by (simp only: real_of_int_less_iff)
|
|
1683 |
thus ?thesis by arith
|
|
1684 |
qed
|
|
1685 |
|
|
1686 |
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
|
|
1687 |
unfolding real_of_int_def by (rule of_int_floor_le)
|
|
1688 |
|
|
1689 |
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
|
|
1690 |
by (auto intro: lemma_floor)
|
|
1691 |
|
|
1692 |
lemma real_of_int_floor_cancel [simp]:
|
|
1693 |
"(real (floor x) = x) = (\<exists>n::int. x = real n)"
|
|
1694 |
using floor_real_of_int by metis
|
|
1695 |
|
|
1696 |
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
|
|
1697 |
unfolding real_of_int_def using floor_unique [of n x] by simp
|
|
1698 |
|
|
1699 |
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
|
|
1700 |
unfolding real_of_int_def by (rule floor_unique)
|
|
1701 |
|
|
1702 |
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
|
|
1703 |
apply (rule inj_int [THEN injD])
|
|
1704 |
apply (simp add: real_of_nat_Suc)
|
|
1705 |
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
|
|
1706 |
done
|
|
1707 |
|
|
1708 |
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
|
|
1709 |
apply (drule order_le_imp_less_or_eq)
|
|
1710 |
apply (auto intro: floor_eq3)
|
|
1711 |
done
|
|
1712 |
|
|
1713 |
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
|
|
1714 |
unfolding real_of_int_def using floor_correct [of r] by simp
|
|
1715 |
|
|
1716 |
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
|
|
1717 |
unfolding real_of_int_def using floor_correct [of r] by simp
|
|
1718 |
|
|
1719 |
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
|
|
1720 |
unfolding real_of_int_def using floor_correct [of r] by simp
|
|
1721 |
|
|
1722 |
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
|
|
1723 |
unfolding real_of_int_def using floor_correct [of r] by simp
|
|
1724 |
|
|
1725 |
lemma le_floor: "real a <= x ==> a <= floor x"
|
|
1726 |
unfolding real_of_int_def by (simp add: le_floor_iff)
|
|
1727 |
|
|
1728 |
lemma real_le_floor: "a <= floor x ==> real a <= x"
|
|
1729 |
unfolding real_of_int_def by (simp add: le_floor_iff)
|
|
1730 |
|
|
1731 |
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
|
|
1732 |
unfolding real_of_int_def by (rule le_floor_iff)
|
|
1733 |
|
|
1734 |
lemma floor_less_eq: "(floor x < a) = (x < real a)"
|
|
1735 |
unfolding real_of_int_def by (rule floor_less_iff)
|
|
1736 |
|
|
1737 |
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
|
|
1738 |
unfolding real_of_int_def by (rule less_floor_iff)
|
|
1739 |
|
|
1740 |
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
|
|
1741 |
unfolding real_of_int_def by (rule floor_le_iff)
|
|
1742 |
|
|
1743 |
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
|
|
1744 |
unfolding real_of_int_def by (rule floor_add_of_int)
|
|
1745 |
|
|
1746 |
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
|
|
1747 |
unfolding real_of_int_def by (rule floor_diff_of_int)
|
|
1748 |
|
|
1749 |
lemma le_mult_floor:
|
|
1750 |
assumes "0 \<le> (a :: real)" and "0 \<le> b"
|
|
1751 |
shows "floor a * floor b \<le> floor (a * b)"
|
|
1752 |
proof -
|
|
1753 |
have "real (floor a) \<le> a"
|
|
1754 |
and "real (floor b) \<le> b" by auto
|
|
1755 |
hence "real (floor a * floor b) \<le> a * b"
|
|
1756 |
using assms by (auto intro!: mult_mono)
|
|
1757 |
also have "a * b < real (floor (a * b) + 1)" by auto
|
|
1758 |
finally show ?thesis unfolding real_of_int_less_iff by simp
|
|
1759 |
qed
|
|
1760 |
|
|
1761 |
lemma floor_divide_eq_div:
|
|
1762 |
"floor (real a / real b) = a div b"
|
|
1763 |
proof cases
|
|
1764 |
assume "b \<noteq> 0 \<or> b dvd a"
|
|
1765 |
with real_of_int_div3[of a b] show ?thesis
|
|
1766 |
by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
|
|
1767 |
(metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
|
|
1768 |
real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
|
|
1769 |
qed (auto simp: real_of_int_div)
|
|
1770 |
|
|
1771 |
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
|
|
1772 |
unfolding real_of_nat_def by simp
|
|
1773 |
|
|
1774 |
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
|
|
1775 |
unfolding real_of_int_def by (rule le_of_int_ceiling)
|
|
1776 |
|
|
1777 |
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
|
|
1778 |
unfolding real_of_int_def by simp
|
|
1779 |
|
|
1780 |
lemma real_of_int_ceiling_cancel [simp]:
|
|
1781 |
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
|
|
1782 |
using ceiling_real_of_int by metis
|
|
1783 |
|
|
1784 |
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
|
|
1785 |
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
|
|
1786 |
|
|
1787 |
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
|
|
1788 |
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
|
|
1789 |
|
|
1790 |
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n"
|
|
1791 |
unfolding real_of_int_def using ceiling_unique [of n x] by simp
|
|
1792 |
|
|
1793 |
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
|
|
1794 |
unfolding real_of_int_def using ceiling_correct [of r] by simp
|
|
1795 |
|
|
1796 |
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
|
|
1797 |
unfolding real_of_int_def using ceiling_correct [of r] by simp
|
|
1798 |
|
|
1799 |
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
|
|
1800 |
unfolding real_of_int_def by (simp add: ceiling_le_iff)
|
|
1801 |
|
|
1802 |
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
|
|
1803 |
unfolding real_of_int_def by (simp add: ceiling_le_iff)
|
|
1804 |
|
|
1805 |
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
|
|
1806 |
unfolding real_of_int_def by (rule ceiling_le_iff)
|
|
1807 |
|
|
1808 |
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
|
|
1809 |
unfolding real_of_int_def by (rule less_ceiling_iff)
|
|
1810 |
|
|
1811 |
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
|
|
1812 |
unfolding real_of_int_def by (rule ceiling_less_iff)
|
|
1813 |
|
|
1814 |
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
|
|
1815 |
unfolding real_of_int_def by (rule le_ceiling_iff)
|
|
1816 |
|
|
1817 |
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
|
|
1818 |
unfolding real_of_int_def by (rule ceiling_add_of_int)
|
|
1819 |
|
|
1820 |
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
|
|
1821 |
unfolding real_of_int_def by (rule ceiling_diff_of_int)
|
|
1822 |
|
|
1823 |
|
|
1824 |
subsubsection {* Versions for the natural numbers *}
|
|
1825 |
|
|
1826 |
definition
|
|
1827 |
natfloor :: "real => nat" where
|
|
1828 |
"natfloor x = nat(floor x)"
|
|
1829 |
|
|
1830 |
definition
|
|
1831 |
natceiling :: "real => nat" where
|
|
1832 |
"natceiling x = nat(ceiling x)"
|
|
1833 |
|
|
1834 |
lemma natfloor_zero [simp]: "natfloor 0 = 0"
|
|
1835 |
by (unfold natfloor_def, simp)
|
|
1836 |
|
|
1837 |
lemma natfloor_one [simp]: "natfloor 1 = 1"
|
|
1838 |
by (unfold natfloor_def, simp)
|
|
1839 |
|
|
1840 |
lemma zero_le_natfloor [simp]: "0 <= natfloor x"
|
|
1841 |
by (unfold natfloor_def, simp)
|
|
1842 |
|
|
1843 |
lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
|
|
1844 |
by (unfold natfloor_def, simp)
|
|
1845 |
|
|
1846 |
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
|
|
1847 |
by (unfold natfloor_def, simp)
|
|
1848 |
|
|
1849 |
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
|
|
1850 |
by (unfold natfloor_def, simp)
|
|
1851 |
|
|
1852 |
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
|
|
1853 |
unfolding natfloor_def by simp
|
|
1854 |
|
|
1855 |
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
|
|
1856 |
unfolding natfloor_def by (intro nat_mono floor_mono)
|
|
1857 |
|
|
1858 |
lemma le_natfloor: "real x <= a ==> x <= natfloor a"
|
|
1859 |
apply (unfold natfloor_def)
|
|
1860 |
apply (subst nat_int [THEN sym])
|
|
1861 |
apply (rule nat_mono)
|
|
1862 |
apply (rule le_floor)
|
|
1863 |
apply simp
|
|
1864 |
done
|
|
1865 |
|
|
1866 |
lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
|
|
1867 |
unfolding natfloor_def real_of_nat_def
|
|
1868 |
by (simp add: nat_less_iff floor_less_iff)
|
|
1869 |
|
|
1870 |
lemma less_natfloor:
|
|
1871 |
assumes "0 \<le> x" and "x < real (n :: nat)"
|
|
1872 |
shows "natfloor x < n"
|
|
1873 |
using assms by (simp add: natfloor_less_iff)
|
|
1874 |
|
|
1875 |
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
|
|
1876 |
apply (rule iffI)
|
|
1877 |
apply (rule order_trans)
|
|
1878 |
prefer 2
|
|
1879 |
apply (erule real_natfloor_le)
|
|
1880 |
apply (subst real_of_nat_le_iff)
|
|
1881 |
apply assumption
|
|
1882 |
apply (erule le_natfloor)
|
|
1883 |
done
|
|
1884 |
|
|
1885 |
lemma le_natfloor_eq_numeral [simp]:
|
|
1886 |
"~ neg((numeral n)::int) ==> 0 <= x ==>
|
|
1887 |
(numeral n <= natfloor x) = (numeral n <= x)"
|
|
1888 |
apply (subst le_natfloor_eq, assumption)
|
|
1889 |
apply simp
|
|
1890 |
done
|
|
1891 |
|
|
1892 |
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
|
|
1893 |
apply (case_tac "0 <= x")
|
|
1894 |
apply (subst le_natfloor_eq, assumption, simp)
|
|
1895 |
apply (rule iffI)
|
|
1896 |
apply (subgoal_tac "natfloor x <= natfloor 0")
|
|
1897 |
apply simp
|
|
1898 |
apply (rule natfloor_mono)
|
|
1899 |
apply simp
|
|
1900 |
apply simp
|
|
1901 |
done
|
|
1902 |
|
|
1903 |
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
|
|
1904 |
unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
|
|
1905 |
|
|
1906 |
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
|
|
1907 |
apply (case_tac "0 <= x")
|
|
1908 |
apply (unfold natfloor_def)
|
|
1909 |
apply simp
|
|
1910 |
apply simp_all
|
|
1911 |
done
|
|
1912 |
|
|
1913 |
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
|
|
1914 |
using real_natfloor_add_one_gt by (simp add: algebra_simps)
|
|
1915 |
|
|
1916 |
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
|
|
1917 |
apply (subgoal_tac "z < real(natfloor z) + 1")
|
|
1918 |
apply arith
|
|
1919 |
apply (rule real_natfloor_add_one_gt)
|
|
1920 |
done
|
|
1921 |
|
|
1922 |
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
|
|
1923 |
unfolding natfloor_def
|
|
1924 |
unfolding real_of_int_of_nat_eq [symmetric] floor_add
|
|
1925 |
by (simp add: nat_add_distrib)
|
|
1926 |
|
|
1927 |
lemma natfloor_add_numeral [simp]:
|
|
1928 |
"~neg ((numeral n)::int) ==> 0 <= x ==>
|
|
1929 |
natfloor (x + numeral n) = natfloor x + numeral n"
|
|
1930 |
by (simp add: natfloor_add [symmetric])
|
|
1931 |
|
|
1932 |
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
|
|
1933 |
by (simp add: natfloor_add [symmetric] del: One_nat_def)
|
|
1934 |
|
|
1935 |
lemma natfloor_subtract [simp]:
|
|
1936 |
"natfloor(x - real a) = natfloor x - a"
|
|
1937 |
unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
|
|
1938 |
by simp
|
|
1939 |
|
|
1940 |
lemma natfloor_div_nat:
|
|
1941 |
assumes "1 <= x" and "y > 0"
|
|
1942 |
shows "natfloor (x / real y) = natfloor x div y"
|
|
1943 |
proof (rule natfloor_eq)
|
|
1944 |
have "(natfloor x) div y * y \<le> natfloor x"
|
|
1945 |
by (rule add_leD1 [where k="natfloor x mod y"], simp)
|
|
1946 |
thus "real (natfloor x div y) \<le> x / real y"
|
|
1947 |
using assms by (simp add: le_divide_eq le_natfloor_eq)
|
|
1948 |
have "natfloor x < (natfloor x) div y * y + y"
|
|
1949 |
apply (subst mod_div_equality [symmetric])
|
|
1950 |
apply (rule add_strict_left_mono)
|
|
1951 |
apply (rule mod_less_divisor)
|
|
1952 |
apply fact
|
|
1953 |
done
|
|
1954 |
thus "x / real y < real (natfloor x div y) + 1"
|
|
1955 |
using assms
|
|
1956 |
by (simp add: divide_less_eq natfloor_less_iff distrib_right)
|
|
1957 |
qed
|
|
1958 |
|
|
1959 |
lemma le_mult_natfloor:
|
|
1960 |
shows "natfloor a * natfloor b \<le> natfloor (a * b)"
|
|
1961 |
by (cases "0 <= a & 0 <= b")
|
|
1962 |
(auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
|
|
1963 |
|
|
1964 |
lemma natceiling_zero [simp]: "natceiling 0 = 0"
|
|
1965 |
by (unfold natceiling_def, simp)
|
|
1966 |
|
|
1967 |
lemma natceiling_one [simp]: "natceiling 1 = 1"
|
|
1968 |
by (unfold natceiling_def, simp)
|
|
1969 |
|
|
1970 |
lemma zero_le_natceiling [simp]: "0 <= natceiling x"
|
|
1971 |
by (unfold natceiling_def, simp)
|
|
1972 |
|
|
1973 |
lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
|
|
1974 |
by (unfold natceiling_def, simp)
|
|
1975 |
|
|
1976 |
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
|
|
1977 |
by (unfold natceiling_def, simp)
|
|
1978 |
|
|
1979 |
lemma real_natceiling_ge: "x <= real(natceiling x)"
|
|
1980 |
unfolding natceiling_def by (cases "x < 0", simp_all)
|
|
1981 |
|
|
1982 |
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
|
|
1983 |
unfolding natceiling_def by simp
|
|
1984 |
|
|
1985 |
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
|
|
1986 |
unfolding natceiling_def by (intro nat_mono ceiling_mono)
|
|
1987 |
|
|
1988 |
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
|
|
1989 |
unfolding natceiling_def real_of_nat_def
|
|
1990 |
by (simp add: nat_le_iff ceiling_le_iff)
|
|
1991 |
|
|
1992 |
lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
|
|
1993 |
unfolding natceiling_def real_of_nat_def
|
|
1994 |
by (simp add: nat_le_iff ceiling_le_iff)
|
|
1995 |
|
|
1996 |
lemma natceiling_le_eq_numeral [simp]:
|
|
1997 |
"~ neg((numeral n)::int) ==>
|
|
1998 |
(natceiling x <= numeral n) = (x <= numeral n)"
|
|
1999 |
by (simp add: natceiling_le_eq)
|
|
2000 |
|
|
2001 |
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
|
|
2002 |
unfolding natceiling_def
|
|
2003 |
by (simp add: nat_le_iff ceiling_le_iff)
|
|
2004 |
|
|
2005 |
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
|
|
2006 |
unfolding natceiling_def
|
|
2007 |
by (simp add: ceiling_eq2 [where n="int n"])
|
|
2008 |
|
|
2009 |
lemma natceiling_add [simp]: "0 <= x ==>
|
|
2010 |
natceiling (x + real a) = natceiling x + a"
|
|
2011 |
unfolding natceiling_def
|
|
2012 |
unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
|
|
2013 |
by (simp add: nat_add_distrib)
|
|
2014 |
|
|
2015 |
lemma natceiling_add_numeral [simp]:
|
|
2016 |
"~ neg ((numeral n)::int) ==> 0 <= x ==>
|
|
2017 |
natceiling (x + numeral n) = natceiling x + numeral n"
|
|
2018 |
by (simp add: natceiling_add [symmetric])
|
|
2019 |
|
|
2020 |
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
|
|
2021 |
by (simp add: natceiling_add [symmetric] del: One_nat_def)
|
|
2022 |
|
|
2023 |
lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
|
|
2024 |
unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
|
|
2025 |
by simp
|
|
2026 |
|
|
2027 |
subsection {* Exponentiation with floor *}
|
|
2028 |
|
|
2029 |
lemma floor_power:
|
|
2030 |
assumes "x = real (floor x)"
|
|
2031 |
shows "floor (x ^ n) = floor x ^ n"
|
|
2032 |
proof -
|
|
2033 |
have *: "x ^ n = real (floor x ^ n)"
|
|
2034 |
using assms by (induct n arbitrary: x) simp_all
|
|
2035 |
show ?thesis unfolding real_of_int_inject[symmetric]
|
|
2036 |
unfolding * floor_real_of_int ..
|
|
2037 |
qed
|
|
2038 |
|
|
2039 |
lemma natfloor_power:
|
|
2040 |
assumes "x = real (natfloor x)"
|
|
2041 |
shows "natfloor (x ^ n) = natfloor x ^ n"
|
|
2042 |
proof -
|
|
2043 |
from assms have "0 \<le> floor x" by auto
|
|
2044 |
note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
|
|
2045 |
from floor_power[OF this]
|
|
2046 |
show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
|
|
2047 |
by simp
|
|
2048 |
qed
|
|
2049 |
|
|
2050 |
|
|
2051 |
subsection {* Implementation of rational real numbers *}
|
|
2052 |
|
|
2053 |
text {* Formal constructor *}
|
|
2054 |
|
|
2055 |
definition Ratreal :: "rat \<Rightarrow> real" where
|
|
2056 |
[code_abbrev, simp]: "Ratreal = of_rat"
|
|
2057 |
|
|
2058 |
code_datatype Ratreal
|
|
2059 |
|
|
2060 |
|
|
2061 |
text {* Numerals *}
|
|
2062 |
|
|
2063 |
lemma [code_abbrev]:
|
|
2064 |
"(of_rat (of_int a) :: real) = of_int a"
|
|
2065 |
by simp
|
|
2066 |
|
|
2067 |
lemma [code_abbrev]:
|
|
2068 |
"(of_rat 0 :: real) = 0"
|
|
2069 |
by simp
|
|
2070 |
|
|
2071 |
lemma [code_abbrev]:
|
|
2072 |
"(of_rat 1 :: real) = 1"
|
|
2073 |
by simp
|
|
2074 |
|
|
2075 |
lemma [code_abbrev]:
|
|
2076 |
"(of_rat (numeral k) :: real) = numeral k"
|
|
2077 |
by simp
|
|
2078 |
|
|
2079 |
lemma [code_abbrev]:
|
|
2080 |
"(of_rat (neg_numeral k) :: real) = neg_numeral k"
|
|
2081 |
by simp
|
|
2082 |
|
|
2083 |
lemma [code_post]:
|
|
2084 |
"(of_rat (0 / r) :: real) = 0"
|
|
2085 |
"(of_rat (r / 0) :: real) = 0"
|
|
2086 |
"(of_rat (1 / 1) :: real) = 1"
|
|
2087 |
"(of_rat (numeral k / 1) :: real) = numeral k"
|
|
2088 |
"(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
|
|
2089 |
"(of_rat (1 / numeral k) :: real) = 1 / numeral k"
|
|
2090 |
"(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
|
|
2091 |
"(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
|
|
2092 |
"(of_rat (numeral k / neg_numeral l) :: real) = numeral k / neg_numeral l"
|
|
2093 |
"(of_rat (neg_numeral k / numeral l) :: real) = neg_numeral k / numeral l"
|
|
2094 |
"(of_rat (neg_numeral k / neg_numeral l) :: real) = neg_numeral k / neg_numeral l"
|
|
2095 |
by (simp_all add: of_rat_divide)
|
|
2096 |
|
|
2097 |
|
|
2098 |
text {* Operations *}
|
|
2099 |
|
|
2100 |
lemma zero_real_code [code]:
|
|
2101 |
"0 = Ratreal 0"
|
|
2102 |
by simp
|
|
2103 |
|
|
2104 |
lemma one_real_code [code]:
|
|
2105 |
"1 = Ratreal 1"
|
|
2106 |
by simp
|
|
2107 |
|
|
2108 |
instantiation real :: equal
|
|
2109 |
begin
|
|
2110 |
|
|
2111 |
definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
|
|
2112 |
|
|
2113 |
instance proof
|
|
2114 |
qed (simp add: equal_real_def)
|
|
2115 |
|
|
2116 |
lemma real_equal_code [code]:
|
|
2117 |
"HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
|
|
2118 |
by (simp add: equal_real_def equal)
|
|
2119 |
|
|
2120 |
lemma [code nbe]:
|
|
2121 |
"HOL.equal (x::real) x \<longleftrightarrow> True"
|
|
2122 |
by (rule equal_refl)
|
|
2123 |
|
|
2124 |
end
|
|
2125 |
|
|
2126 |
lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y"
|
|
2127 |
by (simp add: of_rat_less_eq)
|
|
2128 |
|
|
2129 |
lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> x < y"
|
|
2130 |
by (simp add: of_rat_less)
|
|
2131 |
|
|
2132 |
lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"
|
|
2133 |
by (simp add: of_rat_add)
|
|
2134 |
|
|
2135 |
lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)"
|
|
2136 |
by (simp add: of_rat_mult)
|
|
2137 |
|
|
2138 |
lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)"
|
|
2139 |
by (simp add: of_rat_minus)
|
|
2140 |
|
|
2141 |
lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"
|
|
2142 |
by (simp add: of_rat_diff)
|
|
2143 |
|
|
2144 |
lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
|
|
2145 |
by (simp add: of_rat_inverse)
|
|
2146 |
|
|
2147 |
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
|
|
2148 |
by (simp add: of_rat_divide)
|
|
2149 |
|
|
2150 |
lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
|
|
2151 |
by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)
|
|
2152 |
|
|
2153 |
|
|
2154 |
text {* Quickcheck *}
|
|
2155 |
|
|
2156 |
definition (in term_syntax)
|
|
2157 |
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
|
|
2158 |
[code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
|
|
2159 |
|
|
2160 |
notation fcomp (infixl "\<circ>>" 60)
|
|
2161 |
notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
2162 |
|
|
2163 |
instantiation real :: random
|
|
2164 |
begin
|
|
2165 |
|
|
2166 |
definition
|
|
2167 |
"Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
|
|
2168 |
|
|
2169 |
instance ..
|
|
2170 |
|
|
2171 |
end
|
|
2172 |
|
|
2173 |
no_notation fcomp (infixl "\<circ>>" 60)
|
|
2174 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
2175 |
|
|
2176 |
instantiation real :: exhaustive
|
|
2177 |
begin
|
|
2178 |
|
|
2179 |
definition
|
|
2180 |
"exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
|
|
2181 |
|
|
2182 |
instance ..
|
|
2183 |
|
|
2184 |
end
|
|
2185 |
|
|
2186 |
instantiation real :: full_exhaustive
|
|
2187 |
begin
|
|
2188 |
|
|
2189 |
definition
|
|
2190 |
"full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
|
|
2191 |
|
|
2192 |
instance ..
|
|
2193 |
|
|
2194 |
end
|
|
2195 |
|
|
2196 |
instantiation real :: narrowing
|
|
2197 |
begin
|
|
2198 |
|
|
2199 |
definition
|
|
2200 |
"narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
|
|
2201 |
|
|
2202 |
instance ..
|
|
2203 |
|
|
2204 |
end
|
|
2205 |
|
|
2206 |
|
|
2207 |
subsection {* Setup for Nitpick *}
|
|
2208 |
|
|
2209 |
declaration {*
|
|
2210 |
Nitpick_HOL.register_frac_type @{type_name real}
|
|
2211 |
[(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
|
|
2212 |
(@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
|
|
2213 |
(@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
|
|
2214 |
(@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
|
|
2215 |
(@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
|
|
2216 |
(@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
|
|
2217 |
(@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
|
|
2218 |
(@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
|
|
2219 |
*}
|
|
2220 |
|
|
2221 |
lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real
|
|
2222 |
ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
|
|
2223 |
times_real_inst.times_real uminus_real_inst.uminus_real
|
|
2224 |
zero_real_inst.zero_real
|
|
2225 |
|
|
2226 |
ML_file "Tools/SMT/smt_real.ML"
|
|
2227 |
setup SMT_Real.setup
|
|
2228 |
|
|
2229 |
end
|