author  hoelzl 
Fri, 22 Mar 2013 10:41:43 +0100  
changeset 51474  1e9e68247ad1 
parent 51473  1210309fddab 
child 51478  270b21f3ae0a 
permissions  rwrr 
51471  1 
(* Title: HOL/Basic_Topology.thy 
2 
Author: Brian Huffman 

3 
Author: Johannes Hölzl 

4 
*) 

5 

6 
header {* Topological Spaces *} 

7 

8 
theory Topological_Spaces 

9 
imports Main 

10 
begin 

11 

12 
subsection {* Topological space *} 

13 

14 
class "open" = 

15 
fixes "open" :: "'a set \<Rightarrow> bool" 

16 

17 
class topological_space = "open" + 

18 
assumes open_UNIV [simp, intro]: "open UNIV" 

19 
assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)" 

20 
assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)" 

21 
begin 

22 

23 
definition 

24 
closed :: "'a set \<Rightarrow> bool" where 

25 
"closed S \<longleftrightarrow> open ( S)" 

26 

27 
lemma open_empty [intro, simp]: "open {}" 

28 
using open_Union [of "{}"] by simp 

29 

30 
lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)" 

31 
using open_Union [of "{S, T}"] by simp 

32 

33 
lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)" 

34 
unfolding SUP_def by (rule open_Union) auto 

35 

36 
lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)" 

37 
by (induct set: finite) auto 

38 

39 
lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)" 

40 
unfolding INF_def by (rule open_Inter) auto 

41 

42 
lemma closed_empty [intro, simp]: "closed {}" 

43 
unfolding closed_def by simp 

44 

45 
lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)" 

46 
unfolding closed_def by auto 

47 

48 
lemma closed_UNIV [intro, simp]: "closed UNIV" 

49 
unfolding closed_def by simp 

50 

51 
lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)" 

52 
unfolding closed_def by auto 

53 

54 
lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)" 

55 
unfolding closed_def by auto 

56 

57 
lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)" 

58 
unfolding closed_def uminus_Inf by auto 

59 

60 
lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)" 

61 
by (induct set: finite) auto 

62 

63 
lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)" 

64 
unfolding SUP_def by (rule closed_Union) auto 

65 

66 
lemma open_closed: "open S \<longleftrightarrow> closed ( S)" 

67 
unfolding closed_def by simp 

68 

69 
lemma closed_open: "closed S \<longleftrightarrow> open ( S)" 

70 
unfolding closed_def by simp 

71 

72 
lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S  T)" 

73 
unfolding closed_open Diff_eq by (rule open_Int) 

74 

75 
lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S  T)" 

76 
unfolding open_closed Diff_eq by (rule closed_Int) 

77 

78 
lemma open_Compl [intro]: "closed S \<Longrightarrow> open ( S)" 

79 
unfolding closed_open . 

80 

81 
lemma closed_Compl [intro]: "open S \<Longrightarrow> closed ( S)" 

82 
unfolding open_closed . 

83 

84 
end 

85 

86 
subsection{* Hausdorff and other separation properties *} 

87 

88 
class t0_space = topological_space + 

89 
assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)" 

90 

91 
class t1_space = topological_space + 

92 
assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U" 

93 

94 
instance t1_space \<subseteq> t0_space 

95 
proof qed (fast dest: t1_space) 

96 

97 
lemma separation_t1: 

98 
fixes x y :: "'a::t1_space" 

99 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)" 

100 
using t1_space[of x y] by blast 

101 

102 
lemma closed_singleton: 

103 
fixes a :: "'a::t1_space" 

104 
shows "closed {a}" 

105 
proof  

106 
let ?T = "\<Union>{S. open S \<and> a \<notin> S}" 

107 
have "open ?T" by (simp add: open_Union) 

108 
also have "?T =  {a}" 

109 
by (simp add: set_eq_iff separation_t1, auto) 

110 
finally show "closed {a}" unfolding closed_def . 

111 
qed 

112 

113 
lemma closed_insert [simp]: 

114 
fixes a :: "'a::t1_space" 

115 
assumes "closed S" shows "closed (insert a S)" 

116 
proof  

117 
from closed_singleton assms 

118 
have "closed ({a} \<union> S)" by (rule closed_Un) 

119 
thus "closed (insert a S)" by simp 

120 
qed 

121 

122 
lemma finite_imp_closed: 

123 
fixes S :: "'a::t1_space set" 

124 
shows "finite S \<Longrightarrow> closed S" 

125 
by (induct set: finite, simp_all) 

126 

127 
text {* T2 spaces are also known as Hausdorff spaces. *} 

128 

129 
class t2_space = topological_space + 

130 
assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

131 

132 
instance t2_space \<subseteq> t1_space 

133 
proof qed (fast dest: hausdorff) 

134 

135 
lemma separation_t2: 

136 
fixes x y :: "'a::t2_space" 

137 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 

138 
using hausdorff[of x y] by blast 

139 

140 
lemma separation_t0: 

141 
fixes x y :: "'a::t0_space" 

142 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" 

143 
using t0_space[of x y] by blast 

144 

145 
text {* A perfect space is a topological space with no isolated points. *} 

146 

147 
class perfect_space = topological_space + 

148 
assumes not_open_singleton: "\<not> open {x}" 

149 

150 

151 
subsection {* Generators for toplogies *} 

152 

153 
inductive generate_topology for S where 

154 
UNIV: "generate_topology S UNIV" 

155 
 Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)" 

156 
 UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)" 

157 
 Basis: "s \<in> S \<Longrightarrow> generate_topology S s" 

158 

159 
hide_fact (open) UNIV Int UN Basis 

160 

161 
lemma generate_topology_Union: 

162 
"(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)" 

163 
unfolding SUP_def by (intro generate_topology.UN) auto 

164 

165 
lemma topological_space_generate_topology: 

166 
"class.topological_space (generate_topology S)" 

167 
by default (auto intro: generate_topology.intros) 

168 

169 
subsection {* Order topologies *} 

170 

171 
class order_topology = order + "open" + 

172 
assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))" 

173 
begin 

174 

175 
subclass topological_space 

176 
unfolding open_generated_order 

177 
by (rule topological_space_generate_topology) 

178 

179 
lemma open_greaterThan [simp]: "open {a <..}" 

180 
unfolding open_generated_order by (auto intro: generate_topology.Basis) 

181 

182 
lemma open_lessThan [simp]: "open {..< a}" 

183 
unfolding open_generated_order by (auto intro: generate_topology.Basis) 

184 

185 
lemma open_greaterThanLessThan [simp]: "open {a <..< b}" 

186 
unfolding greaterThanLessThan_eq by (simp add: open_Int) 

187 

188 
end 

189 

190 
class linorder_topology = linorder + order_topology 

191 

192 
lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}" 

193 
by (simp add: closed_open) 

194 

195 
lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}" 

196 
by (simp add: closed_open) 

197 

198 
lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}" 

199 
proof  

200 
have "{a .. b} = {a ..} \<inter> {.. b}" 

201 
by auto 

202 
then show ?thesis 

203 
by (simp add: closed_Int) 

204 
qed 

205 

206 
lemma (in linorder) less_separate: 

207 
assumes "x < y" 

208 
shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}" 

209 
proof cases 

210 
assume "\<exists>z. x < z \<and> z < y" 

211 
then guess z .. 

212 
then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}" 

213 
by auto 

214 
then show ?thesis by blast 

215 
next 

216 
assume "\<not> (\<exists>z. x < z \<and> z < y)" 

217 
with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}" 

218 
by auto 

219 
then show ?thesis by blast 

220 
qed 

221 

222 
instance linorder_topology \<subseteq> t2_space 

223 
proof 

224 
fix x y :: 'a 

225 
from less_separate[of x y] less_separate[of y x] 

226 
show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

227 
by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+ 

228 
qed 

229 

230 
lemma open_right: 

231 
fixes S :: "'a :: {no_top, linorder_topology} set" 

232 
assumes "open S" "x \<in> S" shows "\<exists>b>x. {x ..< b} \<subseteq> S" 

233 
using assms unfolding open_generated_order 

234 
proof induction 

235 
case (Int A B) 

236 
then obtain a b where "a > x" "{x ..< a} \<subseteq> A" "b > x" "{x ..< b} \<subseteq> B" by auto 

237 
then show ?case by (auto intro!: exI[of _ "min a b"]) 

238 
next 

239 
case (Basis S) 

240 
moreover from gt_ex[of x] guess b .. 

241 
ultimately show ?case by (fastforce intro: exI[of _ b]) 

242 
qed (fastforce intro: gt_ex)+ 

243 

244 
lemma open_left: 

245 
fixes S :: "'a :: {no_bot, linorder_topology} set" 

246 
assumes "open S" "x \<in> S" shows "\<exists>b<x. {b <.. x} \<subseteq> S" 

247 
using assms unfolding open_generated_order 

248 
proof induction 

249 
case (Int A B) 

250 
then obtain a b where "a < x" "{a <.. x} \<subseteq> A" "b < x" "{b <.. x} \<subseteq> B" by auto 

251 
then show ?case by (auto intro!: exI[of _ "max a b"]) 

252 
next 

253 
case (Basis S) 

254 
moreover from lt_ex[of x] guess b .. 

255 
ultimately show ?case by (fastforce intro: exI[of _ b]) 

256 
next 

257 
case UN then show ?case by blast 

258 
qed (fastforce intro: lt_ex) 

259 

260 
subsection {* Filters *} 

261 

262 
text {* 

263 
This definition also allows nonproper filters. 

264 
*} 

265 

266 
locale is_filter = 

267 
fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 

268 
assumes True: "F (\<lambda>x. True)" 

269 
assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)" 

270 
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)" 

271 

272 
typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}" 

273 
proof 

274 
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro) 

275 
qed 

276 

277 
lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" 

278 
using Rep_filter [of F] by simp 

279 

280 
lemma Abs_filter_inverse': 

281 
assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" 

282 
using assms by (simp add: Abs_filter_inverse) 

283 

284 

285 
subsubsection {* Eventually *} 

286 

287 
definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" 

288 
where "eventually P F \<longleftrightarrow> Rep_filter F P" 

289 

290 
lemma eventually_Abs_filter: 

291 
assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" 

292 
unfolding eventually_def using assms by (simp add: Abs_filter_inverse) 

293 

294 
lemma filter_eq_iff: 

295 
shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')" 

296 
unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. 

297 

298 
lemma eventually_True [simp]: "eventually (\<lambda>x. True) F" 

299 
unfolding eventually_def 

300 
by (rule is_filter.True [OF is_filter_Rep_filter]) 

301 

302 
lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F" 

303 
proof  

304 
assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext) 

305 
thus "eventually P F" by simp 

306 
qed 

307 

308 
lemma eventually_mono: 

309 
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F" 

310 
unfolding eventually_def 

311 
by (rule is_filter.mono [OF is_filter_Rep_filter]) 

312 

313 
lemma eventually_conj: 

314 
assumes P: "eventually (\<lambda>x. P x) F" 

315 
assumes Q: "eventually (\<lambda>x. Q x) F" 

316 
shows "eventually (\<lambda>x. P x \<and> Q x) F" 

317 
using assms unfolding eventually_def 

318 
by (rule is_filter.conj [OF is_filter_Rep_filter]) 

319 

320 
lemma eventually_Ball_finite: 

321 
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" 

322 
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" 

323 
using assms by (induct set: finite, simp, simp add: eventually_conj) 

324 

325 
lemma eventually_all_finite: 

326 
fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" 

327 
assumes "\<And>y. eventually (\<lambda>x. P x y) net" 

328 
shows "eventually (\<lambda>x. \<forall>y. P x y) net" 

329 
using eventually_Ball_finite [of UNIV P] assms by simp 

330 

331 
lemma eventually_mp: 

332 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

333 
assumes "eventually (\<lambda>x. P x) F" 

334 
shows "eventually (\<lambda>x. Q x) F" 

335 
proof (rule eventually_mono) 

336 
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp 

337 
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F" 

338 
using assms by (rule eventually_conj) 

339 
qed 

340 

341 
lemma eventually_rev_mp: 

342 
assumes "eventually (\<lambda>x. P x) F" 

343 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

344 
shows "eventually (\<lambda>x. Q x) F" 

345 
using assms(2) assms(1) by (rule eventually_mp) 

346 

347 
lemma eventually_conj_iff: 

348 
"eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F" 

349 
by (auto intro: eventually_conj elim: eventually_rev_mp) 

350 

351 
lemma eventually_elim1: 

352 
assumes "eventually (\<lambda>i. P i) F" 

353 
assumes "\<And>i. P i \<Longrightarrow> Q i" 

354 
shows "eventually (\<lambda>i. Q i) F" 

355 
using assms by (auto elim!: eventually_rev_mp) 

356 

357 
lemma eventually_elim2: 

358 
assumes "eventually (\<lambda>i. P i) F" 

359 
assumes "eventually (\<lambda>i. Q i) F" 

360 
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" 

361 
shows "eventually (\<lambda>i. R i) F" 

362 
using assms by (auto elim!: eventually_rev_mp) 

363 

364 
lemma eventually_subst: 

365 
assumes "eventually (\<lambda>n. P n = Q n) F" 

366 
shows "eventually P F = eventually Q F" (is "?L = ?R") 

367 
proof  

368 
from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

369 
and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F" 

370 
by (auto elim: eventually_elim1) 

371 
then show ?thesis by (auto elim: eventually_elim2) 

372 
qed 

373 

374 
ML {* 

375 
fun eventually_elim_tac ctxt thms thm = 

376 
let 

377 
val thy = Proof_Context.theory_of ctxt 

378 
val mp_thms = thms RL [@{thm eventually_rev_mp}] 

379 
val raw_elim_thm = 

380 
(@{thm allI} RS @{thm always_eventually}) 

381 
> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms 

382 
> fold (fn _ => fn thm => @{thm impI} RS thm) thms 

383 
val cases_prop = prop_of (raw_elim_thm RS thm) 

384 
val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])]) 

385 
in 

386 
CASES cases (rtac raw_elim_thm 1) thm 

387 
end 

388 
*} 

389 

390 
method_setup eventually_elim = {* 

391 
Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt)) 

392 
*} "elimination of eventually quantifiers" 

393 

394 

395 
subsubsection {* Finerthan relation *} 

396 

397 
text {* @{term "F \<le> F'"} means that filter @{term F} is finer than 

398 
filter @{term F'}. *} 

399 

400 
instantiation filter :: (type) complete_lattice 

401 
begin 

402 

403 
definition le_filter_def: 

404 
"F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)" 

405 

406 
definition 

407 
"(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F" 

408 

409 
definition 

410 
"top = Abs_filter (\<lambda>P. \<forall>x. P x)" 

411 

412 
definition 

413 
"bot = Abs_filter (\<lambda>P. True)" 

414 

415 
definition 

416 
"sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')" 

417 

418 
definition 

419 
"inf F F' = Abs_filter 

420 
(\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" 

421 

422 
definition 

423 
"Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)" 

424 

425 
definition 

426 
"Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}" 

427 

428 
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)" 

429 
unfolding top_filter_def 

430 
by (rule eventually_Abs_filter, rule is_filter.intro, auto) 

431 

432 
lemma eventually_bot [simp]: "eventually P bot" 

433 
unfolding bot_filter_def 

434 
by (subst eventually_Abs_filter, rule is_filter.intro, auto) 

435 

436 
lemma eventually_sup: 

437 
"eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'" 

438 
unfolding sup_filter_def 

439 
by (rule eventually_Abs_filter, rule is_filter.intro) 

440 
(auto elim!: eventually_rev_mp) 

441 

442 
lemma eventually_inf: 

443 
"eventually P (inf F F') \<longleftrightarrow> 

444 
(\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" 

445 
unfolding inf_filter_def 

446 
apply (rule eventually_Abs_filter, rule is_filter.intro) 

447 
apply (fast intro: eventually_True) 

448 
apply clarify 

449 
apply (intro exI conjI) 

450 
apply (erule (1) eventually_conj) 

451 
apply (erule (1) eventually_conj) 

452 
apply simp 

453 
apply auto 

454 
done 

455 

456 
lemma eventually_Sup: 

457 
"eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)" 

458 
unfolding Sup_filter_def 

459 
apply (rule eventually_Abs_filter, rule is_filter.intro) 

460 
apply (auto intro: eventually_conj elim!: eventually_rev_mp) 

461 
done 

462 

463 
instance proof 

464 
fix F F' F'' :: "'a filter" and S :: "'a filter set" 

465 
{ show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F" 

466 
by (rule less_filter_def) } 

467 
{ show "F \<le> F" 

468 
unfolding le_filter_def by simp } 

469 
{ assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''" 

470 
unfolding le_filter_def by simp } 

471 
{ assume "F \<le> F'" and "F' \<le> F" thus "F = F'" 

472 
unfolding le_filter_def filter_eq_iff by fast } 

473 
{ show "F \<le> top" 

474 
unfolding le_filter_def eventually_top by (simp add: always_eventually) } 

475 
{ show "bot \<le> F" 

476 
unfolding le_filter_def by simp } 

477 
{ show "F \<le> sup F F'" and "F' \<le> sup F F'" 

478 
unfolding le_filter_def eventually_sup by simp_all } 

479 
{ assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''" 

480 
unfolding le_filter_def eventually_sup by simp } 

481 
{ show "inf F F' \<le> F" and "inf F F' \<le> F'" 

482 
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } 

483 
{ assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''" 

484 
unfolding le_filter_def eventually_inf 

485 
by (auto elim!: eventually_mono intro: eventually_conj) } 

486 
{ assume "F \<in> S" thus "F \<le> Sup S" 

487 
unfolding le_filter_def eventually_Sup by simp } 

488 
{ assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'" 

489 
unfolding le_filter_def eventually_Sup by simp } 

490 
{ assume "F'' \<in> S" thus "Inf S \<le> F''" 

491 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

492 
{ assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S" 

493 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

494 
qed 

495 

496 
end 

497 

498 
lemma filter_leD: 

499 
"F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F" 

500 
unfolding le_filter_def by simp 

501 

502 
lemma filter_leI: 

503 
"(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'" 

504 
unfolding le_filter_def by simp 

505 

506 
lemma eventually_False: 

507 
"eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot" 

508 
unfolding filter_eq_iff by (auto elim: eventually_rev_mp) 

509 

510 
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool" 

511 
where "trivial_limit F \<equiv> F = bot" 

512 

513 
lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F" 

514 
by (rule eventually_False [symmetric]) 

515 

516 
lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P" 

517 
by (cases P) (simp_all add: eventually_False) 

518 

519 

520 
subsubsection {* Map function for filters *} 

521 

522 
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" 

523 
where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)" 

524 

525 
lemma eventually_filtermap: 

526 
"eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F" 

527 
unfolding filtermap_def 

528 
apply (rule eventually_Abs_filter) 

529 
apply (rule is_filter.intro) 

530 
apply (auto elim!: eventually_rev_mp) 

531 
done 

532 

533 
lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F" 

534 
by (simp add: filter_eq_iff eventually_filtermap) 

535 

536 
lemma filtermap_filtermap: 

537 
"filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F" 

538 
by (simp add: filter_eq_iff eventually_filtermap) 

539 

540 
lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'" 

541 
unfolding le_filter_def eventually_filtermap by simp 

542 

543 
lemma filtermap_bot [simp]: "filtermap f bot = bot" 

544 
by (simp add: filter_eq_iff eventually_filtermap) 

545 

546 
lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)" 

547 
by (auto simp: filter_eq_iff eventually_filtermap eventually_sup) 

548 

549 
subsubsection {* Order filters *} 

550 

551 
definition at_top :: "('a::order) filter" 

552 
where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" 

553 

554 
lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)" 

555 
unfolding at_top_def 

556 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

557 
fix P Q :: "'a \<Rightarrow> bool" 

558 
assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n" 

559 
then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto 

560 
then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp 

561 
then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" .. 

562 
qed auto 

563 

564 
lemma eventually_ge_at_top: 

565 
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top" 

566 
unfolding eventually_at_top_linorder by auto 

567 

568 
lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)" 

569 
unfolding eventually_at_top_linorder 

570 
proof safe 

571 
fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N]) 

572 
next 

573 
fix N assume "\<forall>n>N. P n" 

574 
moreover from gt_ex[of N] guess y .. 

575 
ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y]) 

576 
qed 

577 

578 
lemma eventually_gt_at_top: 

579 
"eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top" 

580 
unfolding eventually_at_top_dense by auto 

581 

582 
definition at_bot :: "('a::order) filter" 

583 
where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)" 

584 

585 
lemma eventually_at_bot_linorder: 

586 
fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)" 

587 
unfolding at_bot_def 

588 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

589 
fix P Q :: "'a \<Rightarrow> bool" 

590 
assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n" 

591 
then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto 

592 
then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp 

593 
then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" .. 

594 
qed auto 

595 

596 
lemma eventually_le_at_bot: 

597 
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot" 

598 
unfolding eventually_at_bot_linorder by auto 

599 

600 
lemma eventually_at_bot_dense: 

601 
fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)" 

602 
unfolding eventually_at_bot_linorder 

603 
proof safe 

604 
fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N]) 

605 
next 

606 
fix N assume "\<forall>n<N. P n" 

607 
moreover from lt_ex[of N] guess y .. 

608 
ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y]) 

609 
qed 

610 

611 
lemma eventually_gt_at_bot: 

612 
"eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot" 

613 
unfolding eventually_at_bot_dense by auto 

614 

615 
subsection {* Sequentially *} 

616 

617 
abbreviation sequentially :: "nat filter" 

618 
where "sequentially == at_top" 

619 

620 
lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" 

621 
unfolding at_top_def by simp 

622 

623 
lemma eventually_sequentially: 

624 
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 

625 
by (rule eventually_at_top_linorder) 

626 

627 
lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot" 

628 
unfolding filter_eq_iff eventually_sequentially by auto 

629 

630 
lemmas trivial_limit_sequentially = sequentially_bot 

631 

632 
lemma eventually_False_sequentially [simp]: 

633 
"\<not> eventually (\<lambda>n. False) sequentially" 

634 
by (simp add: eventually_False) 

635 

636 
lemma le_sequentially: 

637 
"F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" 

638 
unfolding le_filter_def eventually_sequentially 

639 
by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) 

640 

641 
lemma eventually_sequentiallyI: 

642 
assumes "\<And>x. c \<le> x \<Longrightarrow> P x" 

643 
shows "eventually P sequentially" 

644 
using assms by (auto simp: eventually_sequentially) 

645 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

646 
lemma eventually_sequentially_seg: 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

647 
"eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

648 
unfolding eventually_sequentially 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

649 
apply safe 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

650 
apply (rule_tac x="N + k" in exI) 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

651 
apply rule 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

652 
apply (erule_tac x="n  k" in allE) 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

653 
apply auto [] 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

654 
apply (rule_tac x=N in exI) 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

655 
apply auto [] 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

656 
done 
51471  657 

658 
subsubsection {* Standard filters *} 

659 

660 
definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) 

661 
where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)" 

662 

663 
lemma eventually_within: 

664 
"eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F" 

665 
unfolding within_def 

666 
by (rule eventually_Abs_filter, rule is_filter.intro) 

667 
(auto elim!: eventually_rev_mp) 

668 

669 
lemma within_UNIV [simp]: "F within UNIV = F" 

670 
unfolding filter_eq_iff eventually_within by simp 

671 

672 
lemma within_empty [simp]: "F within {} = bot" 

673 
unfolding filter_eq_iff eventually_within by simp 

674 

675 
lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)" 

676 
by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1) 

677 

678 
lemma within_le: "F within S \<le> F" 

679 
unfolding le_filter_def eventually_within by (auto elim: eventually_elim1) 

680 

681 
lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S" 

682 
unfolding le_filter_def eventually_within by (auto elim: eventually_elim2) 

683 

684 
lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'" 

685 
by (blast intro: within_le le_withinI order_trans) 

686 

687 
subsubsection {* Topological filters *} 

688 

689 
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter" 

690 
where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" 

691 

692 
definition (in topological_space) at :: "'a \<Rightarrow> 'a filter" 

693 
where "at a = nhds a within  {a}" 

694 

51473  695 
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where 
51471  696 
"at_right x \<equiv> at x within {x <..}" 
697 

51473  698 
abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter" where 
51471  699 
"at_left x \<equiv> at x within {..< x}" 
700 

51473  701 
lemma (in topological_space) eventually_nhds: 
51471  702 
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" 
703 
unfolding nhds_def 

704 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

51473  705 
have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp 
51471  706 
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" .. 
707 
next 

708 
fix P Q 

709 
assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 

710 
and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" 

711 
then obtain S T where 

712 
"open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 

713 
"open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto 

714 
hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)" 

715 
by (simp add: open_Int) 

716 
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" .. 

717 
qed auto 

718 

719 
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot" 

720 
unfolding trivial_limit_def eventually_nhds by simp 

721 

722 
lemma eventually_at_topological: 

723 
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))" 

724 
unfolding at_def eventually_within eventually_nhds by simp 

725 

726 
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" 

727 
unfolding trivial_limit_def eventually_at_topological 

728 
by (safe, case_tac "S = {a}", simp, fast, fast) 

729 

730 
lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot" 

731 
by (simp add: at_eq_bot_iff not_open_singleton) 

732 

733 
lemma eventually_at_right: 

734 
fixes x :: "'a :: {no_top, linorder_topology}" 

735 
shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))" 

736 
unfolding eventually_nhds eventually_within at_def 

737 
proof safe 

738 
fix S assume "open S" "x \<in> S" 

739 
note open_right[OF this] 

740 
moreover assume "\<forall>s\<in>S. s \<in>  {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s" 

741 
ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z" 

742 
by (auto simp: subset_eq Ball_def) 

743 
next 

744 
fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z" 

745 
then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in>  {x} \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)" 

746 
by (intro exI[of _ "{..< b}"]) auto 

747 
qed 

748 

749 
lemma eventually_at_left: 

750 
fixes x :: "'a :: {no_bot, linorder_topology}" 

751 
shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))" 

752 
unfolding eventually_nhds eventually_within at_def 

753 
proof safe 

754 
fix S assume "open S" "x \<in> S" 

755 
note open_left[OF this] 

756 
moreover assume "\<forall>s\<in>S. s \<in>  {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s" 

757 
ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z" 

758 
by (auto simp: subset_eq Ball_def) 

759 
next 

760 
fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z" 

761 
then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in>  {x} \<longrightarrow> xa \<in> {..<x} \<longrightarrow> P xa)" 

762 
by (intro exI[of _ "{b <..}"]) auto 

763 
qed 

764 

765 
lemma trivial_limit_at_left_real [simp]: 

766 
"\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))" 

767 
unfolding trivial_limit_def eventually_at_left by (auto dest: dense) 

768 

769 
lemma trivial_limit_at_right_real [simp]: 

770 
"\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))" 

771 
unfolding trivial_limit_def eventually_at_right by (auto dest: dense) 

772 

773 
lemma at_within_eq: "at x within T = nhds x within (T  {x})" 

774 
unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq) 

775 

776 
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)" 

777 
by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 

778 
elim: eventually_elim2 eventually_elim1) 

779 

780 
lemma eventually_at_split: 

781 
"eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)" 

782 
by (subst at_eq_sup_left_right) (simp add: eventually_sup) 

783 

784 
subsection {* Limits *} 

785 

786 
definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where 

787 
"filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2" 

788 

789 
syntax 

790 
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10) 

791 

792 
translations 

793 
"LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1" 

794 

795 
lemma filterlim_iff: 

796 
"(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)" 

797 
unfolding filterlim_def le_filter_def eventually_filtermap .. 

798 

799 
lemma filterlim_compose: 

800 
"filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1" 

801 
unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans) 

802 

803 
lemma filterlim_mono: 

804 
"filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'" 

805 
unfolding filterlim_def by (metis filtermap_mono order_trans) 

806 

807 
lemma filterlim_ident: "LIM x F. x :> F" 

808 
by (simp add: filterlim_def filtermap_ident) 

809 

810 
lemma filterlim_cong: 

811 
"F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'" 

812 
by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2) 

813 

814 
lemma filterlim_within: 

815 
"(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))" 

816 
unfolding filterlim_def 

817 
proof safe 

818 
assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1" 

819 
by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"]) 

820 
qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap) 

821 

822 
lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2" 

823 
unfolding filterlim_def filtermap_filtermap .. 

824 

825 
lemma filterlim_sup: 

826 
"filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)" 

827 
unfolding filterlim_def filtermap_sup by auto 

828 

829 
lemma filterlim_Suc: "filterlim Suc sequentially sequentially" 

830 
by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq) 

831 

832 
subsubsection {* Tendsto *} 

833 

834 
abbreviation (in topological_space) 

835 
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr ">" 55) where 

836 
"(f > l) F \<equiv> filterlim f (nhds l) F" 

837 

838 
lemma tendsto_eq_rhs: "(f > x) F \<Longrightarrow> x = y \<Longrightarrow> (f > y) F" 

839 
by simp 

840 

841 
ML {* 

842 

843 
structure Tendsto_Intros = Named_Thms 

844 
( 

845 
val name = @{binding tendsto_intros} 

846 
val description = "introduction rules for tendsto" 

847 
) 

848 

849 
*} 

850 

851 
setup {* 

852 
Tendsto_Intros.setup #> 

853 
Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros}, 

854 
map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of); 

855 
*} 

856 

51473  857 
lemma (in topological_space) tendsto_def: 
858 
"(f > l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" 

51471  859 
unfolding filterlim_def 
860 
proof safe 

861 
fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l" 

862 
then show "eventually (\<lambda>x. f x \<in> S) F" 

863 
unfolding eventually_nhds eventually_filtermap le_filter_def 

864 
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp) 

865 
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def) 

866 

867 
lemma filterlim_at: 

868 
"(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f > b) F)" 

869 
by (simp add: at_def filterlim_within) 

870 

871 
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f > l) F' \<Longrightarrow> (f > l) F" 

872 
unfolding tendsto_def le_filter_def by fast 

873 

51473  874 
lemma (in topological_space) topological_tendstoI: 
51471  875 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) 
876 
\<Longrightarrow> (f > l) F" 

877 
unfolding tendsto_def by auto 

878 

51473  879 
lemma (in topological_space) topological_tendstoD: 
51471  880 
"(f > l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F" 
881 
unfolding tendsto_def by auto 

882 

883 
lemma order_tendstoI: 

884 
fixes y :: "_ :: order_topology" 

885 
assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F" 

886 
assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F" 

887 
shows "(f > y) F" 

888 
proof (rule topological_tendstoI) 

889 
fix S assume "open S" "y \<in> S" 

890 
then show "eventually (\<lambda>x. f x \<in> S) F" 

891 
unfolding open_generated_order 

892 
proof induct 

893 
case (UN K) 

894 
then obtain k where "y \<in> k" "k \<in> K" by auto 

895 
with UN(2)[of k] show ?case 

896 
by (auto elim: eventually_elim1) 

897 
qed (insert assms, auto elim: eventually_elim2) 

898 
qed 

899 

900 
lemma order_tendstoD: 

901 
fixes y :: "_ :: order_topology" 

902 
assumes y: "(f > y) F" 

903 
shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F" 

904 
and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F" 

905 
using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto 

906 

907 
lemma order_tendsto_iff: 

908 
fixes f :: "_ \<Rightarrow> 'a :: order_topology" 

909 
shows "(f > x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)" 

910 
by (metis order_tendstoI order_tendstoD) 

911 

912 
lemma tendsto_bot [simp]: "(f > a) bot" 

913 
unfolding tendsto_def by simp 

914 

915 
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) > a) (at a)" 

916 
unfolding tendsto_def eventually_at_topological by auto 

917 

918 
lemma tendsto_ident_at_within [tendsto_intros]: 

919 
"((\<lambda>x. x) > a) (at a within S)" 

920 
unfolding tendsto_def eventually_within eventually_at_topological by auto 

921 

922 
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) > k) F" 

923 
by (simp add: tendsto_def) 

924 

925 
lemma tendsto_unique: 

926 
fixes f :: "'a \<Rightarrow> 'b::t2_space" 

927 
assumes "\<not> trivial_limit F" and "(f > a) F" and "(f > b) F" 

928 
shows "a = b" 

929 
proof (rule ccontr) 

930 
assume "a \<noteq> b" 

931 
obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}" 

932 
using hausdorff [OF `a \<noteq> b`] by fast 

933 
have "eventually (\<lambda>x. f x \<in> U) F" 

934 
using `(f > a) F` `open U` `a \<in> U` by (rule topological_tendstoD) 

935 
moreover 

936 
have "eventually (\<lambda>x. f x \<in> V) F" 

937 
using `(f > b) F` `open V` `b \<in> V` by (rule topological_tendstoD) 

938 
ultimately 

939 
have "eventually (\<lambda>x. False) F" 

940 
proof eventually_elim 

941 
case (elim x) 

942 
hence "f x \<in> U \<inter> V" by simp 

943 
with `U \<inter> V = {}` show ?case by simp 

944 
qed 

945 
with `\<not> trivial_limit F` show "False" 

946 
by (simp add: trivial_limit_def) 

947 
qed 

948 

949 
lemma tendsto_const_iff: 

950 
fixes a b :: "'a::t2_space" 

951 
assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) > b) F \<longleftrightarrow> a = b" 

952 
by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) 

953 

954 
lemma increasing_tendsto: 

955 
fixes f :: "_ \<Rightarrow> 'a::order_topology" 

956 
assumes bdd: "eventually (\<lambda>n. f n \<le> l) F" 

957 
and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F" 

958 
shows "(f > l) F" 

959 
using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) 

960 

961 
lemma decreasing_tendsto: 

962 
fixes f :: "_ \<Rightarrow> 'a::order_topology" 

963 
assumes bdd: "eventually (\<lambda>n. l \<le> f n) F" 

964 
and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F" 

965 
shows "(f > l) F" 

966 
using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) 

967 

968 
lemma tendsto_sandwich: 

969 
fixes f g h :: "'a \<Rightarrow> 'b::order_topology" 

970 
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net" 

971 
assumes lim: "(f > c) net" "(h > c) net" 

972 
shows "(g > c) net" 

973 
proof (rule order_tendstoI) 

974 
fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net" 

975 
using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2) 

976 
next 

977 
fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net" 

978 
using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2) 

979 
qed 

980 

981 
lemma tendsto_le: 

982 
fixes f g :: "'a \<Rightarrow> 'b::linorder_topology" 

983 
assumes F: "\<not> trivial_limit F" 

984 
assumes x: "(f > x) F" and y: "(g > y) F" 

985 
assumes ev: "eventually (\<lambda>x. g x \<le> f x) F" 

986 
shows "y \<le> x" 

987 
proof (rule ccontr) 

988 
assume "\<not> y \<le> x" 

989 
with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}" 

990 
by (auto simp: not_le) 

991 
then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F" 

992 
using x y by (auto intro: order_tendstoD) 

993 
with ev have "eventually (\<lambda>x. False) F" 

994 
by eventually_elim (insert xy, fastforce) 

995 
with F show False 

996 
by (simp add: eventually_False) 

997 
qed 

998 

999 
lemma tendsto_le_const: 

1000 
fixes f :: "'a \<Rightarrow> 'b::linorder_topology" 

1001 
assumes F: "\<not> trivial_limit F" 

1002 
assumes x: "(f > x) F" and a: "eventually (\<lambda>x. a \<le> f x) F" 

1003 
shows "a \<le> x" 

1004 
using F x tendsto_const a by (rule tendsto_le) 

1005 

1006 
subsection {* Limits to @{const at_top} and @{const at_bot} *} 

1007 

1008 
lemma filterlim_at_top: 

1009 
fixes f :: "'a \<Rightarrow> ('b::linorder)" 

1010 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)" 

1011 
by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1) 

1012 

1013 
lemma filterlim_at_top_dense: 

1014 
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" 

1015 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)" 

1016 
by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le 

1017 
filterlim_at_top[of f F] filterlim_iff[of f at_top F]) 

1018 

1019 
lemma filterlim_at_top_ge: 

1020 
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b" 

1021 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)" 

1022 
unfolding filterlim_at_top 

1023 
proof safe 

1024 
fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F" 

1025 
with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F" 

1026 
by (auto elim!: eventually_elim1) 

1027 
qed simp 

1028 

1029 
lemma filterlim_at_top_at_top: 

1030 
fixes f :: "'a::linorder \<Rightarrow> 'b::linorder" 

1031 
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 

1032 
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)" 

1033 
assumes Q: "eventually Q at_top" 

1034 
assumes P: "eventually P at_top" 

1035 
shows "filterlim f at_top at_top" 

1036 
proof  

1037 
from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y" 

1038 
unfolding eventually_at_top_linorder by auto 

1039 
show ?thesis 

1040 
proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) 

1041 
fix z assume "x \<le> z" 

1042 
with x have "P z" by auto 

1043 
have "eventually (\<lambda>x. g z \<le> x) at_top" 

1044 
by (rule eventually_ge_at_top) 

1045 
with Q show "eventually (\<lambda>x. z \<le> f x) at_top" 

1046 
by eventually_elim (metis mono bij `P z`) 

1047 
qed 

1048 
qed 

1049 

1050 
lemma filterlim_at_top_gt: 

1051 
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b" 

1052 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)" 

1053 
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge) 

1054 

1055 
lemma filterlim_at_bot: 

1056 
fixes f :: "'a \<Rightarrow> ('b::linorder)" 

1057 
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)" 

1058 
by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1) 

1059 

1060 
lemma filterlim_at_bot_le: 

1061 
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b" 

1062 
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)" 

1063 
unfolding filterlim_at_bot 

1064 
proof safe 

1065 
fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F" 

1066 
with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F" 

1067 
by (auto elim!: eventually_elim1) 

1068 
qed simp 

1069 

1070 
lemma filterlim_at_bot_lt: 

1071 
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b" 

1072 
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)" 

1073 
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans) 

1074 

1075 
lemma filterlim_at_bot_at_right: 

1076 
fixes f :: "'a::{no_top, linorder_topology} \<Rightarrow> 'b::linorder" 

1077 
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 

1078 
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)" 

1079 
assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b" 

1080 
assumes P: "eventually P at_bot" 

1081 
shows "filterlim f at_bot (at_right a)" 

1082 
proof  

1083 
from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y" 

1084 
unfolding eventually_at_bot_linorder by auto 

1085 
show ?thesis 

1086 
proof (intro filterlim_at_bot_le[THEN iffD2] allI impI) 

1087 
fix z assume "z \<le> x" 

1088 
with x have "P z" by auto 

1089 
have "eventually (\<lambda>x. x \<le> g z) (at_right a)" 

1090 
using bound[OF bij(2)[OF `P z`]] 

1091 
unfolding eventually_at_right by (auto intro!: exI[of _ "g z"]) 

1092 
with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)" 

1093 
by eventually_elim (metis bij `P z` mono) 

1094 
qed 

1095 
qed 

1096 

1097 
lemma filterlim_at_top_at_left: 

1098 
fixes f :: "'a::{no_bot, linorder_topology} \<Rightarrow> 'b::linorder" 

1099 
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 

1100 
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)" 

1101 
assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a" 

1102 
assumes P: "eventually P at_top" 

1103 
shows "filterlim f at_top (at_left a)" 

1104 
proof  

1105 
from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y" 

1106 
unfolding eventually_at_top_linorder by auto 

1107 
show ?thesis 

1108 
proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) 

1109 
fix z assume "x \<le> z" 

1110 
with x have "P z" by auto 

1111 
have "eventually (\<lambda>x. g z \<le> x) (at_left a)" 

1112 
using bound[OF bij(2)[OF `P z`]] 

1113 
unfolding eventually_at_left by (auto intro!: exI[of _ "g z"]) 

1114 
with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)" 

1115 
by eventually_elim (metis bij `P z` mono) 

1116 
qed 

1117 
qed 

1118 

1119 
lemma filterlim_split_at: 

1120 
"filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::'a::linorder_topology))" 

1121 
by (subst at_eq_sup_left_right) (rule filterlim_sup) 

1122 

1123 
lemma filterlim_at_split: 

1124 
"filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)" 

1125 
by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup) 

1126 

1127 

1128 
subsection {* Limits on sequences *} 

1129 

1130 
abbreviation (in topological_space) 

1131 
LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 

1132 
("((_)/ > (_))" [60, 60] 60) where 

1133 
"X > L \<equiv> (X > L) sequentially" 

1134 

1135 
definition 

1136 
lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where 

1137 
{*Standard definition of limit using choice operator*} 

1138 
"lim X = (THE L. X > L)" 

1139 

1140 
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 

1141 
"convergent X = (\<exists>L. X > L)" 

1142 

1143 
subsubsection {* Monotone sequences and subsequences *} 

1144 

1145 
definition 

1146 
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

1147 
{*Definition of monotonicity. 

1148 
The use of disjunction here complicates proofs considerably. 

1149 
One alternative is to add a Boolean argument to indicate the direction. 

1150 
Another is to develop the notions of increasing and decreasing first.*} 

1151 
"monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n)  (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" 

1152 

1153 
definition 

1154 
incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

1155 
{*Increasing sequence*} 

1156 
"incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)" 

1157 

1158 
definition 

1159 
decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

1160 
{*Decreasing sequence*} 

1161 
"decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" 

1162 

1163 
definition 

1164 
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where 

1165 
{*Definition of subsequence*} 

1166 
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)" 

1167 

1168 
lemma incseq_mono: "mono f \<longleftrightarrow> incseq f" 

1169 
unfolding mono_def incseq_def by auto 

1170 

1171 
lemma incseq_SucI: 

1172 
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X" 

1173 
using lift_Suc_mono_le[of X] 

1174 
by (auto simp: incseq_def) 

1175 

1176 
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j" 

1177 
by (auto simp: incseq_def) 

1178 

1179 
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)" 

1180 
using incseqD[of A i "Suc i"] by auto 

1181 

1182 
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" 

1183 
by (auto intro: incseq_SucI dest: incseq_SucD) 

1184 

1185 
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)" 

1186 
unfolding incseq_def by auto 

1187 

1188 
lemma decseq_SucI: 

1189 
"(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X" 

1190 
using order.lift_Suc_mono_le[OF dual_order, of X] 

1191 
by (auto simp: decseq_def) 

1192 

1193 
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i" 

1194 
by (auto simp: decseq_def) 

1195 

1196 
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i" 

1197 
using decseqD[of A i "Suc i"] by auto 

1198 

1199 
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" 

1200 
by (auto intro: decseq_SucI dest: decseq_SucD) 

1201 

1202 
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)" 

1203 
unfolding decseq_def by auto 

1204 

1205 
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X" 

1206 
unfolding monoseq_def incseq_def decseq_def .. 

1207 

1208 
lemma monoseq_Suc: 

1209 
"monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)" 

1210 
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. 

1211 

1212 
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" 

1213 
by (simp add: monoseq_def) 

1214 

1215 
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" 

1216 
by (simp add: monoseq_def) 

1217 

1218 
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" 

1219 
by (simp add: monoseq_Suc) 

1220 

1221 
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" 

1222 
by (simp add: monoseq_Suc) 

1223 

1224 
lemma monoseq_minus: 

1225 
fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add" 

1226 
assumes "monoseq a" 

1227 
shows "monoseq (\<lambda> n.  a n)" 

1228 
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") 

1229 
case True 

1230 
hence "\<forall> m. \<forall> n \<ge> m.  a n \<le>  a m" by auto 

1231 
thus ?thesis by (rule monoI2) 

1232 
next 

1233 
case False 

1234 
hence "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" using `monoseq a`[unfolded monoseq_def] by auto 

1235 
thus ?thesis by (rule monoI1) 

1236 
qed 

1237 

1238 
text{*Subsequence (alternative definition, (e.g. Hoskins)*} 

1239 

1240 
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" 

1241 
apply (simp add: subseq_def) 

1242 
apply (auto dest!: less_imp_Suc_add) 

1243 
apply (induct_tac k) 

1244 
apply (auto intro: less_trans) 

1245 
done 

1246 

1247 
text{* for any sequence, there is a monotonic subsequence *} 

1248 
lemma seq_monosub: 

1249 
fixes s :: "nat => 'a::linorder" 

1250 
shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))" 

1251 
proof cases 

1252 
let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)" 

1253 
assume *: "\<forall>n. \<exists>p. ?P p n" 

1254 
def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)" 

1255 
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp 

1256 
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. 

1257 
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto 

1258 
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto 

1259 
then have "subseq f" unfolding subseq_Suc_iff by auto 

1260 
moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc 

1261 
proof (intro disjI2 allI) 

1262 
fix n show "s (f (Suc n)) \<le> s (f n)" 

1263 
proof (cases n) 

1264 
case 0 with P_Suc[of 0] P_0 show ?thesis by auto 

1265 
next 

1266 
case (Suc m) 

1267 
from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp 

1268 
with P_Suc Suc show ?thesis by simp 

1269 
qed 

1270 
qed 

1271 
ultimately show ?thesis by auto 

1272 
next 

1273 
let "?P p m" = "m < p \<and> s m < s p" 

1274 
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))" 

1275 
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less) 

1276 
def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)" 

1277 
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp 

1278 
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. 

1279 
have P_0: "?P (f 0) (Suc N)" 

1280 
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto 

1281 
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)" 

1282 
unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . } 

1283 
note P' = this 

1284 
{ fix i have "N < f i \<and> ?P (f (Suc i)) (f i)" 

1285 
by (induct i) (insert P_0 P', auto) } 

1286 
then have "subseq f" "monoseq (\<lambda>x. s (f x))" 

1287 
unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le) 

1288 
then show ?thesis by auto 

1289 
qed 

1290 

1291 
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" 

1292 
proof(induct n) 

1293 
case 0 thus ?case by simp 

1294 
next 

1295 
case (Suc n) 

1296 
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps 

1297 
have "n < f (Suc n)" by arith 

1298 
thus ?case by arith 

1299 
qed 

1300 

1301 
lemma eventually_subseq: 

1302 
"subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially" 

1303 
unfolding eventually_sequentially by (metis seq_suble le_trans) 

1304 

51473  1305 
lemma not_eventually_sequentiallyD: 
1306 
assumes P: "\<not> eventually P sequentially" 

1307 
shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))" 

1308 
proof  

1309 
from P have "\<forall>n. \<exists>m\<ge>n. \<not> P m" 

1310 
unfolding eventually_sequentially by (simp add: not_less) 

1311 
then obtain r where "\<And>n. r n \<ge> n" "\<And>n. \<not> P (r n)" 

1312 
by (auto simp: choice_iff) 

1313 
then show ?thesis 

1314 
by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"] 

1315 
simp: less_eq_Suc_le subseq_Suc_iff) 

1316 
qed 

1317 

51471  1318 
lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially" 
1319 
unfolding filterlim_iff by (metis eventually_subseq) 

1320 

1321 
lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)" 

1322 
unfolding subseq_def by simp 

1323 

1324 
lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n" 

1325 
using assms by (auto simp: subseq_def) 

1326 

1327 
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X" 

1328 
by (simp add: incseq_def monoseq_def) 

1329 

1330 
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X" 

1331 
by (simp add: decseq_def monoseq_def) 

1332 

1333 
lemma decseq_eq_incseq: 

1334 
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n.  X n)" 

1335 
by (simp add: decseq_def incseq_def) 

1336 

1337 
lemma INT_decseq_offset: 

1338 
assumes "decseq F" 

1339 
shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)" 

1340 
proof safe 

1341 
fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)" 

1342 
show "x \<in> F i" 

1343 
proof cases 

1344 
from x have "x \<in> F n" by auto 

1345 
also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i" 

1346 
unfolding decseq_def by simp 

1347 
finally show ?thesis . 

1348 
qed (insert x, simp) 

1349 
qed auto 

1350 

1351 
lemma LIMSEQ_const_iff: 

1352 
fixes k l :: "'a::t2_space" 

1353 
shows "(\<lambda>n. k) > l \<longleftrightarrow> k = l" 

1354 
using trivial_limit_sequentially by (rule tendsto_const_iff) 

1355 

1356 
lemma LIMSEQ_SUP: 

1357 
"incseq X \<Longrightarrow> X > (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})" 

1358 
by (intro increasing_tendsto) 

1359 
(auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans) 

1360 

1361 
lemma LIMSEQ_INF: 

1362 
"decseq X \<Longrightarrow> X > (INF i. X i :: 'a :: {complete_linorder, linorder_topology})" 

1363 
by (intro decreasing_tendsto) 

1364 
(auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans) 

1365 

1366 
lemma LIMSEQ_ignore_initial_segment: 

1367 
"f > a \<Longrightarrow> (\<lambda>n. f (n + k)) > a" 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

1368 
unfolding tendsto_def 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

1369 
by (subst eventually_sequentially_seg[where k=k]) 
51471  1370 

1371 
lemma LIMSEQ_offset: 

1372 
"(\<lambda>n. f (n + k)) > a \<Longrightarrow> f > a" 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

1373 
unfolding tendsto_def 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

1374 
by (subst (asm) eventually_sequentially_seg[where k=k]) 
51471  1375 

1376 
lemma LIMSEQ_Suc: "f > l \<Longrightarrow> (\<lambda>n. f (Suc n)) > l" 

1377 
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) 

1378 

1379 
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) > l \<Longrightarrow> f > l" 

1380 
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) 

1381 

1382 
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) > l = f > l" 

1383 
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) 

1384 

1385 
lemma LIMSEQ_unique: 

1386 
fixes a b :: "'a::t2_space" 

1387 
shows "\<lbrakk>X > a; X > b\<rbrakk> \<Longrightarrow> a = b" 

1388 
using trivial_limit_sequentially by (rule tendsto_unique) 

1389 

1390 
lemma LIMSEQ_le_const: 

1391 
"\<lbrakk>X > (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" 

1392 
using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially) 

1393 

1394 
lemma LIMSEQ_le: 

1395 
"\<lbrakk>X > x; Y > y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)" 

1396 
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) 

1397 

1398 
lemma LIMSEQ_le_const2: 

1399 
"\<lbrakk>X > (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" 

1400 
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const) 

1401 

1402 
lemma convergentD: "convergent X ==> \<exists>L. (X > L)" 

1403 
by (simp add: convergent_def) 

1404 

1405 
lemma convergentI: "(X > L) ==> convergent X" 

1406 
by (auto simp add: convergent_def) 

1407 

1408 
lemma convergent_LIMSEQ_iff: "convergent X = (X > lim X)" 

1409 
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) 

1410 

1411 
lemma convergent_const: "convergent (\<lambda>n. c)" 

1412 
by (rule convergentI, rule tendsto_const) 

1413 

1414 
lemma monoseq_le: 

1415 
"monoseq a \<Longrightarrow> a > (x::'a::linorder_topology) \<Longrightarrow> 

1416 
((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))" 

1417 
by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff) 

1418 

1419 
lemma LIMSEQ_subseq_LIMSEQ: 

1420 
"\<lbrakk> X > L; subseq f \<rbrakk> \<Longrightarrow> (X o f) > L" 

1421 
unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq]) 

1422 

1423 
lemma convergent_subseq_convergent: 

1424 
"\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)" 

1425 
unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ) 

1426 

1427 
lemma limI: "X > L ==> lim X = L" 

1428 
apply (simp add: lim_def) 

1429 
apply (blast intro: LIMSEQ_unique) 

1430 
done 

1431 

1432 
lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x" 

1433 
using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff) 

1434 

1435 
subsubsection{*Increasing and Decreasing Series*} 

1436 

1437 
lemma incseq_le: "incseq X \<Longrightarrow> X > L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)" 

1438 
by (metis incseq_def LIMSEQ_le_const) 

1439 

1440 
lemma decseq_le: "decseq X \<Longrightarrow> X > L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n" 

1441 
by (metis decseq_def LIMSEQ_le_const2) 

1442 

51473  1443 
subsection {* First countable topologies *} 
1444 

1445 
class first_countable_topology = topological_space + 

1446 
assumes first_countable_basis: 

1447 
"\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

1448 

1449 
lemma (in first_countable_topology) countable_basis_at_decseq: 

1450 
obtains A :: "nat \<Rightarrow> 'a set" where 

1451 
"\<And>i. open (A i)" "\<And>i. x \<in> (A i)" 

1452 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially" 

1453 
proof atomize_elim 

1454 
from first_countable_basis[of x] obtain A 