author  hoelzl 
Tue, 09 Apr 2013 14:04:41 +0200  
changeset 51641  cd05e9fcc63d 
parent 51518  6a56b7088a6a 
child 51773  9328c6681f3c 
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 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51481
diff
changeset

9 
imports Main Conditional_Complete_Lattices 
51471  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 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

42 
lemma openI: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

43 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

44 
shows "open S" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

45 
proof  
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

46 
have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

47 
moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

48 
ultimately show "open S" by simp 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

49 
qed 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

50 

51471  51 
lemma closed_empty [intro, simp]: "closed {}" 
52 
unfolding closed_def by simp 

53 

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

55 
unfolding closed_def by auto 

56 

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

58 
unfolding closed_def by simp 

59 

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

61 
unfolding closed_def by auto 

62 

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

64 
unfolding closed_def by auto 

65 

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

67 
unfolding closed_def uminus_Inf by auto 

68 

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

70 
by (induct set: finite) auto 

71 

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

73 
unfolding SUP_def by (rule closed_Union) auto 

74 

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

76 
unfolding closed_def by simp 

77 

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

79 
unfolding closed_def by simp 

80 

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

82 
unfolding closed_open Diff_eq by (rule open_Int) 

83 

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

85 
unfolding open_closed Diff_eq by (rule closed_Int) 

86 

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

88 
unfolding closed_open . 

89 

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

91 
unfolding open_closed . 

92 

93 
end 

94 

95 
subsection{* Hausdorff and other separation properties *} 

96 

97 
class t0_space = topological_space + 

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

99 

100 
class t1_space = topological_space + 

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

102 

103 
instance t1_space \<subseteq> t0_space 

104 
proof qed (fast dest: t1_space) 

105 

106 
lemma separation_t1: 

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

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

109 
using t1_space[of x y] by blast 

110 

111 
lemma closed_singleton: 

112 
fixes a :: "'a::t1_space" 

113 
shows "closed {a}" 

114 
proof  

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

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

117 
also have "?T =  {a}" 

118 
by (simp add: set_eq_iff separation_t1, auto) 

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

120 
qed 

121 

122 
lemma closed_insert [simp]: 

123 
fixes a :: "'a::t1_space" 

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

125 
proof  

126 
from closed_singleton assms 

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

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

129 
qed 

130 

131 
lemma finite_imp_closed: 

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

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

134 
by (induct set: finite, simp_all) 

135 

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

137 

138 
class t2_space = topological_space + 

139 
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 = {}" 

140 

141 
instance t2_space \<subseteq> t1_space 

142 
proof qed (fast dest: hausdorff) 

143 

144 
lemma separation_t2: 

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

146 
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 = {})" 

147 
using hausdorff[of x y] by blast 

148 

149 
lemma separation_t0: 

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

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

152 
using t0_space[of x y] by blast 

153 

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

155 

156 
class perfect_space = topological_space + 

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

158 

159 

160 
subsection {* Generators for toplogies *} 

161 

162 
inductive generate_topology for S where 

163 
UNIV: "generate_topology S UNIV" 

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

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

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

167 

168 
hide_fact (open) UNIV Int UN Basis 

169 

170 
lemma generate_topology_Union: 

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

172 
unfolding SUP_def by (intro generate_topology.UN) auto 

173 

174 
lemma topological_space_generate_topology: 

175 
"class.topological_space (generate_topology S)" 

176 
by default (auto intro: generate_topology.intros) 

177 

178 
subsection {* Order topologies *} 

179 

180 
class order_topology = order + "open" + 

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

182 
begin 

183 

184 
subclass topological_space 

185 
unfolding open_generated_order 

186 
by (rule topological_space_generate_topology) 

187 

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

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

190 

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

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

193 

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

195 
unfolding greaterThanLessThan_eq by (simp add: open_Int) 

196 

197 
end 

198 

199 
class linorder_topology = linorder + order_topology 

200 

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

202 
by (simp add: closed_open) 

203 

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

205 
by (simp add: closed_open) 

206 

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

208 
proof  

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

210 
by auto 

211 
then show ?thesis 

212 
by (simp add: closed_Int) 

213 
qed 

214 

215 
lemma (in linorder) less_separate: 

216 
assumes "x < y" 

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

218 
proof cases 

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

220 
then guess z .. 

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

222 
by auto 

223 
then show ?thesis by blast 

224 
next 

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

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

227 
by auto 

228 
then show ?thesis by blast 

229 
qed 

230 

231 
instance linorder_topology \<subseteq> t2_space 

232 
proof 

233 
fix x y :: 'a 

234 
from less_separate[of x y] less_separate[of y x] 

235 
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 = {}" 

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

237 
qed 

238 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

239 
lemma (in linorder_topology) open_right: 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

240 
assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S" 
51471  241 
using assms unfolding open_generated_order 
242 
proof induction 

243 
case (Int A B) 

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

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

246 
next 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

247 
case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex) 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

248 
qed blast+ 
51471  249 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

250 
lemma (in linorder_topology) open_left: 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

251 
assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S" 
51471  252 
using assms unfolding open_generated_order 
253 
proof induction 

254 
case (Int A B) 

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

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

257 
next 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

258 
case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex) 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

259 
qed blast+ 
51471  260 

261 
subsection {* Filters *} 

262 

263 
text {* 

264 
This definition also allows nonproper filters. 

265 
*} 

266 

267 
locale is_filter = 

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

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

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

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

272 

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

274 
proof 

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

276 
qed 

277 

278 
lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" 

279 
using Rep_filter [of F] by simp 

280 

281 
lemma Abs_filter_inverse': 

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

283 
using assms by (simp add: Abs_filter_inverse) 

284 

285 

286 
subsubsection {* Eventually *} 

287 

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

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

290 

291 
lemma eventually_Abs_filter: 

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

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

294 

295 
lemma filter_eq_iff: 

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

297 
unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. 

298 

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

300 
unfolding eventually_def 

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

302 

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

304 
proof  

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

306 
thus "eventually P F" by simp 

307 
qed 

308 

309 
lemma eventually_mono: 

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

311 
unfolding eventually_def 

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

313 

314 
lemma eventually_conj: 

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

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

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

318 
using assms unfolding eventually_def 

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

320 

321 
lemma eventually_Ball_finite: 

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

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

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

325 

326 
lemma eventually_all_finite: 

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

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

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

330 
using eventually_Ball_finite [of UNIV P] assms by simp 

331 

332 
lemma eventually_mp: 

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

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

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

336 
proof (rule eventually_mono) 

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

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

339 
using assms by (rule eventually_conj) 

340 
qed 

341 

342 
lemma eventually_rev_mp: 

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

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

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

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

347 

348 
lemma eventually_conj_iff: 

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

350 
by (auto intro: eventually_conj elim: eventually_rev_mp) 

351 

352 
lemma eventually_elim1: 

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

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

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

356 
using assms by (auto elim!: eventually_rev_mp) 

357 

358 
lemma eventually_elim2: 

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

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

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

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

363 
using assms by (auto elim!: eventually_rev_mp) 

364 

365 
lemma eventually_subst: 

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

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

368 
proof  

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

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

371 
by (auto elim: eventually_elim1) 

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

373 
qed 

374 

375 
ML {* 

376 
fun eventually_elim_tac ctxt thms thm = 

377 
let 

378 
val thy = Proof_Context.theory_of ctxt 

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

380 
val raw_elim_thm = 

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

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

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

384 
val cases_prop = prop_of (raw_elim_thm RS thm) 

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

386 
in 

387 
CASES cases (rtac raw_elim_thm 1) thm 

388 
end 

389 
*} 

390 

391 
method_setup eventually_elim = {* 

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

393 
*} "elimination of eventually quantifiers" 

394 

395 

396 
subsubsection {* Finerthan relation *} 

397 

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

399 
filter @{term F'}. *} 

400 

401 
instantiation filter :: (type) complete_lattice 

402 
begin 

403 

404 
definition le_filter_def: 

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

406 

407 
definition 

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

409 

410 
definition 

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

412 

413 
definition 

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

415 

416 
definition 

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

418 

419 
definition 

420 
"inf F F' = Abs_filter 

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

422 

423 
definition 

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

425 

426 
definition 

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

428 

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

430 
unfolding top_filter_def 

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

432 

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

434 
unfolding bot_filter_def 

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

436 

437 
lemma eventually_sup: 

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

439 
unfolding sup_filter_def 

440 
by (rule eventually_Abs_filter, rule is_filter.intro) 

441 
(auto elim!: eventually_rev_mp) 

442 

443 
lemma eventually_inf: 

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

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

446 
unfolding inf_filter_def 

447 
apply (rule eventually_Abs_filter, rule is_filter.intro) 

448 
apply (fast intro: eventually_True) 

449 
apply clarify 

450 
apply (intro exI conjI) 

451 
apply (erule (1) eventually_conj) 

452 
apply (erule (1) eventually_conj) 

453 
apply simp 

454 
apply auto 

455 
done 

456 

457 
lemma eventually_Sup: 

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

459 
unfolding Sup_filter_def 

460 
apply (rule eventually_Abs_filter, rule is_filter.intro) 

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

462 
done 

463 

464 
instance proof 

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

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

467 
by (rule less_filter_def) } 

468 
{ show "F \<le> F" 

469 
unfolding le_filter_def by simp } 

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

471 
unfolding le_filter_def by simp } 

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

473 
unfolding le_filter_def filter_eq_iff by fast } 

474 
{ show "F \<le> top" 

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

476 
{ show "bot \<le> F" 

477 
unfolding le_filter_def by simp } 

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

479 
unfolding le_filter_def eventually_sup by simp_all } 

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

481 
unfolding le_filter_def eventually_sup by simp } 

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

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

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

485 
unfolding le_filter_def eventually_inf 

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

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

488 
unfolding le_filter_def eventually_Sup by simp } 

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

490 
unfolding le_filter_def eventually_Sup by simp } 

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

492 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

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

494 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

495 
qed 

496 

497 
end 

498 

499 
lemma filter_leD: 

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

501 
unfolding le_filter_def by simp 

502 

503 
lemma filter_leI: 

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

505 
unfolding le_filter_def by simp 

506 

507 
lemma eventually_False: 

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

509 
unfolding filter_eq_iff by (auto elim: eventually_rev_mp) 

510 

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

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

513 

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

515 
by (rule eventually_False [symmetric]) 

516 

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

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

519 

520 

521 
subsubsection {* Map function for filters *} 

522 

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

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

525 

526 
lemma eventually_filtermap: 

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

528 
unfolding filtermap_def 

529 
apply (rule eventually_Abs_filter) 

530 
apply (rule is_filter.intro) 

531 
apply (auto elim!: eventually_rev_mp) 

532 
done 

533 

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

535 
by (simp add: filter_eq_iff eventually_filtermap) 

536 

537 
lemma filtermap_filtermap: 

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

539 
by (simp add: filter_eq_iff eventually_filtermap) 

540 

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

542 
unfolding le_filter_def eventually_filtermap by simp 

543 

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

545 
by (simp add: filter_eq_iff eventually_filtermap) 

546 

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

548 
by (auto simp: filter_eq_iff eventually_filtermap eventually_sup) 

549 

550 
subsubsection {* Order filters *} 

551 

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

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

554 

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

556 
unfolding at_top_def 

557 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

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

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

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

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

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

563 
qed auto 

564 

565 
lemma eventually_ge_at_top: 

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

567 
unfolding eventually_at_top_linorder by auto 

568 

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

570 
unfolding eventually_at_top_linorder 

571 
proof safe 

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

573 
next 

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

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

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

577 
qed 

578 

579 
lemma eventually_gt_at_top: 

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

581 
unfolding eventually_at_top_dense by auto 

582 

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

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

585 

586 
lemma eventually_at_bot_linorder: 

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

588 
unfolding at_bot_def 

589 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

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

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

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

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

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

595 
qed auto 

596 

597 
lemma eventually_le_at_bot: 

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

599 
unfolding eventually_at_bot_linorder by auto 

600 

601 
lemma eventually_at_bot_dense: 

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

603 
unfolding eventually_at_bot_linorder 

604 
proof safe 

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

606 
next 

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

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

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

610 
qed 

611 

612 
lemma eventually_gt_at_bot: 

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

614 
unfolding eventually_at_bot_dense by auto 

615 

616 
subsection {* Sequentially *} 

617 

618 
abbreviation sequentially :: "nat filter" 

619 
where "sequentially == at_top" 

620 

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

622 
unfolding at_top_def by simp 

623 

624 
lemma eventually_sequentially: 

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

626 
by (rule eventually_at_top_linorder) 

627 

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

629 
unfolding filter_eq_iff eventually_sequentially by auto 

630 

631 
lemmas trivial_limit_sequentially = sequentially_bot 

632 

633 
lemma eventually_False_sequentially [simp]: 

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

635 
by (simp add: eventually_False) 

636 

637 
lemma le_sequentially: 

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

639 
unfolding le_filter_def eventually_sequentially 

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

641 

642 
lemma eventually_sequentiallyI: 

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

644 
shows "eventually P sequentially" 

645 
using assms by (auto simp: eventually_sequentially) 

646 

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

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

648 
"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

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

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

651 
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

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

653 
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

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

655 
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

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

657 
done 
51471  658 

659 
subsubsection {* Standard filters *} 

660 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

661 
definition principal :: "'a set \<Rightarrow> 'a filter" where 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

662 
"principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

663 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

664 
lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

665 
unfolding principal_def 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

666 
by (rule eventually_Abs_filter, rule is_filter.intro) auto 
51471  667 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

668 
lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

669 
unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

670 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

671 
lemma principal_UNIV[simp]: "principal UNIV = top" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

672 
by (auto simp: filter_eq_iff eventually_principal) 
51471  673 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

674 
lemma principal_empty[simp]: "principal {} = bot" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

675 
by (auto simp: filter_eq_iff eventually_principal) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

676 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

677 
lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

678 
by (auto simp: le_filter_def eventually_principal) 
51471  679 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

680 
lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

681 
unfolding le_filter_def eventually_principal 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

682 
apply safe 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

683 
apply (erule_tac x="\<lambda>x. x \<in> A" in allE) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

684 
apply (auto elim: eventually_elim1) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

685 
done 
51471  686 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

687 
lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

688 
unfolding eq_iff by simp 
51471  689 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

690 
lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

691 
unfolding filter_eq_iff eventually_sup eventually_principal by auto 
51471  692 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

693 
lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

694 
unfolding filter_eq_iff eventually_inf eventually_principal 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

695 
by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"]) 
51471  696 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

697 
lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

698 
unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

699 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

700 
lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

701 
unfolding filter_eq_iff eventually_filtermap eventually_principal by simp 
51471  702 

703 
subsubsection {* Topological filters *} 

704 

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

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

707 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

708 
definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

709 
where "at a within s = inf (nhds a) (principal (s  {a}))" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

710 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

711 
abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

712 
"at x \<equiv> at x within (CONST UNIV)" 
51471  713 

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

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

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

723 
proof (rule eventually_Abs_filter, rule is_filter.intro) 

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

727 
fix P Q 

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

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

730 
then obtain S T where 

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

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

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

734 
by (simp add: open_Int) 

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

736 
qed auto 

737 

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

739 
unfolding trivial_limit_def eventually_nhds by simp 

740 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

741 
lemma eventually_at_filter: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

742 
"eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

743 
unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

744 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

745 
lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

746 
unfolding at_within_def by (intro inf_mono) auto 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

747 

51471  748 
lemma eventually_at_topological: 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

749 
"eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

750 
unfolding eventually_nhds eventually_at_filter by simp 
51471  751 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

752 
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

753 
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) 
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

754 

51471  755 
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" 
756 
unfolding trivial_limit_def eventually_at_topological 

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

758 

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

760 
by (simp add: at_eq_bot_iff not_open_singleton) 

761 

762 
lemma eventually_at_right: 

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

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

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

765 
unfolding eventually_at_topological 
51471  766 
proof safe 
51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

767 
from gt_ex[of x] guess y .. 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

768 
moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y] 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

769 
moreover note gt_ex[of x] 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

770 
moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s" 
51471  771 
ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z" 
772 
by (auto simp: subset_eq Ball_def) 

773 
next 

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

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

775 
then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)" 
51471  776 
by (intro exI[of _ "{..< b}"]) auto 
777 
qed 

778 

779 
lemma eventually_at_left: 

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

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

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

782 
unfolding eventually_at_topological 
51471  783 
proof safe 
51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

784 
from lt_ex[of x] guess y .. 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

785 
moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y] 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

786 
moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s" 
51471  787 
ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z" 
788 
by (auto simp: subset_eq Ball_def) 

789 
next 

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

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

791 
then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s)" 
51471  792 
by (intro exI[of _ "{b <..}"]) auto 
793 
qed 

794 

795 
lemma trivial_limit_at_left_real [simp]: 

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

797 
unfolding trivial_limit_def eventually_at_left by (auto dest: dense) 

798 

799 
lemma trivial_limit_at_right_real [simp]: 

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

801 
unfolding trivial_limit_def eventually_at_right by (auto dest: dense) 

802 

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

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

804 
by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
51471  805 
elim: eventually_elim2 eventually_elim1) 
806 

807 
lemma eventually_at_split: 

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

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

810 

811 
subsection {* Limits *} 

812 

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

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

815 

816 
syntax 

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

818 

819 
translations 

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

821 

822 
lemma filterlim_iff: 

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

824 
unfolding filterlim_def le_filter_def eventually_filtermap .. 

825 

826 
lemma filterlim_compose: 

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

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

829 

830 
lemma filterlim_mono: 

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

832 
unfolding filterlim_def by (metis filtermap_mono order_trans) 

833 

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

835 
by (simp add: filterlim_def filtermap_ident) 

836 

837 
lemma filterlim_cong: 

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

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

840 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

841 
lemma filterlim_principal: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

842 
"(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

843 
unfolding filterlim_def eventually_filtermap le_principal .. 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

844 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

845 
lemma filterlim_inf: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

846 
"(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

847 
unfolding filterlim_def by simp 
51471  848 

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

850 
unfolding filterlim_def filtermap_filtermap .. 

851 

852 
lemma filterlim_sup: 

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

854 
unfolding filterlim_def filtermap_sup by auto 

855 

856 
lemma filterlim_Suc: "filterlim Suc sequentially sequentially" 

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

858 

859 
subsubsection {* Tendsto *} 

860 

861 
abbreviation (in topological_space) 

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

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

864 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

865 
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

866 
"Lim A f = (THE l. (f > l) A)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

867 

51471  868 
lemma tendsto_eq_rhs: "(f > x) F \<Longrightarrow> x = y \<Longrightarrow> (f > y) F" 
869 
by simp 

870 

871 
ML {* 

872 

873 
structure Tendsto_Intros = Named_Thms 

874 
( 

875 
val name = @{binding tendsto_intros} 

876 
val description = "introduction rules for tendsto" 

877 
) 

878 

879 
*} 

880 

881 
setup {* 

882 
Tendsto_Intros.setup #> 

883 
Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros}, 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

884 
map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of); 
51471  885 
*} 
886 

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

51471  889 
unfolding filterlim_def 
890 
proof safe 

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

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

893 
unfolding eventually_nhds eventually_filtermap le_filter_def 

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

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

896 

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

898 
unfolding tendsto_def le_filter_def by fast 

899 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

900 
lemma tendsto_within_subset: "(f > l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f > l) (at x within T)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

901 
by (blast intro: tendsto_mono at_le) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

902 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

903 
lemma filterlim_at: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

904 
"(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f > b) F)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

905 
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

906 

51473  907 
lemma (in topological_space) topological_tendstoI: 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

908 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f > l) F" 
51471  909 
unfolding tendsto_def by auto 
910 

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

914 

915 
lemma order_tendstoI: 

916 
fixes y :: "_ :: order_topology" 

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

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

919 
shows "(f > y) F" 

920 
proof (rule topological_tendstoI) 

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

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

923 
unfolding open_generated_order 

924 
proof induct 

925 
case (UN K) 

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

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

928 
by (auto elim: eventually_elim1) 

929 
qed (insert assms, auto elim: eventually_elim2) 

930 
qed 

931 

932 
lemma order_tendstoD: 

933 
fixes y :: "_ :: order_topology" 

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

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

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

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

938 

939 
lemma order_tendsto_iff: 

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

941 
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)" 

942 
by (metis order_tendstoI order_tendstoD) 

943 

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

945 
unfolding tendsto_def by simp 

946 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

947 
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) > a) (at a within s)" 
51471  948 
unfolding tendsto_def eventually_at_topological by auto 
949 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

950 
lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) > k) F" 
51471  951 
by (simp add: tendsto_def) 
952 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

953 
lemma (in t2_space) tendsto_unique: 
51471  954 
assumes "\<not> trivial_limit F" and "(f > a) F" and "(f > b) F" 
955 
shows "a = b" 

956 
proof (rule ccontr) 

957 
assume "a \<noteq> b" 

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

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

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

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

962 
moreover 

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

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

965 
ultimately 

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

967 
proof eventually_elim 

968 
case (elim x) 

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

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

971 
qed 

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

973 
by (simp add: trivial_limit_def) 

974 
qed 

975 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

976 
lemma (in t2_space) tendsto_const_iff: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

977 
assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) > b) F \<longleftrightarrow> a = b" 
51471  978 
by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) 
979 

980 
lemma increasing_tendsto: 

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

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

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

984 
shows "(f > l) F" 

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

986 

987 
lemma decreasing_tendsto: 

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

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

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

991 
shows "(f > l) F" 

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

993 

994 
lemma tendsto_sandwich: 

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

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

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

998 
shows "(g > c) net" 

999 
proof (rule order_tendstoI) 

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

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

1002 
next 

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

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

1005 
qed 

1006 

1007 
lemma tendsto_le: 

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

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

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

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

1012 
shows "y \<le> x" 

1013 
proof (rule ccontr) 

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

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

1016 
by (auto simp: not_le) 

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

1018 
using x y by (auto intro: order_tendstoD) 

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

1020 
by eventually_elim (insert xy, fastforce) 

1021 
with F show False 

1022 
by (simp add: eventually_False) 

1023 
qed 

1024 

1025 
lemma tendsto_le_const: 

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

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

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

1029 
shows "a \<le> x" 

1030 
using F x tendsto_const a by (rule tendsto_le) 

1031 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1032 
subsubsection {* Rules about @{const Lim} *} 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1033 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1034 
lemma (in t2_space) tendsto_Lim: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1035 
"\<not>(trivial_limit net) \<Longrightarrow> (f > l) net \<Longrightarrow> Lim net f = l" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1036 
unfolding Lim_def using tendsto_unique[of net f] by auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1037 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1038 
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1039 
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1040 

51471  1041 
subsection {* Limits to @{const at_top} and @{const at_bot} *} 
1042 

1043 
lemma filterlim_at_top: 

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

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

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

1047 

1048 
lemma filterlim_at_top_dense: 

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

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

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

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

1053 

1054 
lemma filterlim_at_top_ge: 

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

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

1057 
unfolding filterlim_at_top 

1058 
proof safe 

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

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

1061 
by (auto elim!: eventually_elim1) 

1062 
qed simp 

1063 

1064 
lemma filterlim_at_top_at_top: 

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

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

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

1068 
assumes Q: "eventually Q at_top" 

1069 
assumes P: "eventually P at_top" 

1070 
shows "filterlim f at_top at_top" 

1071 
proof  

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

1073 
unfolding eventually_at_top_linorder by auto 

1074 
show ?thesis 

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

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

1077 
with x have "P z" by auto 

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

1079 
by (rule eventually_ge_at_top) 

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

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

1082 
qed 

1083 
qed 

1084 

1085 
lemma filterlim_at_top_gt: 

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

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

1088 
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge) 

1089 

1090 
lemma filterlim_at_bot: 

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

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

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

1094 

1095 
lemma filterlim_at_bot_le: 

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

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

1098 
unfolding filterlim_at_bot 

1099 
proof safe 

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

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

1102 
by (auto elim!: eventually_elim1) 

1103 
qed simp 

1104 

1105 
lemma filterlim_at_bot_lt: 

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

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

1108 
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans) 

1109 

1110 
lemma filterlim_at_bot_at_right: 

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

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

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

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

1115 
assumes P: "eventually P at_bot" 

1116 
shows "filterlim f at_bot (at_right a)" 

1117 
proof  

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

1119 
unfolding eventually_at_bot_linorder by auto 

1120 
show ?thesis 

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

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

1123 
with x have "P z" by auto 

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

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

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

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

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

1129 
qed 

1130 
qed 

1131 

1132 
lemma filterlim_at_top_at_left: 

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

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

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

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

1137 
assumes P: "eventually P at_top" 

1138 
shows "filterlim f at_top (at_left a)" 

1139 
proof  

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

1141 
unfolding eventually_at_top_linorder by auto 

1142 
show ?thesis 

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

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

1145 
with x have "P z" by auto 

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

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

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

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

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

1151 
qed 

1152 
qed 

1153 

1154 
lemma filterlim_split_at: 

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

1156 
by (subst at_eq_sup_left_right) (rule filterlim_sup) 

1157 

1158 
lemma filterlim_at_split: 

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

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

1161 

1162 

1163 
subsection {* Limits on sequences *} 

1164 

1165 
abbreviation (in topological_space) 

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

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

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

1169 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1170 
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1171 
"lim X \<equiv> Lim sequentially X" 
51471  1172 

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

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

1175 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1176 
lemma lim_def: "lim X = (THE L. X > L)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1177 
unfolding Lim_def .. 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1178 

51471  1179 
subsubsection {* Monotone sequences and subsequences *} 
1180 

1181 
definition 

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

1183 
{*Definition of monotonicity. 

1184 
The use of disjunction here complicates proofs considerably. 

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

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

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

1188 

1189 
definition 

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

1191 
{*Increasing sequence*} 

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

1193 

1194 
definition 

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

1196 
{*Decreasing sequence*} 

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

1198 

1199 
definition 

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

1201 
{*Definition of subsequence*} 

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

1203 

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

1205 
unfolding mono_def incseq_def by auto 

1206 

1207 
lemma incseq_SucI: 

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

1209 
using lift_Suc_mono_le[of X] 

1210 
by (auto simp: incseq_def) 

1211 

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

1213 
by (auto simp: incseq_def) 

1214 

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

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

1217 

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

1219 
by (auto intro: incseq_SucI dest: incseq_SucD) 

1220 

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

1222 
unfolding incseq_def by auto 

1223 

1224 
lemma decseq_SucI: 

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

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

1227 
by (auto simp: decseq_def) 

1228 

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

1230 
by (auto simp: decseq_def) 

1231 

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

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

1234 

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

1236 
by (auto intro: decseq_SucI dest: decseq_SucD) 

1237 

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

1239 
unfolding decseq_def by auto 

1240 

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

1242 
unfolding monoseq_def incseq_def decseq_def .. 

1243 

1244 
lemma monoseq_Suc: 

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

1246 
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. 

1247 

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

1249 
by (simp add: monoseq_def) 

1250 

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

1252 
by (simp add: monoseq_def) 

1253 

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

1255 
by (simp add: monoseq_Suc) 

1256 

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

1258 
by (simp add: monoseq_Suc) 

1259 

1260 
lemma monoseq_minus: 

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

1262 
assumes "monoseq a" 

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

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

1265 
case True 

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

1267 
thus ?thesis by (rule monoI2) 

1268 
next 

1269 
case False 

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

1271 
thus ?thesis by (rule monoI1) 

1272 
qed 

1273 

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

1275 

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

1277 
apply (simp add: subseq_def) 

1278 
apply (auto dest!: less_imp_Suc_add) 

1279 
apply (induct_tac k) 

1280 
apply (auto intro: less_trans) 

1281 
done 

1282 

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

1284 
lemma seq_monosub: 

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

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

1287 
proof cases 

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

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

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

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

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

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

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

1295 
then have "subseq f" unfolding subseq_Suc_iff by auto 

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

1297 
proof (intro disjI2 allI) 

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

1299 
proof (cases n) 

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

1301 
next 

1302 
case (Suc m) 

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

1304 
with P_Suc Suc show ?thesis by simp 

1305 
qed 

1306 
qed 

1307 
ultimately show ?thesis by auto 

1308 
next 

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

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

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

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

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

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

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

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

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

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

1319 
note P' = this 

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

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

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

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

1324 
then show ?thesis by auto 

1325 
qed 

1326 

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

1328 
proof(induct n) 

1329 
case 0 thus ?case by simp 

1330 
next 

1331 
case (Suc n) 

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

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

1334 
thus ?case by arith 

1335 
qed 

1336 

1337 
lemma eventually_subseq: 

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

1339 
unfolding eventually_sequentially by (metis seq_suble le_trans) 

1340 

51473  1341 
lemma not_eventually_sequentiallyD: 
1342 
assumes P: "\<not> eventually P sequentially" 

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

1344 
proof  

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

1346 
unfolding eventually_sequentially by (simp add: not_less) 

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

1348 
by (auto simp: choice_iff) 

1349 
then show ?thesis 

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

1351 
simp: less_eq_Suc_le subseq_Suc_iff) 

1352 
qed 

1353 

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

1356 

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

1358 
unfolding subseq_def by simp 

1359 

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

1361 
using assms by (auto simp: subseq_def) 

1362 

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

1364 
by (simp add: incseq_def monoseq_def) 

1365 

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

1367 
by (simp add: decseq_def monoseq_def) 

1368 

1369 
lemma decseq_eq_incseq: 

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

1371 
by (simp add: decseq_def incseq_def) 

1372 

1373 
lemma INT_decseq_offset: 

1374 
assumes "decseq F" 

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

1376 
proof safe 

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

1378 
show "x \<in> F i" 

1379 
proof cases 

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

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

1382 
unfolding decseq_def by simp 

1383 
finally show ?thesis . 

1384 
qed (insert x, simp) 

1385 
qed auto 

1386 

1387 
lemma LIMSEQ_const_iff: 

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

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

1390 
using trivial_limit_sequentially by (rule tendsto_const_iff) 

1391 

1392 
lemma LIMSEQ_SUP: 

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

1394 
by (intro increasing_tendsto) 

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

1396 

1397 
lemma LIMSEQ_INF: 

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

1399 
by (intro decreasing_tendsto) 

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

1401 

1402 
lemma LIMSEQ_ignore_initial_segment: 

1403 
"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

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

1405 
by (subst eventually_sequentially_seg[where k=k]) 
51471  1406 

1407 
lemma LIMSEQ_offset: 

1408 
"(\<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

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

1410 
by (subst (asm) eventually_sequentially_seg[where k=k]) 
51471  1411 

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

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

1414 

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